Homotopy limits in type theory
| Autor: | Peter LeFanu Lumsdaine, Krzysztof Kapulkin, Jeremy Avigad |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
FOS: Computer and information sciences
Pure mathematics Computer Science - Logic in Computer Science Homotopy Proof assistant Fibration D.2.4 Mathematics - Category Theory Mathematics - Logic 03B70 55U35 16. Peace & justice Mathematics::Algebraic Topology Computer Science Applications Logic in Computer Science (cs.LO) Mathematics (miscellaneous) Type theory F.4.1 Mathematics::K-Theory and Homology Mathematics::Category Theory Homotopy type theory FOS: Mathematics Category Theory (math.CT) Logic (math.LO) Mathematics |
| DOI: | 10.48550/arxiv.1304.0680 |
| Popis: | 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. Comment: 33 pages; v3: theorem numbering changed since v2 to match journal version |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|