MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS

DOI10.1017/jsl.2021.39OpenAlexW3166306701MaRDI QIDQ5879185

Nicola Gambino, Marco Federico Larrea

Publication date: 27 February 2023

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1906.01491

zbMATH Keywords

algebraic weak factorisation systemcomprehension categoryMartin-Löf theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Fibered categories (18D30) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

Uses Software

• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic model structures
• Algebraic weak factorisation systems. I: Accessible AWFS.
• Algebraic weak factorisation systems. II: Categories of weak maps.
• The identity type weak factorisation system
• Comprehension categories and the semantics of type dependency
• Categorical logic and type theory
• Types for proofs and programs. International workshop TYPES '95, Torino, Italy, June 5--8, 1995. Selected papers
• On the construction of functorial factorizations for model categories
• The Frobenius condition, right properness, and uniform fibrations
• Revisiting the categorical interpretation of dependent type theory
• A Kripke model for simplicial sets
• The theory and practice of Reedy categories
• Topological and Simplicial Models of Identity Types
• The Local Universes Model
• Locally cartesian closed categories and type theory
• Homotopy theoretic models of identity types
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Elementary fibrations of enriched groupoids
• Understanding the small object argument

This page was built for publication: MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS