Martin-Löf complexes

DOI10.1016/J.APAL.2013.05.001zbMATH Open1323.03012arXiv0906.4521OpenAlexW2098385002MaRDI QIDQ385803FDOQ385803

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)

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.

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

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

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)

Cites Work

• Categorical logic and type theory
• Homotopical algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types are weak \(\omega \)-groupoids
• Title not available (Why is that?)
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Title not available (Why is that?)
• The identity type weak factorisation system
• Locally cartesian closed categories and type theory
• Title not available (Why is that?)
• The petit topos of globular sets
• Weak omega-categories from intensional type theory
• Two-dimensional models of type theory
• Combinatorial realizability models of type theory
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Strong stacks and classifying spaces
• Title not available (Why is that?)
• Type theory and homotopy
• Title not available (Why is that?)

Cited In (6)

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

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)