Model structure on the universe of all types in interval type theory

DOI10.1017/S0960129520000213OpenAlexW3119304695MaRDI QIDQ5022925

Nicolas Tabareau, Simon Boulier

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/s0960129520000213

zbMATH Keywords

model structurehomotopy type theoryfibrant typesinterval type theory

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Uses Software

• Coq
• cubicaltt
• GitHub
• cart-cube

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The identity type weak factorisation system
• Quotient inductive-inductive types
• The Frobenius condition, right properness, and uniform fibrations
• The simplicial model of univalent foundations (after Voevodsky)
• The univalence axiom in cubical sets
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• On Higher Inductive Types in Cubical Type Theory