Homotopy canonicity of homotopy type theory

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.