Dependent cocones under spans

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

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

module synthetic-homotopy-theory.dependent-cocones-under-spans where
Imports 
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-identifications
open import foundation.commuting-squares-of-maps
open import foundation.constant-type-families
open import foundation.contractible-types
open import foundation.dependent-homotopies
open import foundation.dependent-identifications
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.retractions
open import foundation.sections
open import foundation.span-diagrams
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.transport-along-higher-identifications
open import foundation.transport-along-identifications
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.injective-maps

open import synthetic-homotopy-theory.cocones-under-spans

Idea

Consider a span 𝒮 := (A <-- S --> B) and a cocone structure c of 𝒮 into a type X. Furthermore, consider a type family P over X. In this case we may consider dependent cocone structures on P over c.

A dependent cocone d over (i , j , H) on P consists of two dependent functions

  i' : (a : A) → P (i a)
  j' : (b : B) → P (j b)

and a family of dependent identifications

  (s : S) → dependent-identification P (H s) (i' (f s)) (j' (g s)).

Definitions

Dependent cocones

module _
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5)
  where

  dependent-cocone : UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
  dependent-cocone =
    Σ ( (a : A) → P (horizontal-map-cocone f g c a))
      ( λ hA →
        Σ ( (b : B) → P (vertical-map-cocone f g c b))
          ( λ hB →
            (s : S) →
            dependent-identification P
              ( coherence-square-cocone f g c s)
              ( hA (f s))
              ( hB (g s))))

  module _
    (d : dependent-cocone)
    where

    horizontal-map-dependent-cocone :
      (a : A) → P (horizontal-map-cocone f g c a)
    horizontal-map-dependent-cocone = pr1 d

    vertical-map-dependent-cocone :
      (b : B) → P (vertical-map-cocone f g c b)
    vertical-map-dependent-cocone = pr1 (pr2 d)

    coherence-square-dependent-cocone :
      (s : S) →
      dependent-identification P
        ( coherence-square-cocone f g c s)
        ( horizontal-map-dependent-cocone (f s))
        ( vertical-map-dependent-cocone (g s))
    coherence-square-dependent-cocone = pr2 (pr2 d)

dependent-cocone-span-diagram :
  { l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4}
  ( c : cocone-span-diagram 𝒮 X) (P : X → UU l5) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
dependent-cocone-span-diagram {𝒮 = 𝒮} =
  dependent-cocone (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮)

Cocones equipped with dependent cocones

module _
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (P : X → UU l5)
  where

  cocone-with-dependent-cocone : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
  cocone-with-dependent-cocone =
    Σ (cocone f g X) (λ c → dependent-cocone f g c P)

module _
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (P : X → UU l5)
  (c : cocone-with-dependent-cocone f g P)
  where

  cocone-cocone-with-dependent-cocone : cocone f g X
  cocone-cocone-with-dependent-cocone = pr1 c

  horizontal-map-cocone-with-dependent-cocone : A → X
  horizontal-map-cocone-with-dependent-cocone =
    horizontal-map-cocone f g cocone-cocone-with-dependent-cocone

  vertical-map-cocone-with-dependent-cocone : B → X
  vertical-map-cocone-with-dependent-cocone =
    vertical-map-cocone f g cocone-cocone-with-dependent-cocone

  coherence-square-cocone-with-dependent-cocone :
    coherence-square-maps g f
      ( vertical-map-cocone-with-dependent-cocone)
      ( horizontal-map-cocone-with-dependent-cocone)
  coherence-square-cocone-with-dependent-cocone =
    coherence-square-cocone f g cocone-cocone-with-dependent-cocone

  dependent-cocone-cocone-with-dependent-cocone :
    dependent-cocone f g cocone-cocone-with-dependent-cocone P
  dependent-cocone-cocone-with-dependent-cocone = pr2 c

  horizontal-map-dependent-cocone-with-dependent-cocone :
    (a : A) → P (horizontal-map-cocone-with-dependent-cocone a)
  horizontal-map-dependent-cocone-with-dependent-cocone =
    horizontal-map-dependent-cocone f g
      ( cocone-cocone-with-dependent-cocone)
      ( P)
      ( dependent-cocone-cocone-with-dependent-cocone)

  vertical-map-dependent-cocone-with-dependent-cocone :
    (b : B) → P (vertical-map-cocone-with-dependent-cocone b)
  vertical-map-dependent-cocone-with-dependent-cocone =
    vertical-map-dependent-cocone f g
      ( cocone-cocone-with-dependent-cocone)
      ( P)
      ( dependent-cocone-cocone-with-dependent-cocone)

  coherence-square-dependent-cocone-with-dependent-cocone :
    (s : S) →
    dependent-identification P
      ( coherence-square-cocone-with-dependent-cocone s)
      ( horizontal-map-dependent-cocone-with-dependent-cocone (f s))
      ( vertical-map-dependent-cocone-with-dependent-cocone (g s))
  coherence-square-dependent-cocone-with-dependent-cocone =
    coherence-square-dependent-cocone f g
      ( cocone-cocone-with-dependent-cocone)
      ( P)
      ( dependent-cocone-cocone-with-dependent-cocone)

