Simon Huber Presents Homotopy Canonicity in Cubical Type Theory 🧪

Homotopy Type Theory Electronic Seminar Talks, 2019-02-21 Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this talk I will present why if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral. The proof involves proof relevant computability predicates (also known as sconing) and doesn't involve a reduction relation. This is joint work with Thierry Coquand and Christian Sattler.