Canonicity and homotopy canonicity for cubical type theory

zbMath1486.03027arXiv1902.06572MaRDI QIDQ5028486

Simon Huber, Thierry Coquand, Christian Sattler

Publication date: 9 February 2022

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

Mathematics Subject Classification ID

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

Related Items

The compatibility of the minimalist foundation with homotopy type theory

Uses Software

• cubicaltt

Cites Work

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