# Sequential Colimits in Homotopy Type Theory

Content created by Vojtěch Štěpančík.

Created 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.