Postcomposing dependent cocones with maps

dependent-cocone-map :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  ( f : S → A) (g : S → B) (c : cocone f g X) (P : X → UU l5) →
  ( (x : X) → P x) → dependent-cocone f g c P
pr1 (dependent-cocone-map f g c P h) a =
  h (horizontal-map-cocone f g c a)
pr1 (pr2 (dependent-cocone-map f g c P h)) b =
  h (vertical-map-cocone f g c b)
pr2 (pr2 (dependent-cocone-map f g c P h)) s =
  apd h (coherence-square-cocone f g c s)

dependent-cocone-map-span-diagram :
  { l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4}
  ( c : cocone-span-diagram 𝒮 X) (P : X → UU l5) →
  ( (x : X) → P x) → dependent-cocone-span-diagram c P
dependent-cocone-map-span-diagram {𝒮 = 𝒮} c =
  dependent-cocone-map (left-map-span-diagram 𝒮) (right-map-span-diagram 𝒮) c

Properties

Characterization of identifications of dependent cocones over a fixed cocone

module _
  {l1 l2 l3 l4 l5 : Level}
  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
  {X : UU l4} (c : cocone f g X)
  (P : X → UU l5) (d : dependent-cocone f g c P)
  where

  coherence-htpy-dependent-cocone :
    ( d' : dependent-cocone f g c P) →
    ( horizontal-map-dependent-cocone f g c P d ~
      horizontal-map-dependent-cocone f g c P d') →
    ( vertical-map-dependent-cocone f g c P d ~
      vertical-map-dependent-cocone f g c P d') →
    UU (l1 ⊔ l5)
  coherence-htpy-dependent-cocone d' K L =
    (s : S) →
    ( ( coherence-square-dependent-cocone f g c P d s) ∙ (L (g s))) ＝
    ( ( ap (tr P (coherence-square-cocone f g c s)) (K (f s))) ∙
      ( coherence-square-dependent-cocone f g c P d' s))

  htpy-dependent-cocone :
    (d' : dependent-cocone f g c P) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
  htpy-dependent-cocone d' =
    Σ ( horizontal-map-dependent-cocone f g c P d ~
        horizontal-map-dependent-cocone f g c P d')
      ( λ K →
        Σ ( vertical-map-dependent-cocone f g c P d ~
            vertical-map-dependent-cocone f g c P d')
          ( coherence-htpy-dependent-cocone d' K))

  refl-htpy-dependent-cocone :
    htpy-dependent-cocone d
  pr1 refl-htpy-dependent-cocone = refl-htpy
  pr1 (pr2 refl-htpy-dependent-cocone) = refl-htpy
  pr2 (pr2 refl-htpy-dependent-cocone) = right-unit-htpy

  htpy-eq-dependent-cocone :
    (d' : dependent-cocone f g c P) → d ＝ d' → htpy-dependent-cocone d'
  htpy-eq-dependent-cocone .d refl = refl-htpy-dependent-cocone

  module _
    (d' : dependent-cocone f g c P)
    (p : d ＝ d')
    where

    horizontal-htpy-eq-dependent-cocone :
      horizontal-map-dependent-cocone f g c P d ~
      horizontal-map-dependent-cocone f g c P d'
    horizontal-htpy-eq-dependent-cocone =
      pr1 (htpy-eq-dependent-cocone d' p)

    vertical-htpy-eq-dependent-cocone :
      vertical-map-dependent-cocone f g c P d ~
      vertical-map-dependent-cocone f g c P d'
    vertical-htpy-eq-dependent-cocone =
      pr1 (pr2 (htpy-eq-dependent-cocone d' p))

    coherence-square-htpy-eq-dependent-cocone :
      coherence-htpy-dependent-cocone d'
        ( horizontal-htpy-eq-dependent-cocone)
        ( vertical-htpy-eq-dependent-cocone)
    coherence-square-htpy-eq-dependent-cocone =
      pr2 (pr2 (htpy-eq-dependent-cocone d' p))

  abstract
    is-torsorial-htpy-dependent-cocone :
      is-torsorial htpy-dependent-cocone
    is-torsorial-htpy-dependent-cocone =
      is-torsorial-Eq-structure
        ( is-torsorial-htpy (horizontal-map-dependent-cocone f g c P d))
        ( horizontal-map-dependent-cocone f g c P d , refl-htpy)
        ( is-torsorial-Eq-structure
          ( is-torsorial-htpy (vertical-map-dependent-cocone f g c P d))
          ( vertical-map-dependent-cocone f g c P d , refl-htpy)
          ( is-contr-equiv
            ( Σ ( (s : S) →
                  dependent-identification P
                    ( coherence-square-cocone f g c s)
                    ( horizontal-map-dependent-cocone f g c P d (f s))
                    ( vertical-map-dependent-cocone f g c P d (g s)))
                ( λ γ → coherence-square-dependent-cocone f g c P d ~ γ))
            ( equiv-tot (equiv-concat-htpy inv-htpy-right-unit-htpy))
            ( is-torsorial-htpy
              ( coherence-square-dependent-cocone f g c P d))))

  abstract
    is-equiv-htpy-eq-dependent-cocone :
      (d' : dependent-cocone f g c P) → is-equiv (htpy-eq-dependent-cocone d')
    is-equiv-htpy-eq-dependent-cocone =
      fundamental-theorem-id
        ( is-torsorial-htpy-dependent-cocone)
        ( htpy-eq-dependent-cocone)

    eq-htpy-dependent-cocone :
      (d' : dependent-cocone f g c P) → htpy-dependent-cocone d' → d ＝ d'
    eq-htpy-dependent-cocone d' =
      map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')

    is-section-eq-htpy-dependent-cocone :
      (d' : dependent-cocone f g c P) →
      ( htpy-eq-dependent-cocone d' ∘ eq-htpy-dependent-cocone d') ~ id
    is-section-eq-htpy-dependent-cocone d' =
      is-section-map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')

    is-retraction-eq-htpy-dependent-cocone :
      (d' : dependent-cocone f g c P) →
      ( eq-htpy-dependent-cocone d' ∘ htpy-eq-dependent-cocone d') ~ id
    is-retraction-eq-htpy-dependent-cocone d' =
      is-retraction-map-inv-is-equiv (is-equiv-htpy-eq-dependent-cocone d')

Dependent homotopies of dependent cocones over homotopies of cocones

module _
  {l1 l2 l3 l4 l5 : Level}
  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
  {X : UU l4}
  where

  coherence-dependent-htpy-dependent-cocone :
    ( c c' : cocone f g X) (H : htpy-cocone f g c c') (P : X → UU l5)
    ( d : dependent-cocone f g c P)
    ( d' : dependent-cocone f g c' P) →
    dependent-homotopy (λ _ → P)
      ( horizontal-htpy-cocone f g c c' H)
      ( horizontal-map-dependent-cocone f g c P d)
      ( horizontal-map-dependent-cocone f g c' P d') →
    dependent-homotopy (λ _ → P)
      ( vertical-htpy-cocone f g c c' H)
      ( vertical-map-dependent-cocone f g c P d)
      ( vertical-map-dependent-cocone f g c' P d') →
    UU (l1 ⊔ l5)
  coherence-dependent-htpy-dependent-cocone c c' H P d d' K L =
    (s : S) →
    dependent-identification² P
      ( coherence-htpy-cocone f g c c' H s)
      ( concat-dependent-identification P
        ( coherence-square-cocone f g c s)
        ( vertical-htpy-cocone f g c c' H (g s))
        ( coherence-square-dependent-cocone f g c P d s)
        ( L (g s)))
      ( concat-dependent-identification P
        ( horizontal-htpy-cocone f g c c' H (f s))
        ( coherence-square-cocone f g c' s)
        ( K (f s))
        ( coherence-square-dependent-cocone f g c' P d' s))

  dependent-htpy-dependent-cocone :
    ( c c' : cocone f g X) (H : htpy-cocone f g c c') (P : X → UU l5)
    ( d : dependent-cocone f g c P) (d' : dependent-cocone f g c' P) →
    UU (l1 ⊔ l2 ⊔ l3 ⊔ l5)
  dependent-htpy-dependent-cocone c c' H P d d' =
    Σ ( dependent-homotopy (λ _ → P)
        ( horizontal-htpy-cocone f g c c' H)
        ( horizontal-map-dependent-cocone f g c P d)
        ( horizontal-map-dependent-cocone f g c' P d'))
      ( λ K →
        Σ ( dependent-homotopy (λ _ → P)
            ( vertical-htpy-cocone f g c c' H)
            ( vertical-map-dependent-cocone f g c P d)
            ( vertical-map-dependent-cocone f g c' P d'))
          ( coherence-dependent-htpy-dependent-cocone c c' H P d d' K))

  refl-dependent-htpy-dependent-cocone :
    ( c : cocone f g X) (P : X → UU l5) (d : dependent-cocone f g c P) →
    dependent-htpy-dependent-cocone c c (refl-htpy-cocone f g c) P d d
  pr1 (refl-dependent-htpy-dependent-cocone c P d) = refl-htpy
  pr1 (pr2 (refl-dependent-htpy-dependent-cocone c P d)) = refl-htpy
  pr2 (pr2 (refl-dependent-htpy-dependent-cocone c P d)) s =
    right-unit-dependent-identification P
      ( coherence-square-cocone f g c s)
      ( coherence-square-dependent-cocone f g c P d s)

  dependent-htpy-dependent-eq-dependent-cocone :
    (c c' : cocone f g X) (p : c ＝ c') (P : X → UU l5)
    (d : dependent-cocone f g c P) (d' : dependent-cocone f g c' P) →
    dependent-identification (λ c'' → dependent-cocone f g c'' P) p d d' →
    dependent-htpy-dependent-cocone c c' (htpy-eq-cocone f g c c' p) P d d'
  dependent-htpy-dependent-eq-dependent-cocone c .c refl P d ._ refl =
    refl-dependent-htpy-dependent-cocone c P d

  abstract
    is-torsorial-dependent-htpy-over-refl-dependent-cocone :
      (c : cocone f g X) (P : X → UU l5) (d : dependent-cocone f g c P) →
      is-torsorial
        ( dependent-htpy-dependent-cocone c c (refl-htpy-cocone f g c) P d)
    is-torsorial-dependent-htpy-over-refl-dependent-cocone c P d =
      is-torsorial-Eq-structure
        ( is-torsorial-htpy _)
        ( horizontal-map-dependent-cocone f g c P d , refl-htpy)
        ( is-torsorial-Eq-structure
          ( is-torsorial-htpy _)
          ( vertical-map-dependent-cocone f g c P d , refl-htpy)
          ( is-torsorial-htpy _))

Characterizing equality of cocones equipped with dependent cocones

We now move to characterize equality of cocones equipped with dependent cocones, from which it follows that dependent homotopies of dependent cocones characterize dependent identifications of them.

module _
  {l1 l2 l3 l4 l5 : Level}
  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
  {X : UU l4} (P : X → UU l5)
  where

  htpy-cocone-with-dependent-cocone :
    (c c' : cocone-with-dependent-cocone f g P) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
  htpy-cocone-with-dependent-cocone c c' =
    Σ ( htpy-cocone f g
        ( cocone-cocone-with-dependent-cocone f g P c)
        ( cocone-cocone-with-dependent-cocone f g P c'))
      ( λ H →
        dependent-htpy-dependent-cocone f g
          ( cocone-cocone-with-dependent-cocone f g P c)
          ( cocone-cocone-with-dependent-cocone f g P c')
          ( H)
          ( P)
          ( dependent-cocone-cocone-with-dependent-cocone f g P c)
          ( dependent-cocone-cocone-with-dependent-cocone f g P c'))

  refl-htpy-cocone-with-dependent-cocone :
    (c : cocone-with-dependent-cocone f g P) →
    htpy-cocone-with-dependent-cocone c c
  pr1 (refl-htpy-cocone-with-dependent-cocone c) =
    refl-htpy-cocone f g (cocone-cocone-with-dependent-cocone f g P c)
  pr2 (refl-htpy-cocone-with-dependent-cocone c) =
    refl-dependent-htpy-dependent-cocone f g
      ( cocone-cocone-with-dependent-cocone f g P c)
      ( P)
      ( dependent-cocone-cocone-with-dependent-cocone f g P c)

  htpy-eq-cocone-with-dependent-cocone :
    (c c' : cocone-with-dependent-cocone f g P) →
    c ＝ c' →
    htpy-cocone-with-dependent-cocone c c'
  htpy-eq-cocone-with-dependent-cocone c .c refl =
    refl-htpy-cocone-with-dependent-cocone c

  abstract
    is-torsorial-htpy-cocone-with-dependent-cocone :
      (c : cocone-with-dependent-cocone f g P) →
      is-torsorial (htpy-cocone-with-dependent-cocone c)
    is-torsorial-htpy-cocone-with-dependent-cocone c =
      is-torsorial-Eq-structure
        ( is-torsorial-htpy-cocone f g
          ( cocone-cocone-with-dependent-cocone f g P c))
        ( cocone-cocone-with-dependent-cocone f g P c ,
          refl-htpy-cocone f g (cocone-cocone-with-dependent-cocone f g P c))
        ( is-torsorial-dependent-htpy-over-refl-dependent-cocone f g
          ( cocone-cocone-with-dependent-cocone f g P c)
          ( P)
          ( dependent-cocone-cocone-with-dependent-cocone f g P c))

  abstract
    is-equiv-htpy-eq-cocone-with-dependent-cocone :
      (c c' : cocone-with-dependent-cocone f g P) →
      is-equiv (htpy-eq-cocone-with-dependent-cocone c c')
    is-equiv-htpy-eq-cocone-with-dependent-cocone c =
      fundamental-theorem-id
        ( is-torsorial-htpy-cocone-with-dependent-cocone c)
        ( htpy-eq-cocone-with-dependent-cocone c)

  eq-htpy-cocone-with-dependent-cocone :
    (c c' : cocone-with-dependent-cocone f g P) →
    htpy-cocone-with-dependent-cocone c c' → c ＝ c'
  eq-htpy-cocone-with-dependent-cocone c c' =
    map-inv-is-equiv (is-equiv-htpy-eq-cocone-with-dependent-cocone c c')

  extensionality-cocone-with-dependent-cocone :
    (c c' : cocone-with-dependent-cocone f g P) →
    (c ＝ c') ≃ htpy-cocone-with-dependent-cocone c c'
  extensionality-cocone-with-dependent-cocone c c' =
    ( htpy-eq-cocone-with-dependent-cocone c c' ,
      is-equiv-htpy-eq-cocone-with-dependent-cocone c c')

Dependent cocones on constant type families are equivalent to nondependent cocones

module _
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
  where

  dependent-cocone-constant-type-family-cocone :
    cocone f g Y → dependent-cocone f g c (λ _ → Y)
  pr1 (dependent-cocone-constant-type-family-cocone (f' , g' , H)) = f'
  pr1 (pr2 (dependent-cocone-constant-type-family-cocone (f' , g' , H))) = g'
  pr2 (pr2 (dependent-cocone-constant-type-family-cocone (f' , g' , H))) s =
    tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)) ∙ H s

  cocone-dependent-cocone-constant-type-family :
    dependent-cocone f g c (λ _ → Y) → cocone f g Y
  pr1 (cocone-dependent-cocone-constant-type-family (f' , g' , H)) = f'
  pr1 (pr2 (cocone-dependent-cocone-constant-type-family (f' , g' , H))) = g'
  pr2 (pr2 (cocone-dependent-cocone-constant-type-family (f' , g' , H))) s =
    ( inv
      ( tr-constant-type-family (coherence-square-cocone f g c s) (f' (f s)))) ∙
    ( H s)

  is-section-cocone-dependent-cocone-constant-type-family :
    is-section
      ( dependent-cocone-constant-type-family-cocone)
      ( cocone-dependent-cocone-constant-type-family)
  is-section-cocone-dependent-cocone-constant-type-family (f' , g' , H) =
    eq-pair-eq-fiber
      ( eq-pair-eq-fiber
        ( eq-htpy
          ( λ s →
            is-section-inv-concat
              ( tr-constant-type-family
                ( coherence-square-cocone f g c s)
                ( f' (f s)))
              ( H s))))

  is-retraction-cocone-dependent-cocone-constant-type-family :
    is-retraction
      ( dependent-cocone-constant-type-family-cocone)
      ( cocone-dependent-cocone-constant-type-family)
  is-retraction-cocone-dependent-cocone-constant-type-family (f' , g' , H) =
    eq-pair-eq-fiber
      ( eq-pair-eq-fiber
        ( eq-htpy
          ( λ s →
            is-retraction-inv-concat
              ( tr-constant-type-family
                ( coherence-square-cocone f g c s)
                ( f' (f s)))
              ( H s))))

  is-equiv-dependent-cocone-constant-type-family-cocone :
    is-equiv dependent-cocone-constant-type-family-cocone
  is-equiv-dependent-cocone-constant-type-family-cocone =
    is-equiv-is-invertible
      ( cocone-dependent-cocone-constant-type-family)
      ( is-section-cocone-dependent-cocone-constant-type-family)
      ( is-retraction-cocone-dependent-cocone-constant-type-family)

  compute-dependent-cocone-constant-type-family :
    cocone f g Y ≃ dependent-cocone f g c (λ _ → Y)
  compute-dependent-cocone-constant-type-family =
    ( dependent-cocone-constant-type-family-cocone ,
      is-equiv-dependent-cocone-constant-type-family-cocone)

Computing the dependent cocone map on a constant type family

module _
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
  where

  triangle-dependent-cocone-map-constant-type-family :
    dependent-cocone-map f g c (λ _ → Y) ~
    dependent-cocone-constant-type-family-cocone f g c ∘ cocone-map f g c
  triangle-dependent-cocone-map-constant-type-family h =
    eq-htpy-dependent-cocone f g c
      ( λ _ → Y)
      ( dependent-cocone-map f g c (λ _ → Y) h)
      ( dependent-cocone-constant-type-family-cocone f g c (cocone-map f g c h))
      ( ( refl-htpy) ,
        ( refl-htpy) ,
        ( λ s →
          right-unit ∙
          apd-constant-type-family h (coherence-square-cocone f g c s)))

  triangle-dependent-cocone-map-constant-type-family' :
    cocone-map f g c ~
    cocone-dependent-cocone-constant-type-family f g c ∘
    dependent-cocone-map f g c (λ _ → Y)
  triangle-dependent-cocone-map-constant-type-family' h =
    eq-htpy-cocone f g
      ( cocone-map f g c h)
      ( ( cocone-dependent-cocone-constant-type-family f g c
          ( dependent-cocone-map f g c (λ _ → Y) h)))
      ( ( refl-htpy) ,
        ( refl-htpy) ,
        ( λ s →
          right-unit ∙
          left-transpose-eq-concat
            ( tr-constant-type-family
              ( coherence-square-cocone f g c s)
              ( pr1 (dependent-cocone-map f g c (λ _ → Y) h) (f s)))
            ( ap h (coherence-square-cocone f g c s))
            ( apd h (coherence-square-cocone f g c s))
            ( inv
              ( apd-constant-type-family h (coherence-square-cocone f g c s)))))

The nondependent cocone map at Y is an equivalence if and only if the dependent cocone map at the constant type family (λ _ → Y) is

module _
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X) {Y : UU l5}
  where

  is-equiv-cocone-map-is-equiv-dependent-cocone-map-constant-type-family :
    is-equiv (dependent-cocone-map f g c (λ _ → Y)) →
    is-equiv (cocone-map f g c)
  is-equiv-cocone-map-is-equiv-dependent-cocone-map-constant-type-family =
    is-equiv-top-map-triangle
      ( dependent-cocone-map f g c (λ _ → Y))
      ( dependent-cocone-constant-type-family-cocone f g c)
      ( cocone-map f g c)
      ( triangle-dependent-cocone-map-constant-type-family f g c)
      ( is-equiv-dependent-cocone-constant-type-family-cocone f g c)

  is-equiv-dependent-cocone-map-constant-type-family-is-equiv-cocone-map :
    is-equiv (cocone-map f g c) →
    is-equiv (dependent-cocone-map f g c (λ _ → Y))
  is-equiv-dependent-cocone-map-constant-type-family-is-equiv-cocone-map H =
    is-equiv-left-map-triangle
      ( dependent-cocone-map f g c (λ _ → Y))
      ( dependent-cocone-constant-type-family-cocone f g c)
      ( cocone-map f g c)
      ( triangle-dependent-cocone-map-constant-type-family f g c)
      ( H)
      ( is-equiv-dependent-cocone-constant-type-family-cocone f g c)

Computing with the characterization of identifications of dependent cocones on constant type families over a fixed cocone

If two dependent cocones on a constant type family are homotopic, then so are their nondependent counterparts.

module _
  {l1 l2 l3 l4 l5 : Level}
  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
  {X : UU l4} (c : cocone f g X)
  (Y : UU l5)
  where

  coherence-htpy-cocone-dependent-cocone-coherence-htpy-dependent-cocone-constant-type-family :
    ( d d' : dependent-cocone f g c (λ _ → Y)) →
    ( K :
      horizontal-map-dependent-cocone f g c (λ _ → Y) d ~
      horizontal-map-dependent-cocone f g c (λ _ → Y) d')
    ( L :
      vertical-map-dependent-cocone f g c (λ _ → Y) d ~
      vertical-map-dependent-cocone f g c (λ _ → Y) d')
    ( H : coherence-htpy-dependent-cocone f g c (λ _ → Y) d d' K L) →
    statement-coherence-htpy-cocone f g
      ( cocone-dependent-cocone-constant-type-family f g c d)
      ( cocone-dependent-cocone-constant-type-family f g c d')
      ( K)
      ( L)
  coherence-htpy-cocone-dependent-cocone-coherence-htpy-dependent-cocone-constant-type-family
    d d' K L H x =
    ( left-whisker-concat-coherence-square-identifications
      ( inv
        ( tr-constant-type-family
          ( coherence-square-cocone f g c x)
          ( horizontal-map-dependent-cocone f g c (λ _ → Y) d (f x))))
      ( ap (tr (λ _ → Y) (coherence-square-cocone f g c x)) (K (f x)))
      ( coherence-square-dependent-cocone f g c (λ _ → Y) d x)
      ( coherence-square-dependent-cocone f g c (λ _ → Y) d' x)
      ( L (g x))
      ( H x)) ∙
    ( ap
      ( _∙ coherence-square-dependent-cocone f g c (λ _ → Y) d' x)
      ( naturality-inv-tr-constant-type-family
        ( coherence-square-cocone f g c x)
        ( K (f x)))) ∙
    ( assoc
      ( K (f x))
      ( inv
        ( tr-constant-type-family
          ( coherence-square-cocone f g c x)
          ( horizontal-map-dependent-cocone f g c (λ _ → Y) d' (f x))))
      ( coherence-square-dependent-cocone f g c (λ _ → Y) d' x))

If the dependent cocones on constant type families constructed from nondependent cocones are homotopic, then so are the nondependent cocones.

module _
  {l1 l2 l3 l4 l5 : Level}
  {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B)
  {X : UU l4} {Y : UU l5}
  where

  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family :
    (c : cocone f g X)
    (d d' : cocone f g Y) →
    ( K : horizontal-map-cocone f g d ~ horizontal-map-cocone f g d')
    ( L : vertical-map-cocone f g d ~ vertical-map-cocone f g d') →
    coherence-htpy-dependent-cocone f g c (λ _ → Y)
      ( dependent-cocone-constant-type-family-cocone f g c d)
      ( dependent-cocone-constant-type-family-cocone f g c d')
      ( K)
      ( L) →
    statement-coherence-htpy-cocone f g
      ( d)
      ( d')
      ( K)
      ( L)
  coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family
    c d d' K L H x =
    is-injective-concat
      ( tr-constant-type-family
        ( coherence-square-cocone f g c x)
        ( horizontal-map-cocone f g d (f x)))
      ( ( inv
          ( assoc
            ( tr-constant-type-family
              ( coherence-square-cocone f g c x)
              ( horizontal-map-cocone f g d (f x)))
            ( coherence-square-cocone f g d x)
            ( L (g x)))) ∙
        ( H x) ∙
        ( right-whisker-concat-coherence-square-identifications
          ( tr-constant-type-family
            ( coherence-square-cocone f g c x)
            ( horizontal-map-cocone f g d (f x)))
          ( ap (tr (λ _ → Y) (coherence-square-cocone f g c x)) (K (f x)))
          ( K (f x))
          ( tr-constant-type-family
            ( coherence-square-cocone f g c x)
            ( horizontal-map-cocone f g d' (f x)))
          ( inv
            ( naturality-tr-constant-type-family
              ( coherence-square-cocone f g c x)
              ( K (f x))))
          ( coherence-square-cocone f g d' x)))

Recent changes