Dependent 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-01-16.

module synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams where
Imports
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.binary-homotopies
open import foundation.commuting-triangles-of-maps
open import foundation.constant-type-families
open import foundation.dependent-homotopies
open import foundation.dependent-identifications
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-types
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 synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.dependent-coforks
open import synthetic-homotopy-theory.sequential-diagrams

Idea

Given a sequential diagram (A, a), a cocone c with vertex X under it, and a type family P : X → 𝓤, we may construct dependent cocones on P over c.

A dependent cocone under a sequential diagram on P over c ≐ (X, i, H) consists of a sequence of dependent maps i'ₙ : (x : Aₙ) → P (iₙ x) and a sequence of dependent homotopies H'ₙ : i'ₙ ~ i'ₙ₊₁ ∘ aₙ over H.

Definitions

Dependent cocones under sequential diagrams

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

  dependent-cocone-sequential-diagram : UU (l1  l3)
  dependent-cocone-sequential-diagram =
    Σ ( ( n : ) (a : family-sequential-diagram A n) 
        P (map-cocone-sequential-diagram c n a))
      ( λ i 
        ( n : ) 
        dependent-homotopy  _  P)
          ( coherence-cocone-sequential-diagram c n)
          ( i n)
          ( i (succ-ℕ n)  map-sequential-diagram A n))

Components of dependent cocones under sequential diagrams

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

  map-dependent-cocone-sequential-diagram :
    ( n : ) (a : family-sequential-diagram A n) 
    P (map-cocone-sequential-diagram c n a)
  map-dependent-cocone-sequential-diagram = pr1 d

  coherence-triangle-dependent-cocone-sequential-diagram :
    ( n : )  (a : family-sequential-diagram A n) 
    dependent-identification P
      ( coherence-cocone-sequential-diagram c n a)
      ( map-dependent-cocone-sequential-diagram n a)
      ( map-dependent-cocone-sequential-diagram
        ( succ-ℕ n)
        ( map-sequential-diagram A n a))
  coherence-triangle-dependent-cocone-sequential-diagram = pr2 d

Homotopies of dependent cocones under sequential diagrams

