Sequential Colimits in Homotopy Type Theory
Content created by Vojtěch Štěpančík.
Created on 2024-06-06.
Last modified on 2024-06-06.
This file collects references to formalization of constructions and theorems from [SvDR20].
module literature.sequential-colimits-in-homotopy-type-theory where
2 Homotopy Type Theory
The second section introduces basic notions from homotopy type theory, which we import below for completeness.
open import foundation.universe-levels using ( UU ) open import foundation.identity-types using ( Id -- "path" ; refl -- "constant path" ; inv -- "inverse path" ; concat -- "concatenation of paths" ; assoc -- "associativity of concatenation" ) open import foundation.action-on-identifications-functions using ( ap -- "functions respect paths" ) open import foundation.homotopies using ( _~_ -- "homotopy" ) open import foundation.equivalences using ( equiv -- "equivalence" ) open import foundation.univalence using ( univalence -- "the univalence axiom" ; map-eq -- "function p̅ associated to a path" ) open import foundation.function-extensionality using ( funext -- "the function extensionality axiom" ) open import foundation.fibers-of-maps using ( fiber -- "the homotopy fiber of a function" ) open import foundation.transport-along-identifications using ( tr -- "transport" ) open import foundation.action-on-identifications-dependent-functions using ( apd -- "dependent functions respect paths" ) open import foundation.truncated-types using ( is-trunc -- "`n`-truncated types" ) open import foundation.truncations using ( trunc -- "the `n`-truncation of a type" ; unit-trunc -- "the unit map into a type's `n`-truncation" ; is-truncation-trunc -- "precomposing by the unit is an equivalence" ) open import foundation.connected-types using ( is-connected -- "`n`-connected types" ) open import foundation.truncated-maps using ( is-trunc-map -- "`n`-truncated functions" ) open import foundation.connected-maps using ( is-connected-map -- "`n`-connected functions" )
3 Sequences and Sequential Colimits
The third section defines categorical properties of sequences (which are called sequential diagrams in agda-unimath) and the colimiting functor. It concludes by defining shifts of sequences, showing that they induce equivalences on sequential colimits, and defines lifts of elements in a sequential diagram.
Definition 3.1. Sequences.
open import synthetic-homotopy-theory.sequential-diagrams using ( sequential-diagram )
Definition 3.2. Sequential colimits and their induction and recursion principles.
Induction and recursion are given by the dependent and non-dependent universal
properties, respectively. Since we work in a setting without computational
higher inductive types, the maps induced by induction and recursion only compute
up to a path, even on points. Our homotopies in the definitions of cocones go
from left to right (i.e. iₙ ~ iₙ₊₁ ∘ aₙ
), instead of right to left.
Our formalization works with sequential colimits specified by a cocone with a universal property, and results about the standard construction of colimits are obtained by specialization to the canonical cocone.
open import synthetic-homotopy-theory.sequential-colimits using ( standard-sequential-colimit -- the canonical colimit type ; map-cocone-standard-sequential-colimit -- "the canonical injection" ; coherence-cocone-standard-sequential-colimit -- "the glue" ; dup-standard-sequential-colimit -- "the induction principle" ; up-standard-sequential-colimit -- "the recursion principle" )
Lemma 3.3. Uniqueness property of the sequential colimit.
The data of a homotopy between two functions out of the standard sequential
colimit is specified by the type htpy-out-of-standard-sequential-colimit
,
which we can then turn into a proper homotopy.
open import synthetic-homotopy-theory.sequential-colimits using ( htpy-out-of-standard-sequential-colimit -- data of a homotopy ; htpy-htpy-out-of-standard-sequential-colimit -- "data of a homotopy induces a homotopy" )
Definition 3.4. Natural transformations and natural equivalences between sequential diagrams.
We call natural transformations morphisms of sequential diagrams, and natural equivalences equivalences of sequential diagrams.
open import synthetic-homotopy-theory.morphisms-sequential-diagrams using ( hom-sequential-diagram -- "natural transformation" ; id-hom-sequential-diagram -- "identity natural transformation" ; comp-hom-sequential-diagram -- "composition of natural transformations" ) open import synthetic-homotopy-theory.equivalences-sequential-diagrams using ( equiv-sequential-diagram -- "natural equivalence" )
Lemma 3.5. Functoriality of the Sequential Colimit.
open import synthetic-homotopy-theory.functoriality-sequential-colimits using ( map-hom-standard-sequential-colimit -- "a natural transformation induces a map" ; preserves-id-map-hom-standard-sequential-colimit -- "1∞ ~ id(A∞)" ; preserves-comp-map-hom-standard-sequential-colimit -- "(σ ∘ τ)∞ ~ σ∞ ∘ τ∞" ; htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram -- "homotopy of natural transformations induces a homotopy" ; equiv-equiv-standard-sequential-colimit -- "if τ is an equivalence, then τ∞ is an equivalence" )
Lemma 3.6. Dropping a head of a sequential diagram preserves the sequential colimit.
Lemma 3.7. Dropping finitely many vertices from the beginning of a sequential diagram preserves the sequential colimit.
Denoting by A[k]
the sequence A
with the first k
vertices removed, we show
that the type of cocones under A[k]
is equivalent to the type of cocones under
A
, and conclude that any sequential colimit of A[k]
also has the universal
property of a colimit of A
. Specializing to the standard sequential colimit,
we get and equivalence A[k]∞ ≃ A∞
.
open import synthetic-homotopy-theory.shifts-sequential-diagrams using ( compute-sequential-colimit-shift-sequential-diagram -- "A[k]∞ ≃ A∞" ) compute-sequential-colimit-shift-sequential-diagram-once = λ l (A : sequential-diagram l) → compute-sequential-colimit-shift-sequential-diagram A 1
4 Fibered Sequences
The fourth section defines fibered sequences, which we call dependent sequential diagrams in the library. It introduces the "Σ of a sequence", which we call the total sequential diagram, and asks the main question about the interplay between Σ and taking the colimit.
The paper defines fibered sequences as a family over the total space
B : Σ ℕ A → 𝒰
, but we use the curried definition B : (n : ℕ) → A(n) → 𝒰
.
Definition 4.1. Fibered sequences. Equifibered sequences.
open import synthetic-homotopy-theory.dependent-sequential-diagrams using ( dependent-sequential-diagram -- "A sequence (B, b) fibered over (A, a)" )
Lemma 4.2. The type of families over a colimit is equivalent to the type of equifibered sequences.
This property is also called the descent property of sequential colimits, because it characterizes families over a sequential colimit.
-- TODO
Definition 4.3. Σ of a fibered sequence.
open import synthetic-homotopy-theory.total-sequential-diagrams using ( total-sequential-diagram -- "Σ (A, a) (B, b)" ; pr1-total-sequential-diagram -- "the canonical projection" )
Construction. The equifibered family associated to a fibered sequence.
-- TODO
5 Colimits and Sums
Theorem 5.1. Interaction between colim
and Σ
.
-- TODO
6 Induction on the Sum of Sequential Colimits
-- TODO
7 Applications of the Main Theorem
Lemma 7.1. TODO description.
-- TODO
Lemma 7.2. Colimit of the terminal sequential diagram is contractible.
-- TODO
Lemma 7.3. Encode-decode.
This principle is called the Fundamental theorem of identity types in the library.
open import foundation.fundamental-theorem-of-identity-types using ( fundamental-theorem-id)
Lemma 7.4. Characterization of path spaces of images of the canonical maps into the sequential colimit.
-- TODO
Corollary 7.5. The loop space of a sequential colimit is the sequential colimit of loop spaces.
-- TODO
Corollary 7.6. For a morphism of sequential diagrams, the fibers of the induced map between sequential colimits are characterized as sequential colimits of the fibers.
-- TODO
Corollary 7.7.1. If each type in a sequential diagram is k
-truncated, then
the colimit is k
-truncated.
-- TODO
Corollary 7.7.2. The k
-truncation of a sequential colimit is the
sequential colimit of k
-truncations.
-- TODO
Corollary 7.7.3. If each type in a sequential diagram is k
-connected, then
the colimit is k
-connected.
-- TODO
Corollary 7.7.4. If each component of a morphism between sequential diagrams
is k
-truncated/k
-connected, then the induced map of sequential colimits is
k
-truncated/k
-connected.
-- TODO
Corollary 7.7.5. If each map in a sequential diagram is
k
-truncated/k
-connected, then the first injection into the colimit is
k
-truncated/k
-connected.
-- TODO
References
- [SvDR20]
- Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, 845–858. Association for Computing Machinery, 07 2020. doi:10.1145/3373718.3394801.
Recent changes
- 2024-06-06. Vojtěch Štěpančík. Various website improvements (#1154).