On Higher Inductive Types in Cubical Type Theory

On Higher Inductive Types in Cubical Type Theory

[Anders Mortberg]

We recently uploaded the paper "On Higher Inductive Types in
Cubical Type Theory" to the arxiv:

https://arxiv.org/abs/1802.01170


-----
On Higher Inductive Types in Cubical Type Theory
Authors: Thierry Coquand, Simon Huber and Anders Mörtberg

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

--
Anders, Simon and Thierry