Change search
ReferencesLink to record
Permanent link

Direct link
Homotopy limits in type theory
Department of Philosophy and Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh, Pennsylvania, U.S.A..ORCID iD: 0000-0002-4602-9779
Department of Mathematics, University of Pittsburgh, Pennsylvania, U.S.A..
Institute for Advanced Study, Princeton, New Jersey, U.S.A..ORCID iD: 0000-0003-1390-2970
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
Abstract [en]

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.
Keyword [en]
homotopy type theory, homotopy limits, pullbacks, formalisation, proof assistants
National Category
Algebra and Logic
Research subject
Mathematical Logic
URN: urn:nbn:se:su:diva-128394DOI: 10.1017/S0960129514000498OAI: diva2:914763
Available from: 2016-03-25 Created: 2016-03-25 Last updated: 2016-04-04Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textarXiv:1304.0860

Search in DiVA

By author/editor
Avigad, JeremyLumsdaine, Peter LeFanu
In the same journal
Mathematical Structures in Computer Science
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 33 hits
ReferencesLink to record
Permanent link

Direct link