Homotopy canonicity of homotopy type theory
- Date: Wednesday 4 March 2020, 16:00 – 17:00
- Location: Mathematics Level 8, MALL 1, School of Mathematics
- Type: Logic, Seminars, Pure Mathematics
- Cost: Free
Christian Sattler, University of Nottingham. Part of the Logic Seminar Series.
Constructive type theories satisfy *canonicity*, an important metatheoretic property. Canonicity fails for homotopy type theory because of the axioms of univalence and function extensionality. Voevodsky's *homotopy canonicity* conjecture states that a homotopical version of this property still holds: every closed element of the natural number type is related via the identity type to a numeral. So far, this was known only for 1-truncated homotopy type theory, shown by Shulman using Artin glueing along a groupoid-valued global sections functor. In this talk, I will present a proof of homotopy canonicity. This is joint work with Chris Kapulkin.