Martin-Löf complexes

DOI10.1016/j.apal.2013.05.001zbMath1323.03012arXiv0906.4521MaRDI QIDQ385803

Michael A. Warren, Pieter J. W. Hofstra, Steven Awodey

Publication date: 11 December 2013

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

groupoids; homotopy type theory; 1-truncation; Martin-Löf complex; Quillen model structure

Mathematics Subject Classification ID

03G30: Categorical logic, topoi

55U40: Topological categories, foundations of homotopy theory

Related Items

Combinatorial realizability models of type theory, Homotopy type theory and Voevodsky’s univalent foundations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatorial realizability models of type theory
• The identity type weak factorisation system
• Categorical logic and type theory
• The petit topos of globular sets
• Homotopical algebra
• Weak omega-categories from intensional type theory
• Types are weak ω -groupoids
• Locally cartesian closed categories and type theory
• Two-dimensional models of type theory
• Homotopy theoretic models of identity types
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Strong stacks and classifying spaces
• Type Theory and Homotopy