On Higher Inductive Types in Cubical Type Theory

• DOI: 10.1145/3209108.3209197
• Publication Date: 2018-06-27T12:14:43Z
• Authors: Thierry Coquand; Simon Huber; Anders Mörtberg
• Keywords: Extensionality; Type theory; Topos theory; Constructive

Cubical type theory provides a constructive justification to certain aspects of homotopy such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. paper describes semantics, expressed presheaf topos with suitable structure inspired by cubical sets, some higher inductive types. It also extends syntax for types spheres, torus, suspensions, truncations, pushouts. All these are justified semantics have judgmental computation rules all constructors, including dimensional ones, universes closed under formers.