Cocones under 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.cocones-under-sequential-diagrams where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.binary-homotopies
open import foundation.commuting-squares-of-homotopies
open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.postcomposition-functions
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import synthetic-homotopy-theory.dependent-sequential-diagrams
open import synthetic-homotopy-theory.equifibered-sequential-diagrams
open import synthetic-homotopy-theory.sequential-diagrams

Idea

A cocone under a sequential diagram (A, a) with codomain X : 𝒰 consists of a family of maps iₙ : A n → C and a family of homotopies Hₙ asserting that the triangles

       aₙ
 Aₙ ------> Aₙ₊₁
   \       /
    \     /
  iₙ \   / iₙ₊₁
      ∨ ∨
       X

commute.

Definitions

Cocones under sequential diagrams

module _
  { l1 l2 : Level} (A : sequential-diagram l1) (X : UU l2)
  where

  cocone-sequential-diagram : UU (l1 ⊔ l2)
  cocone-sequential-diagram =
    Σ ( ( n : ℕ) → family-sequential-diagram A n → X)
      ( λ i →
        ( n : ℕ) →
        coherence-triangle-maps
          ( i n)
          ( i (succ-ℕ n))
          ( map-sequential-diagram A n))

Components of cocones under sequential diagrams

module _
  { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  ( c : cocone-sequential-diagram A X)
  where

  map-cocone-sequential-diagram : (n : ℕ) → family-sequential-diagram A n → X
  map-cocone-sequential-diagram = pr1 c

  coherence-cocone-sequential-diagram :
    ( n : ℕ) →
    coherence-triangle-maps
      ( map-cocone-sequential-diagram n)
      ( map-cocone-sequential-diagram (succ-ℕ n))
      ( map-sequential-diagram A n)
  coherence-cocone-sequential-diagram = pr2 c

  first-map-cocone-sequential-diagram : family-sequential-diagram A 0 → X
  first-map-cocone-sequential-diagram = map-cocone-sequential-diagram 0

Homotopies of cocones under a sequential diagram

A homotopy between two cocones (X, i, H) and (X, j, L) with the same vertex consists of a sequence of homotopies Kₙ : iₙ ~ jₙ and a coherence datum filling the “pinched cylinder” with the faces Kₙ, Hₙ, Lₙ and Kₙ₊₁.

The coherence datum may be better understood by viewing a cocone as a morphism from (A, a) to the constant cocone (n ↦ X, n ↦ id) — the two types are strictly equal. Then a homotopy of cocones is a regular homotopy of morphisms of sequential diagrams.

module _
  { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  ( c c' : cocone-sequential-diagram A X)
  where

  coherence-htpy-cocone-sequential-diagram :
    ( (n : ℕ) →
      map-cocone-sequential-diagram c n ~ map-cocone-sequential-diagram c' n) →
    UU (l1 ⊔ l2)
  coherence-htpy-cocone-sequential-diagram K =
    ( n : ℕ) →
    coherence-square-homotopies
      ( K n)
      ( coherence-cocone-sequential-diagram c n)
      ( coherence-cocone-sequential-diagram c' n)
      ( K (succ-ℕ n) ·r map-sequential-diagram A n)

  htpy-cocone-sequential-diagram :
    UU (l1 ⊔ l2)
  htpy-cocone-sequential-diagram =
    Σ ( ( n : ℕ) →
        ( map-cocone-sequential-diagram c n) ~
        ( map-cocone-sequential-diagram c' n))
      ( coherence-htpy-cocone-sequential-diagram)

Components of a homotopy of cocones under a sequential diagram

module _
  { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  { c c' : cocone-sequential-diagram A X}
  ( H : htpy-cocone-sequential-diagram c c')
  where

  htpy-htpy-cocone-sequential-diagram :
    ( n : ℕ) →
    ( map-cocone-sequential-diagram c n) ~
    ( map-cocone-sequential-diagram c' n)
  htpy-htpy-cocone-sequential-diagram = pr1 H

  coherence-htpy-htpy-cocone-sequential-diagram :
    coherence-htpy-cocone-sequential-diagram c c'
      ( htpy-htpy-cocone-sequential-diagram)
  coherence-htpy-htpy-cocone-sequential-diagram = pr2 H

Inverting homotopies of cocones under sequential diagrams

module _
  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  {c c' : cocone-sequential-diagram A X}
  (H : htpy-cocone-sequential-diagram c c')
  where

  inv-htpy-cocone-sequential-diagram : htpy-cocone-sequential-diagram c' c
  pr1 inv-htpy-cocone-sequential-diagram n =
    inv-htpy (htpy-htpy-cocone-sequential-diagram H n)
  pr2 inv-htpy-cocone-sequential-diagram n =
    horizontal-inv-coherence-square-homotopies
      ( htpy-htpy-cocone-sequential-diagram H n)
      ( coherence-cocone-sequential-diagram c n)
      ( coherence-cocone-sequential-diagram c' n)
      ( ( htpy-htpy-cocone-sequential-diagram H (succ-ℕ n)) ·r
        ( map-sequential-diagram A n))
      ( coherence-htpy-htpy-cocone-sequential-diagram H n)

Concatenation of homotopies of cocones under a sequential diagram

module _
  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  {c c' c'' : cocone-sequential-diagram A X}
  (H : htpy-cocone-sequential-diagram c c')
  (K : htpy-cocone-sequential-diagram c' c'')
  where

  concat-htpy-cocone-sequential-diagram : htpy-cocone-sequential-diagram c c''
  pr1 concat-htpy-cocone-sequential-diagram n =
    ( htpy-htpy-cocone-sequential-diagram H n) ∙h
    ( htpy-htpy-cocone-sequential-diagram K n)
  pr2 concat-htpy-cocone-sequential-diagram n =
    horizontal-pasting-coherence-square-homotopies
      ( htpy-htpy-cocone-sequential-diagram H n)
      ( htpy-htpy-cocone-sequential-diagram K n)
      ( coherence-cocone-sequential-diagram c n)
      ( coherence-cocone-sequential-diagram c' n)
      ( coherence-cocone-sequential-diagram c'' n)
      ( ( htpy-htpy-cocone-sequential-diagram H (succ-ℕ n)) ·r
        ( map-sequential-diagram A n))
      ( ( htpy-htpy-cocone-sequential-diagram K (succ-ℕ n)) ·r
        ( map-sequential-diagram A n))
      ( coherence-htpy-htpy-cocone-sequential-diagram H n)
      ( coherence-htpy-htpy-cocone-sequential-diagram K n)

Postcomposing cocones under a sequential diagram with a map

Given a cocone c with vertex X under (A, a) and a map f : X → Y, we may extend c to a cocone with vertex Y.

module _
  { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
  ( c : cocone-sequential-diagram A X)
  where

  cocone-map-sequential-diagram :
    { l : Level} {Y : UU l} →
    ( X → Y) → cocone-sequential-diagram A Y
  pr1 (cocone-map-sequential-diagram f) n =
    f ∘ map-cocone-sequential-diagram c n
  pr2 (cocone-map-sequential-diagram f) n =
    f ·l (coherence-cocone-sequential-diagram c n)

Postcomposition cocones under postcomposition sequential diagrams

module _
  { l1 l2 l3 : Level} (X : UU l1) (A : sequential-diagram l2) {Y : UU l3}
  ( c : cocone-sequential-diagram A Y)
  where

  cocone-postcomp-sequential-diagram :
    cocone-sequential-diagram (postcomp-sequential-diagram X A) (X → Y)
  pr1 cocone-postcomp-sequential-diagram n g x =
    map-cocone-sequential-diagram c n (g x)
  pr2 cocone-postcomp-sequential-diagram n g =
    htpy-postcomp X (coherence-cocone-sequential-diagram c n) g

Equifibered sequential diagrams induced by type families over cocones under sequential diagrams

Given a sequential diagram (A, a) and a cocone c under it with vertex X, and a type family P : X → 𝒰, we may compose them together to get

       aₙ
 Aₙ ------> Aₙ₊₁
   \       /
    \  Hₙ /
  iₙ \   / iₙ₊₁
      ∨ ∨
       X
       | P
       ∨
       𝒰 ,

which gives us a collection of type families Pₙ : Aₙ → 𝒰, and a collection of equivalences Pₙ a ≃ Pₙ₊₁ (aₙ a) induced by transporting in P along Hₙ. This data comes together to form an equifibered sequential diagram over A.

module _
  {l1 l2 l3 : Level} {A : sequential-diagram l1}
  {X : UU l2} (c : cocone-sequential-diagram A X)
  (P : X → UU l3)
  where

  equifibered-sequential-diagram-family-cocone :
    equifibered-sequential-diagram A l3
  pr1 equifibered-sequential-diagram-family-cocone n a =
    P (map-cocone-sequential-diagram c n a)
  pr2 equifibered-sequential-diagram-family-cocone n a =
    equiv-tr P (coherence-cocone-sequential-diagram c n a)

  dependent-sequential-diagram-family-cocone : dependent-sequential-diagram A l3
  dependent-sequential-diagram-family-cocone =
    dependent-sequential-diagram-equifibered-sequential-diagram
      ( equifibered-sequential-diagram-family-cocone)

  is-equifibered-dependent-sequential-diagram-family-cocone :
    is-equifibered-dependent-sequential-diagram
      ( dependent-sequential-diagram-family-cocone)
  is-equifibered-dependent-sequential-diagram-family-cocone =
    is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram
      ( equifibered-sequential-diagram-family-cocone)

Properties

Characterization of identity types of cocones under sequential diagrams

Equality of cocones with the same vertex is captured by a homotopy between them.

module _
  { l1 l2 : Level} (A : sequential-diagram l1) {X : UU l2}
  ( c : cocone-sequential-diagram A X)
  where

  refl-htpy-cocone-sequential-diagram :
    htpy-cocone-sequential-diagram c c
  pr1 refl-htpy-cocone-sequential-diagram n = refl-htpy
  pr2 refl-htpy-cocone-sequential-diagram n = right-unit-htpy

  htpy-eq-cocone-sequential-diagram :
    ( c' : cocone-sequential-diagram A X) → ( c ＝ c') →
    htpy-cocone-sequential-diagram c c'
  htpy-eq-cocone-sequential-diagram .c refl =
    refl-htpy-cocone-sequential-diagram

  abstract
    is-torsorial-htpy-cocone-sequential-diagram :
      is-torsorial (htpy-cocone-sequential-diagram c)
    is-torsorial-htpy-cocone-sequential-diagram =
      is-torsorial-Eq-structure
        ( is-torsorial-binary-htpy (map-cocone-sequential-diagram c))
        ( ( map-cocone-sequential-diagram c) ,
          ( ev-pair refl-htpy))
        ( is-torsorial-binary-htpy
          ( λ n → coherence-cocone-sequential-diagram c n ∙h refl-htpy))

    is-equiv-htpy-eq-cocone-sequential-diagram :
      ( c' : cocone-sequential-diagram A X) →
      is-equiv (htpy-eq-cocone-sequential-diagram c')
    is-equiv-htpy-eq-cocone-sequential-diagram =
      fundamental-theorem-id
        ( is-torsorial-htpy-cocone-sequential-diagram)
        ( htpy-eq-cocone-sequential-diagram)

  extensionality-cocone-sequential-diagram :
    ( c' : cocone-sequential-diagram A X) →
    ( c ＝ c') ≃ htpy-cocone-sequential-diagram c c'
  pr1 (extensionality-cocone-sequential-diagram c') =
    htpy-eq-cocone-sequential-diagram c'
  pr2 (extensionality-cocone-sequential-diagram c') =
    is-equiv-htpy-eq-cocone-sequential-diagram c'

  eq-htpy-cocone-sequential-diagram :
    ( c' : cocone-sequential-diagram A X) →
    htpy-cocone-sequential-diagram c c' →
    c ＝ c'
  eq-htpy-cocone-sequential-diagram c' =
    map-inv-equiv (extensionality-cocone-sequential-diagram c')

Postcomposing a cocone under a sequential diagram by identity is the identity

module _
  { l1 l2 : Level} (A : sequential-diagram l1) {X : UU l2}
  ( c : cocone-sequential-diagram A X)
  where

  htpy-cocone-map-id-sequential-diagram :
    htpy-cocone-sequential-diagram (cocone-map-sequential-diagram c id) c
  pr1 htpy-cocone-map-id-sequential-diagram n =
    refl-htpy
  pr2 htpy-cocone-map-id-sequential-diagram n =
    ( right-unit-htpy) ∙h
    ( left-unit-law-left-whisker-comp
      ( coherence-cocone-sequential-diagram c n))

  cocone-map-id-sequential-diagram : cocone-map-sequential-diagram c id ＝ c
  cocone-map-id-sequential-diagram =
    eq-htpy-cocone-sequential-diagram A _ _
      ( htpy-cocone-map-id-sequential-diagram)

Postcomposing cocones under a sequential colimit distributes over function composition

In other words, extending a cocone c with vertex X by the map k ∘ h : X → Z results in the same cocone as first extending by h and then by k.

module _
  { l1 l2 l3 l4 : Level} (A : sequential-diagram l1)
  { X : UU l2} {Y : UU l3} {Z : UU l4}
  ( c : cocone-sequential-diagram A X)
  where

  htpy-cocone-map-comp-sequential-diagram :
    ( h : X → Y) (k : Y → Z) →
    htpy-cocone-sequential-diagram
      ( cocone-map-sequential-diagram c (k ∘ h))
      ( cocone-map-sequential-diagram (cocone-map-sequential-diagram c h) k)
  pr1 (htpy-cocone-map-comp-sequential-diagram h k) n =
    refl-htpy
  pr2 (htpy-cocone-map-comp-sequential-diagram h k) n =
    ( right-unit-htpy) ∙h
    ( inv-preserves-comp-left-whisker-comp k h
      ( coherence-cocone-sequential-diagram c n))

  cocone-map-comp-sequential-diagram :
    ( h : X → Y) (k : Y → Z) →
    cocone-map-sequential-diagram c (k ∘ h) ＝
    cocone-map-sequential-diagram (cocone-map-sequential-diagram c h) k
  cocone-map-comp-sequential-diagram h k =
    eq-htpy-cocone-sequential-diagram A
      ( cocone-map-sequential-diagram c (k ∘ h))
      ( cocone-map-sequential-diagram (cocone-map-sequential-diagram c h) k)
      ( htpy-cocone-map-comp-sequential-diagram h k)

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