Homotopy limits in type theory
classification
🧮 math.LO
cs.LOmath.CT
keywords
homotopylimitsapproachtheorytypeassistantcategorieschallenges
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.