Canonicity and homotopy canonicity for cubical type theory
From MaRDI portal
Publication:5028486
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
Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)
Related Items
Uses Software
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