Sequential diagrams

Content created by Fredrik Bakke, Vojtěch Štěpančík and Egbert Rijke.

Created on 2023-10-23.
Last modified on 2024-05-23.

module synthetic-homotopy-theory.sequential-diagrams where
open import elementary-number-theory.natural-numbers

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.universe-levels


A sequential diagram (A, a) is a sequence of types A : ℕ → 𝒰 over the natural numbers, equipped with a family of maps aₙ : Aₙ → Aₙ₊₁ for all n.

They can be represented by diagrams

     a₀      a₁      a₂
 A₀ ---> A₁ ---> A₂ ---> ⋯

extending infinitely to the right.

Sequential diagrams are dual to inverse sequential diagrams, and are also sometimes called cotowers.


sequential-diagram : (l : Level)  UU (lsuc l)
sequential-diagram l = Σ (  UU l)  A  (n : )  A n  A (succ-ℕ n))

module _
  { l : Level} (A : sequential-diagram l)

  family-sequential-diagram :   UU l
  family-sequential-diagram = pr1 A

  map-sequential-diagram :
    (n : )  family-sequential-diagram n  family-sequential-diagram (succ-ℕ n)
  map-sequential-diagram = pr2 A
module _
  { l : Level} (X : UU l)

  constant-sequential-diagram : sequential-diagram l
  pr1 constant-sequential-diagram _ = X
  pr2 constant-sequential-diagram _ x = x


The identity type of sequential diagrams is characterized in the file about equivalences of sequential diagrams.

Postcomposition sequential diagrams

Given a sequential diagram A and a type X there is a sequential diagram X → A defined by levelwise postcomposition.

           (f₀ ∘ -)          (f₁ ∘ -)          (f₂ ∘ -)
  (X → A₀) -------> (X → A₁) -------> (X → A₂) -------> (X → A₃) -------> ⋯
module _
  {l1 l2 : Level} (X : UU l1) (A : sequential-diagram l2)

  postcomp-sequential-diagram : sequential-diagram (l1  l2)
  pr1 postcomp-sequential-diagram n = X  family-sequential-diagram A n
  pr2 postcomp-sequential-diagram n g x = map-sequential-diagram A n (g x)

A sequential diagram of contractible types consists of equivalences

This is an easy corollary of the fact that every map between contractible types is an equivalence.

module _
  {l1 : Level} {A : sequential-diagram l1}

  is-equiv-sequential-diagram-is-contr :
    ((n : )  is-contr (family-sequential-diagram A n)) 
    (n : )  is-equiv (map-sequential-diagram A n)
  is-equiv-sequential-diagram-is-contr contrs n =
      ( map-sequential-diagram A n)
      ( contrs n)
      ( contrs (succ-ℕ n))


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