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.
Higher Inductive Types in Cubical Computational Type Theory - Slides (slides.pdf) | 2.50MiB |
Fri 18 JanDisplayed time zone: Belfast change
10:35 - 12:03 | |||
10:35 22mTalk | Higher Inductive Types in Cubical Computational Type Theory Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
10:57 22mTalk | Constructing Quotient Inductive-Inductive Types Research Papers Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham, András Kovács Eötvös Loránd University Link to publication DOI Media Attached File Attached | ||
11:19 22mTalk | Definitional Proof-Irrelevance without K Research Papers Gaetan Gilbert , Jesper Cockx Chalmers | University of Gothenburg, Matthieu Sozeau Inria, Nicolas Tabareau Inria Link to publication DOI Media Attached File Attached | ||
11:41 22mTalk | Bisimulation as Path Type for Guarded Recursive Types Research Papers Link to publication DOI Media Attached File Attached |