Homotopy limits in type theory
2015 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 25, no 5, 1040-1070 p.Article in journal (Refereed) Published
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.
Place, publisher, year, edition, pages
2015. Vol. 25, no 5, 1040-1070 p.
homotopy type theory, homotopy limits, pullbacks, formalisation, proof assistants
Algebra and Logic
Research subject Mathematical Logic
IdentifiersURN: urn:nbn:se:su:diva-128394DOI: 10.1017/S0960129514000498OAI: oai:DiVA.org:su-128394DiVA: diva2:914763