Homotopy limits in type theory
Logic
2019-02-20 v3 Logic in Computer Science
Category Theory
Abstract
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.
Cite
@article{arxiv.1304.0680,
title = {Homotopy limits in type theory},
author = {Jeremy Avigad and Chris Kapulkin and Peter LeFanu Lumsdaine},
journal= {arXiv preprint arXiv:1304.0680},
year = {2019}
}
Comments
33 pages; v3: theorem numbering changed since v2 to match journal version