Kan Complexes as a Univalent Model of Type Theory
- Date: Monday 29 October 2018, 14:00 – 15:00
- Location: Mathematics Level 8, MALL 1, School of Mathematics
- Type: Seminars, Pure Mathematics
- Cost: Free
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.