Canonicity and homotopy canonicity for cubical type theory
From MaRDI portal
Publication:5028486
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 1420782 (Why is no real title available?)
- scientific article; zbMATH DE number 226803 (Why is no real title available?)
- scientific article; zbMATH DE number 3297895 (Why is no real title available?)
- A cubical approach to straightening
- A type theory for synthetic \(\infty\)-categories
- A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
- An algebraic weak factorisation system on 01-substitution sets: a constructive proof
- Axioms for modelling cubical type theory in a topos
- Canonicity and normalization for dependent type theory
- Canonicity for cubical type theory
- Cubical type theory: a constructive interpretation of the univalence axiom
- Homotopy type theory. Univalent foundations of mathematics
- Intensional interpretations of functionals of finite type I
- Internal type theory
- Internal universes in models of homotopy type theory
- On higher inductive types in cubical type theory
- Partial Horn logic and Cartesian categories
- Polynomial functors and polynomial monads
- Semantics of higher inductive types
- The Frobenius condition, right properness, and uniform fibrations
- The simplicial model of univalent foundations (after Voevodsky)
- Types for Proofs and Programs
- Univalence for inverse diagrams and homotopy canonicity
Cited in
(12)- Canonicity for cubical type theory
- Canonicity for 2-dimensional type theory
- On higher inductive types in cubical type theory
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- For the metatheory of type theory, internal sconing is enough
- Axioms for modelling cubical type theory in a topos
- Cubical methods in homotopy type theory and univalent foundations
- A cubical model of homotopy type theory
- A cubical approach to synthetic homotopy theory
- On equivalence and canonical forms in the LF type theory
- Syntax and models of Cartesian cubical type theory
- The compatibility of the minimalist foundation with homotopy type theory
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)
