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
Imports 
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

Idea

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.

Definition

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)
  where

  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)
  where

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

Properties

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)
  where

  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}
  where

  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 =
    is-equiv-is-contr
      ( map-sequential-diagram A n)
      ( contrs n)
      ( contrs (succ-ℕ n))

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