Kan Complexes as a Univalent Model of Type Theory

Gabriele Lobbia, University of Leeds

Voevodsky's Univalence Axiom states that the idea of "identity" and the one of "equivalence" are equivalent. C. Kapulkin and P. L. Lumsdaine provided a model of homotopy type theory where this particular axiom holds. I will start by giving the notions of Kan complexes and fibrations.

Then I will briefly describe type theory and its natural models in category theory. Lastly I will state the type-theoretic and simplicial versions of the univalence axiom and give the idea of the proof in the simplicial model.