Martin-Löf complexes

DOI10.1016/J.APAL.2013.05.001MaRDI QIDQ385803zbMATHOpenAlexFDO

Authors Michael A. Warren, Steve Awodey, Pieter Hofstra

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

groupoids1-truncationhomotopy type theoryQuillen model structureMartin-Löf complex

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Abstract: In this paper we define Martin-L"{o}f complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-L"{o}f type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-L"{o}f complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-L"{o}f complexes are a model of homotopy 1-types.

Recommendations

• scientific article; zbMATH DE number 1439417
• Hilbert complexes
• Euler complexes
• Kuratowski complexes
• Morse complexes and multiplicative structures
• scientific article; zbMATH DE number 596351
• scientific article; zbMATH DE number 6806819
• Complexes galoisiens
• Homology of Littlewood complexes
• Selmer complexes

Cites work

• scientific article; zbMATH DE number 2134022 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3521950 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 937396 (Why is no real title available?)
• scientific article; zbMATH DE number 3287761 (Why is no real title available?)
• scientific article; zbMATH DE number 2222246 (Why is no real title available?)
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Categorical logic and type theory
• Combinatorial realizability models of type theory
• Homotopical algebra
• Homotopy theoretic models of identity types
• Locally cartesian closed categories and type theory
• Strong stacks and classifying spaces
• The identity type weak factorisation system
• The petit topos of globular sets
• Two-dimensional models of type theory
• Type theory and homotopy
• Types are weak \(\omega \)-groupoids
• Weak omega-categories from intensional type theory

Cited in

(6)

• Homotopy type theory and Voevodsky's univalent foundations
• Notions of anonymous existence in Martin-Löf type theory
• Loxodromic elements for the relative free factor complex
• Combinatorial realizability models of type theory
• MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
• The category of equilogical spaces and the effective topos as homotopical quotients

This page was built for publication: Martin-Löf complexes

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