# Dependent cocones under spans ```agda module synthetic-homotopy-theory.dependent-cocones-under-spans where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea Consider a span `𝒮 := (A <-- S --> B)` and a [cocone structure](synthetic-homotopy-theory.cocones-under-spans.md) `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 ```text i' : (a : A) → P (i a) j' : (b : B) → P (j b) ``` and a family of [dependent identifications](foundation.dependent-identifications.md) ```text (s : S) → dependent-identification P (H s) (i' (f s)) (j' (g s)). ``` ## Definitions ### Dependent cocones ```agda 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 ```agda 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 ```agda 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 ```agda 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 ```agda 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. ```agda 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 ```agda 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 ```agda 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 ```agda 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. ```agda 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. ```agda 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))) ```