Sequential diagrams

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

Created on 2023-10-23.
Last modified on 2024-01-11.

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

open import foundation.dependent-pair-types
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)


  1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '20). Association for Computing Machinery, New York, NY, USA, 845–858, DOI:10.1145

Recent changes