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