Syntax and models of Cartesian cubical type theory
From MaRDI portal
Publication:5022926
DOI10.1017/S0960129521000347OpenAlexW4206010916MaRDI QIDQ5022926
Thierry Coquand, Guillaume Brunerie, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata, Carlo Angiuli
Publication date: 20 January 2022
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129521000347
Related Items (4)
Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ A formal logic for formal category theory ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Meaning explanations at higher dimension
- A cubical model of homotopy type theory
- The Frobenius condition, right properness, and uniform fibrations
- The simplicial model of univalent foundations (after Voevodsky)
- A Kripke model for simplicial sets
- The univalence axiom in cubical sets
- Canonicity for cubical type theory
- Guarded cubical type theory
- An algebraic weak factorisation system on 01-substitution sets: a constructive proof
- A type theory for synthetic $\infty$-categories
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- A Cubical Approach to Synthetic Homotopy Theory
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
- On Higher Inductive Types in Cubical Type Theory
- A Constructive Model of Directed Univalence in Bicubical Sets
- Varieties of Cubical Sets
- Computational higher-dimensional type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- ABSTRACT HOMOTOPY
- Unifying Cubical Models of Univalent Type Theory
- A presheaf model of parametric type theory
This page was built for publication: Syntax and models of Cartesian cubical type theory
