Sequential Colimits in Homotopy Type Theory
| Autor: | Egbert Rijke, Floris van Doorn, Kristina Sojakova |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Class (set theory)
Pure mathematics Conjecture Homotopy 010102 general mathematics 0102 computer and information sciences Mathematical proof Mathematics::Algebraic Topology 01 natural sciences Interpretation (model theory) Development (topology) 010201 computation theory & mathematics Mathematics::Category Theory Homotopy type theory 0101 mathematics Commutative property Mathematics |
| Zdroj: | LICS |
| Popis: | Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|