Canonicity and homotopy canonicity for cubical type theory

zbMATH Open1486.03027arXiv1902.06572MaRDI QIDQ5028486FDOQ5028486

Authors: Thierry Coquand, Simon Huber, Christian Sattler 

Publication date: 9 February 2022

Abstract: Cubical type theory provides a constructive justification of homotopy type theory. 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. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.

Full work available at URL: https://arxiv.org/abs/1902.06572

Recommendations

• Canonicity for cubical type theory
• Univalence for inverse diagrams and homotopy canonicity
• On higher inductive types in cubical type theory
• scientific article
• scientific article; zbMATH DE number 7003193

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Partial Horn logic and Cartesian categories
• Title not available (Why is that?)
• Internal type theory
• Title not available (Why is that?)
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Intensional interpretations of functionals of finite type I
• The simplicial model of univalent foundations (after Voevodsky)
• Univalence for inverse diagrams and homotopy canonicity
• Polynomial functors and polynomial monads
• Types for Proofs and Programs
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• A cubical approach to straightening
• Semantics of higher inductive types
• Title not available (Why is that?)
• A type theory for synthetic $\infty$-categories
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• The Frobenius condition, right properness, and uniform fibrations
• Title not available (Why is that?)
• On Higher Inductive Types in Cubical Type Theory
• Title not available (Why is that?)
• Canonicity for cubical type theory
• Canonicity and normalization for dependent type theory

Cited In (4)

• Title not available (Why is that?)
• Cubical methods in homotopy type theory and univalent foundations
• On equivalence and canonical forms in the LF type theory
• The compatibility of the minimalist foundation with homotopy type theory

Uses Software

• cubicaltt

This page was built for publication: Canonicity and homotopy canonicity for cubical type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5028486)