Syntax and models of Cartesian cubical type theory

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

zbMATH Keywords

type theoryhomotopy type theorycubical type theory

Mathematics Subject Classification ID

General logic (03Bxx)

Related Items (8)

Cubical methods in homotopy type theory and univalent foundations ⋮ Naive cubical type theory ⋮ Simplicial sets inside cubical sets ⋮ A formal logic for formal category theory ⋮ Unnamed Item ⋮ Kripke-Joyal forcing for type theory and uniform fibrations ⋮ A 2-categorical proof of Frobenius for fibrations defined from a generic point ⋮ Single-set cubical categories and their formalisation with a proof assistant

Uses Software

• Nuprl
• cubicaltt
• GitHub
• RedPRL
• cart-cube
• Cubical agda

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