# Dependent suspension structures ```agda module synthetic-homotopy-theory.dependent-suspension-structures where ``` <details><summary>Imports</summary> ```agda open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications open import foundation.constant-maps open import foundation.dependent-identifications open import foundation.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.homotopies open import foundation.identity-types open import foundation.injective-maps open import foundation.structure-identity-principle open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universal-property-unit-type open import foundation.universe-levels open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.suspension-structures ``` </details> ## Idea This is the dependent analog of [suspension structures](synthetic-homotopy-theory.suspension-structures.md). The relation between [suspension structures](synthetic-homotopy-theory.suspension-structures.md) and dependent suspension structures mirrors the relation between [cocones under a span](synthetic-homotopy-theory.cocones-under-spans.md) and [dependent cocones under a span](synthetic-homotopy-theory.dependent-cocones-under-spans.md). Fix a type `X` and consider a suspension cocone `(f , g , h)` with nadir `Y`. Given a type family `P : Y → UU`, a dependent suspension cocone on `P` over `(f , g , h)` consists of dependent functions ```text north : (t : unit) → P (f t) south : (t : unit) → P (g t) ``` together with a family of dependent identifications ```text merid : (x : X) → dependent-identification P (h x) ((north ∘ (terminal-map X)) x) (south ∘ (terminal-map X) x) ``` Using the [universal property of `unit`](foundation.unit-type.md) and the previous characterization of suspension cocones (to be found in the file [synthetic-homotopy-theory.suspension-structures](synthetic-homotopy-theory.suspension-structures.md)), we can characterize dependent cocones over a suspension cocone as equivalent to the following: For a suspension structure `(N , S , m)`, a dependent suspension structure in `P` over (N , S , m)` is given by points ```text north : P N south : P S ``` and a family of dependent identifications ```text meridian : (x : X) → dependent-identification P (m x) north south ``` ## Definition ### Dependent Suspension Cocones ```agda module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) (c : suspension-cocone X Y) where dependent-suspension-cocone : UU (l1 ⊔ l3) dependent-suspension-cocone = dependent-cocone ( terminal-map X) ( terminal-map X) ( c) ( B) ``` ### Dependent Suspension Structures ```agda module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) (c : suspension-structure X Y) where dependent-suspension-structure : UU (l1 ⊔ l3) dependent-suspension-structure = Σ ( B (north-suspension-structure c)) ( λ N → Σ ( B (south-suspension-structure c)) ( λ S → (x : X) → dependent-identification ( B) ( meridian-suspension-structure c x) ( N) ( S))) module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {B : Y → UU l3} {c : suspension-structure X Y} (d : dependent-suspension-structure B c) where north-dependent-suspension-structure : B (north-suspension-structure c) north-dependent-suspension-structure = pr1 (d) south-dependent-suspension-structure : B (south-suspension-structure c) south-dependent-suspension-structure = (pr1 ∘ pr2) (d) meridian-dependent-suspension-structure : (x : X) → dependent-identification ( B) ( meridian-suspension-structure c x) ( north-dependent-suspension-structure) ( south-dependent-suspension-structure) meridian-dependent-suspension-structure = (pr2 ∘ pr2) (d) ``` ## Properties #### Equivalence between dependent suspension structures and dependent suspension cocones ```agda module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (c : suspension-structure X Y) (B : Y → UU l3) where dependent-cocone-dependent-suspension-structure : dependent-suspension-structure B c → dependent-suspension-cocone B (suspension-cocone-suspension-structure c) pr1 (dependent-cocone-dependent-suspension-structure d) t = north-dependent-suspension-structure d pr1 (pr2 (dependent-cocone-dependent-suspension-structure d)) t = south-dependent-suspension-structure d pr2 (pr2 (dependent-cocone-dependent-suspension-structure d)) x = meridian-dependent-suspension-structure d x equiv-dependent-suspension-structure-suspension-cocone : ( dependent-suspension-cocone ( B) ( suspension-cocone-suspension-structure c)) ≃ ( dependent-suspension-structure B c) equiv-dependent-suspension-structure-suspension-cocone = ( equiv-Σ ( λ n → Σ ( B (south-suspension-structure c)) ( λ s → (x : X) → ( dependent-identification ( B) ( meridian-suspension-structure c x) ( n) ( s)))) ( equiv-dependent-universal-property-unit ( λ x → B (north-suspension-structure c))) ( λ north-suspension-c → ( equiv-Σ ( λ s → (x : X) → ( dependent-identification ( B) ( meridian-suspension-structure c x) ( map-equiv ( equiv-dependent-universal-property-unit ( λ _ → B (north-suspension-structure c))) ( north-suspension-c)) ( s))) ( equiv-dependent-universal-property-unit ( point (B (south-suspension-structure c)))) ( λ south-suspension-c → id-equiv)))) htpy-map-inv-equiv-dependent-suspension-structure-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure : map-inv-equiv equiv-dependent-suspension-structure-suspension-cocone ~ dependent-cocone-dependent-suspension-structure htpy-map-inv-equiv-dependent-suspension-structure-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure ( d) = is-injective-equiv ( equiv-dependent-suspension-structure-suspension-cocone) ( is-section-map-inv-equiv ( equiv-dependent-suspension-structure-suspension-cocone) ( d)) ``` #### Characterizing equality of dependent suspension structures ```agda module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) {c : suspension-structure X Y} (d d' : dependent-suspension-structure B c) where htpy-dependent-suspension-structure : UU (l1 ⊔ l3) htpy-dependent-suspension-structure = Σ ( north-dependent-suspension-structure d = north-dependent-suspension-structure d') ( λ N-htpy → Σ ( south-dependent-suspension-structure d = south-dependent-suspension-structure d') ( λ S-htpy → (x : X) → coherence-square-identifications ( ap ( tr B (meridian-suspension-structure c x)) ( N-htpy)) ( meridian-dependent-suspension-structure d x) ( meridian-dependent-suspension-structure d' x) ( S-htpy))) module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) {susp-str : suspension-structure X Y} {d-susp-str0 d-susp-str1 : dependent-suspension-structure B susp-str} where north-htpy-dependent-suspension-structure : htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1 → north-dependent-suspension-structure d-susp-str0 = north-dependent-suspension-structure d-susp-str1 north-htpy-dependent-suspension-structure = pr1 south-htpy-dependent-suspension-structure : htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1 → south-dependent-suspension-structure d-susp-str0 = south-dependent-suspension-structure d-susp-str1 south-htpy-dependent-suspension-structure = (pr1 ∘ pr2) meridian-htpy-dependent-suspension-structure : ( d-susp-str : htpy-dependent-suspension-structure B d-susp-str0 d-susp-str1) → ( x : X) → coherence-square-identifications ( ap ( tr B (meridian-suspension-structure susp-str x)) ( north-htpy-dependent-suspension-structure d-susp-str)) ( meridian-dependent-suspension-structure d-susp-str0 x) ( meridian-dependent-suspension-structure d-susp-str1 x) ( south-htpy-dependent-suspension-structure d-susp-str) meridian-htpy-dependent-suspension-structure = pr2 ∘ pr2 module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) {c : suspension-structure X Y} (d : dependent-suspension-structure B c) where extensionality-dependent-suspension-structure : ( d' : dependent-suspension-structure B c) → ( d = d') ≃ ( htpy-dependent-suspension-structure B d d') extensionality-dependent-suspension-structure = extensionality-Σ ( λ (S , m) (N-htpy) → Σ (south-dependent-suspension-structure d = S) ( λ S-htpy → (x : X) → coherence-square-identifications ( ap (tr B (meridian-suspension-structure c x)) N-htpy) ( meridian-dependent-suspension-structure d x) ( m x) ( S-htpy))) ( refl) ( refl , λ x → right-unit) ( λ N → id-equiv) ( extensionality-Σ ( λ m S-htpy → (x : X) → ( meridian-dependent-suspension-structure d x ∙ S-htpy) = ( m x)) ( refl) ( λ x → right-unit) ( λ S → id-equiv) ( λ m → equiv-concat-htpy right-unit-htpy m ∘e inv-equiv equiv-eq-htpy)) module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) {c : suspension-structure X Y} {d d' : dependent-suspension-structure B c} where htpy-eq-dependent-suspension-structure : (d = d') → htpy-dependent-suspension-structure B d d' htpy-eq-dependent-suspension-structure = map-equiv ( extensionality-dependent-suspension-structure B d d') eq-htpy-dependent-suspension-structure : htpy-dependent-suspension-structure B d d' → d = d' eq-htpy-dependent-suspension-structure = map-inv-equiv ( extensionality-dependent-suspension-structure B d d') module _ {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3) {c : suspension-structure X Y} (d : dependent-suspension-structure B c) where refl-htpy-dependent-suspension-structure : htpy-dependent-suspension-structure B d d pr1 refl-htpy-dependent-suspension-structure = refl pr1 (pr2 refl-htpy-dependent-suspension-structure) = refl pr2 (pr2 refl-htpy-dependent-suspension-structure) x = right-unit is-refl-refl-htpy-dependent-suspension-structure : refl-htpy-dependent-suspension-structure = htpy-eq-dependent-suspension-structure B refl is-refl-refl-htpy-dependent-suspension-structure = refl ```