Higher inductive types in cubical computational type theory
Abstract
Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 02, 2019
- Source ID
- 10.1145/3290314
Entities
People
- Evan Cavallo
- Robert Harper
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University