A homotopy of dependent cocones (P, i', H') and (P, j', L') consists of a sequence of homotopies Kₙ : i'ₙ ~ j'ₙ and a coherence datum.

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

  coherence-htpy-dependent-cocone-sequential-diagram :
    ( d d' : dependent-cocone-sequential-diagram c P) 
    ( K :
      ( n : ) 
      ( map-dependent-cocone-sequential-diagram P d n) ~
      ( map-dependent-cocone-sequential-diagram P d' n)) 
    UU (l1  l3)
  coherence-htpy-dependent-cocone-sequential-diagram d d' K =
    ( n : ) (a : family-sequential-diagram A n) 
    ( ( coherence-triangle-dependent-cocone-sequential-diagram P d n a) 
      ( K (succ-ℕ n) (map-sequential-diagram A n a))) 
    ( ( ap
        ( tr P (coherence-cocone-sequential-diagram c n a))
        ( K n a)) 
      ( coherence-triangle-dependent-cocone-sequential-diagram P d' n a))

  htpy-dependent-cocone-sequential-diagram :
    ( d d' : dependent-cocone-sequential-diagram c P) 
    UU (l1  l3)
  htpy-dependent-cocone-sequential-diagram d d' =
    Σ ( ( n : ) 
        ( map-dependent-cocone-sequential-diagram P d n) ~
        ( map-dependent-cocone-sequential-diagram P d' n))
      ( coherence-htpy-dependent-cocone-sequential-diagram d d')

Components of homotopies of dependent cocones under sequential diagrams

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

  htpy-htpy-dependent-cocone-sequential-diagram :
    ( n : ) 
    ( map-dependent-cocone-sequential-diagram P d n) ~
    ( map-dependent-cocone-sequential-diagram P d' n)
  htpy-htpy-dependent-cocone-sequential-diagram = pr1 H

  coherence-htpy-htpy-dependent-cocone-sequential-diagram :
    coherence-htpy-dependent-cocone-sequential-diagram P d d'
      ( htpy-htpy-dependent-cocone-sequential-diagram)
  coherence-htpy-htpy-dependent-cocone-sequential-diagram = pr2 H

Obtaining dependent cocones under sequential diagrams by postcomposing cocones under sequential diagrams with dependent maps

Given a cocone c with vertex X, and a dependent map h : (x : X) → P x, we may extend c to a dependent cocone on P over c.

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

  dependent-cocone-map-sequential-diagram :
    { l : Level} (P : X  UU l) 
    ( (x : X)  P x)  dependent-cocone-sequential-diagram c P
  pr1 (dependent-cocone-map-sequential-diagram P h) n =
    h  map-cocone-sequential-diagram c n
  pr2 (dependent-cocone-map-sequential-diagram P h) n =
    apd h  coherence-cocone-sequential-diagram c n

Properties

Characterization of identity types of dependent cocones under sequential diagrams

Equality of dependent cocones is captured by a homotopy between them.

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

  refl-htpy-dependent-cocone-sequential-diagram :
    ( d : dependent-cocone-sequential-diagram c P) 
    htpy-dependent-cocone-sequential-diagram P d d
  pr1 (refl-htpy-dependent-cocone-sequential-diagram d) n = refl-htpy
  pr2 (refl-htpy-dependent-cocone-sequential-diagram d) n = right-unit-htpy

  htpy-eq-dependent-cocone-sequential-diagram :
    ( d d' : dependent-cocone-sequential-diagram c P) 
    ( d  d')  htpy-dependent-cocone-sequential-diagram P d d'
  htpy-eq-dependent-cocone-sequential-diagram d .d refl =
    refl-htpy-dependent-cocone-sequential-diagram d

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

    is-equiv-htpy-eq-dependent-cocone-sequential-diagram :
      ( d d' : dependent-cocone-sequential-diagram c P) 
      is-equiv (htpy-eq-dependent-cocone-sequential-diagram d d')
    is-equiv-htpy-eq-dependent-cocone-sequential-diagram d =
      fundamental-theorem-id
        ( is-torsorial-htpy-dependent-cocone-sequential-diagram d)
        ( htpy-eq-dependent-cocone-sequential-diagram d)

  extensionality-dependent-cocone-sequential-diagram :
    ( d d' : dependent-cocone-sequential-diagram c P) 
    ( d  d')  htpy-dependent-cocone-sequential-diagram P d d'
  pr1 (extensionality-dependent-cocone-sequential-diagram d d') =
    htpy-eq-dependent-cocone-sequential-diagram d d'
  pr2 (extensionality-dependent-cocone-sequential-diagram d d') =
    is-equiv-htpy-eq-dependent-cocone-sequential-diagram d d'

  eq-htpy-dependent-cocone-sequential-diagram :
    ( d d' : dependent-cocone-sequential-diagram c P) 
    htpy-dependent-cocone-sequential-diagram P d d'  (d  d')
  eq-htpy-dependent-cocone-sequential-diagram d d' =
    map-inv-equiv (extensionality-dependent-cocone-sequential-diagram d d')

Dependent cocones under sequential diagrams on fiberwise constant type families are equivalent to regular cocones under sequential diagrams

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

  compute-dependent-cocone-sequential-diagram-constant-family :
    ( dependent-cocone-sequential-diagram c  _  Y)) 
    ( cocone-sequential-diagram A Y)
  compute-dependent-cocone-sequential-diagram-constant-family =
    equiv-tot
      ( λ i 
        equiv-Π-equiv-family
          ( λ n 
            equiv-Π-equiv-family
              ( λ a 
                equiv-concat
                  ( inv
                    ( tr-constant-type-family
                      ( coherence-cocone-sequential-diagram c n a)
                      ( i n a)))
                  ( i (succ-ℕ n) (map-sequential-diagram A n a)))))

  map-compute-dependent-cocone-sequential-diagram-constant-family :
    dependent-cocone-sequential-diagram c  _  Y) 
    cocone-sequential-diagram A Y
  map-compute-dependent-cocone-sequential-diagram-constant-family =
    map-equiv compute-dependent-cocone-sequential-diagram-constant-family

  triangle-compute-dependent-cocone-sequential-diagram-constant-family :
    coherence-triangle-maps
      ( cocone-map-sequential-diagram c)
      ( map-compute-dependent-cocone-sequential-diagram-constant-family)
      ( dependent-cocone-map-sequential-diagram c  _  Y))
  triangle-compute-dependent-cocone-sequential-diagram-constant-family h =
    eq-htpy-cocone-sequential-diagram A
      ( cocone-map-sequential-diagram c h)
      ( map-compute-dependent-cocone-sequential-diagram-constant-family
        ( dependent-cocone-map-sequential-diagram c  _  Y) h))
      ( ( ev-pair refl-htpy) ,
        ( λ n a 
          right-unit 
          left-transpose-eq-concat _ _ _
            ( inv
              ( apd-constant-type-family h
                ( coherence-cocone-sequential-diagram c n a)))))

Dependent cocones under sequential diagrams are special cases of dependent coforks

Just like with the regular cocones under sequential diagrams, we have an analogous correspondence between dependent cocones over a cocone c and dependent coforks over the cofork corresponding to c.

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

  module _
    { l3 : Level} (P : X  UU l3)
    where

    dependent-cocone-sequential-diagram-dependent-cofork :
      dependent-cofork
        ( bottom-map-cofork-cocone-sequential-diagram A)
        ( top-map-cofork-cocone-sequential-diagram A)
        ( cofork-cocone-sequential-diagram A c)
        ( P) 
      dependent-cocone-sequential-diagram c P
    pr1 (dependent-cocone-sequential-diagram-dependent-cofork e) =
      ev-pair
        ( map-dependent-cofork
          ( bottom-map-cofork-cocone-sequential-diagram A)
          ( top-map-cofork-cocone-sequential-diagram A)
          ( P)
          ( e))
    pr2 (dependent-cocone-sequential-diagram-dependent-cofork e) =
      ev-pair
        ( coherence-dependent-cofork
          ( bottom-map-cofork-cocone-sequential-diagram A)
          ( top-map-cofork-cocone-sequential-diagram A)
          ( P)
          ( e))

    dependent-cofork-dependent-cocone-sequential-diagram :
      dependent-cocone-sequential-diagram c P 
      dependent-cofork
        ( bottom-map-cofork-cocone-sequential-diagram A)
        ( top-map-cofork-cocone-sequential-diagram A)
        ( cofork-cocone-sequential-diagram A c)
        ( P)
    pr1 (dependent-cofork-dependent-cocone-sequential-diagram d) =
      ind-Σ (map-dependent-cocone-sequential-diagram P d)
    pr2 (dependent-cofork-dependent-cocone-sequential-diagram d) =
      ind-Σ (coherence-triangle-dependent-cocone-sequential-diagram P d)

    abstract
      is-section-dependent-cocone-sequential-diagram-dependent-cofork :
        ( dependent-cofork-dependent-cocone-sequential-diagram 
          dependent-cocone-sequential-diagram-dependent-cofork) ~
        ( id)
      is-section-dependent-cocone-sequential-diagram-dependent-cofork e =
        eq-htpy-dependent-cofork
          ( bottom-map-cofork-cocone-sequential-diagram A)
          ( top-map-cofork-cocone-sequential-diagram A)
          ( P)
          ( dependent-cofork-dependent-cocone-sequential-diagram
            ( dependent-cocone-sequential-diagram-dependent-cofork e))
          ( e)
          ( refl-htpy , right-unit-htpy)

      is-retraction-dependent-cocone-sequential-diagram-dependent-cofork :
        ( dependent-cocone-sequential-diagram-dependent-cofork 
          dependent-cofork-dependent-cocone-sequential-diagram) ~
        ( id)
      is-retraction-dependent-cocone-sequential-diagram-dependent-cofork d =
        eq-htpy-dependent-cocone-sequential-diagram P
          ( dependent-cocone-sequential-diagram-dependent-cofork
            ( dependent-cofork-dependent-cocone-sequential-diagram d))
          ( d)
          ( ev-pair refl-htpy , ev-pair right-unit-htpy)

    is-equiv-dependent-cocone-sequential-diagram-dependent-cofork :
      is-equiv dependent-cocone-sequential-diagram-dependent-cofork
    is-equiv-dependent-cocone-sequential-diagram-dependent-cofork =
      is-equiv-is-invertible
        ( dependent-cofork-dependent-cocone-sequential-diagram)
        ( is-retraction-dependent-cocone-sequential-diagram-dependent-cofork)
        ( is-section-dependent-cocone-sequential-diagram-dependent-cofork)

    equiv-dependent-cocone-sequential-diagram-dependent-cofork :
      dependent-cofork
        ( bottom-map-cofork-cocone-sequential-diagram A)
        ( top-map-cofork-cocone-sequential-diagram A)
        ( cofork-cocone-sequential-diagram A c)
        ( P) 
      dependent-cocone-sequential-diagram c P
    pr1 equiv-dependent-cocone-sequential-diagram-dependent-cofork =
      dependent-cocone-sequential-diagram-dependent-cofork
    pr2 equiv-dependent-cocone-sequential-diagram-dependent-cofork =
      is-equiv-dependent-cocone-sequential-diagram-dependent-cofork

  triangle-dependent-cocone-sequential-diagram-dependent-cofork :
    { l3 : Level} (P : X  UU l3) 
    coherence-triangle-maps
      ( dependent-cocone-map-sequential-diagram c P)
      ( dependent-cocone-sequential-diagram-dependent-cofork P)
      ( dependent-cofork-map
        ( bottom-map-cofork-cocone-sequential-diagram A)
        ( top-map-cofork-cocone-sequential-diagram A)
        ( cofork-cocone-sequential-diagram A c))
  triangle-dependent-cocone-sequential-diagram-dependent-cofork P h =
    eq-htpy-dependent-cocone-sequential-diagram P
      ( dependent-cocone-map-sequential-diagram c P h)
      ( dependent-cocone-sequential-diagram-dependent-cofork P
        ( dependent-cofork-map
          ( bottom-map-cofork-cocone-sequential-diagram A)
          ( top-map-cofork-cocone-sequential-diagram A)
          ( cofork-cocone-sequential-diagram A c)
          ( h)))
      ( ev-pair refl-htpy , ev-pair right-unit-htpy)

Recent changes