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

DOI10.1017/S0960129520000213MaRDI QIDQ5022925zbMATH OpenOpenAlexFDO

Authors Simon Boulier, Nicolas Tabareau

Publication date 20 January 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/s0960129520000213

zbMATH Keywords

fibrant typeshomotopy type theoryinterval type theorymodel structure

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Recommendations

• Model structures on categories of models of type theories
• Homotopy theoretic models of identity types
• Homotopy-theoretic models of type theory
• Internal universes in models of homotopy type theory
• Natural models of homotopy type theory

Cites work

• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Cotorsion pairs and model categories
• Cubical type theory: a constructive interpretation of the univalence axiom
• Extending homotopy type theory with strict equality
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 7003193 (Why is no real title available?)
• scientific article; zbMATH DE number 1860105 (Why is no real title available?)
• Internal universes in models of homotopy type theory
• Non-constructivity in Kan simplicial sets
• On higher inductive types in cubical type theory
• Quotient inductive-inductive types
• The Frobenius condition, right properness, and uniform fibrations
• The identity type weak factorisation system
• The simplicial model of univalent foundations (after Voevodsky)
• The univalence axiom in cubical sets

Cited in

(3)

• Model structures on categories of models of type theories
• On the ubiquity of certain total type structures
• The equivariant model structure on cartesian cubical sets

Describes a project that uses

Uses Software

• Coq
• cubicaltt
• cart-cube
• GitHub

This page was built for publication: Model structure on the universe of all types in interval type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5022925)