Dependent universal property of suspensions

src/synthetic-homotopy-theory/dependent-suspension-structures.lagda.md

@@ -113,8 +113,8 @@ module _
 ```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
-  (ss : suspension-structure X Y)
   (B : Y → UU l3)
+  (ss : suspension-structure X Y)
   where
 
   dependent-suspension-structure : UU (l1 ⊔ l3)
@@ -133,7 +133,7 @@ module _
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {B : Y → UU l3}
   {ss : suspension-structure X Y}
-  (d-ss : dependent-suspension-structure ss B)
+  (d-ss : dependent-suspension-structure B ss)
   where
 
   north-dependent-suspension-structure : B (north-suspension-structure ss)
@@ -156,15 +156,74 @@ module _
 
 #### Equivalence between dependent suspension structures and dependent suspension cocones
 
-Soon TODO
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (ss : suspension-structure X Y)
+  (B : Y → UU l3)
+  where
+
+  dependent-cocone-dependent-suspension-structure :
+    dependent-suspension-structure B ss →
+    dependent-suspension-cocone B (cocone-suspension-structure X Y ss)
+  pr1 (dependent-cocone-dependent-suspension-structure dss) t =
+    north-dependent-suspension-structure dss
+  pr1 (pr2 (dependent-cocone-dependent-suspension-structure dss)) t =
+    south-dependent-suspension-structure dss
+  pr2 (pr2 (dependent-cocone-dependent-suspension-structure dss)) x =
+    meridian-dependent-suspension-structure dss x
+
+  comparison-dependent-suspension-cocone :
+    ( dependent-suspension-cocone
+      ( B)
+      ( cocone-suspension-structure X Y ss)) ≃
+    ( dependent-suspension-structure B ss)
+  comparison-dependent-suspension-cocone =
+    equiv-Σ
+      (λ N-d-susp-str →
+        Σ (B (south-suspension-structure ss))
+          ( λ S-d-susp-str →
+            (x : X) →
+              ( dependent-identification
+                ( B)
+                ( meridian-suspension-structure ss x)
+                ( N-d-susp-str)
+                ( S-d-susp-str))))
+      ( equiv-dependent-universal-property-unit
+        ( λ x → (B (north-suspension-structure ss))))
+      ( λ N-susp-c →
+        ( equiv-Σ
+          (λ S-d-susp-str →
+            (x : X) →
+              ( dependent-identification
+                ( B)
+                ( meridian-suspension-structure ss x)
+                ( map-equiv
+                  ( equiv-dependent-universal-property-unit (λ x₁ → B (pr1 ss)))
+                  ( N-susp-c))
+                ( S-d-susp-str)))
+          (equiv-dependent-universal-property-unit
+            ( const unit (UU l3) (B (south-suspension-structure ss))))
+          λ S-susp-c → id-equiv))
+
+  htpy-map-inv-comparison-dependent-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure :
+    map-inv-equiv comparison-dependent-suspension-cocone ~
+    dependent-cocone-dependent-suspension-structure
+  htpy-map-inv-comparison-dependent-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure
+    ( dss) =
+      map-inv-equiv
+        ( equiv-ap comparison-dependent-suspension-cocone
+          ( map-inv-equiv comparison-dependent-suspension-cocone dss)
+          ( dependent-cocone-dependent-suspension-structure dss))
+        (is-section-map-inv-equiv comparison-dependent-suspension-cocone dss)
+```
 
 #### Characterizing equality of dependent suspension structures
 
 ```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
   {ss : suspension-structure X Y}
-  (d-ss d-ss' : dependent-suspension-structure ss B)
+  (d-ss d-ss' : dependent-suspension-structure B ss)
   where
 
   htpy-dependent-suspension-structure : UU (l1 ⊔ l3)
@@ -184,14 +243,49 @@ module _
                 ( N-htpy))
               ( meridian-dependent-suspension-structure d-ss' x)))
 
+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
+          ( meridian-dependent-suspension-structure d-susp-str0 x)
+          ( south-htpy-dependent-suspension-structure d-susp-str)
+          ( ap
+            (tr B (meridian-suspension-structure susp-str x))
+            (north-htpy-dependent-suspension-structure d-susp-str))
+          ( meridian-dependent-suspension-structure d-susp-str1 x))
+  meridian-htpy-dependent-suspension-structure = pr2 ∘ pr2
+
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
   {ss : suspension-structure X Y}
-  (d-ss : dependent-suspension-structure ss B)
+  (d-ss : dependent-suspension-structure B ss)
   where
 
   extensionality-dependent-suspension-structure :
-    ( d-ss' : dependent-suspension-structure ss B) →
+    ( d-ss' : dependent-suspension-structure B ss) →
     ( d-ss ＝ d-ss') ≃
     ( htpy-dependent-suspension-structure B d-ss d-ss')
   extensionality-dependent-suspension-structure =
@@ -222,7 +316,7 @@ module _
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
   {ss : suspension-structure X Y}
-  {d-ss d-ss' : dependent-suspension-structure ss B}
+  {d-ss d-ss' : dependent-suspension-structure B ss}
   where
 
   htpy-eq-dependent-suspension-structure :
@@ -242,7 +336,7 @@ module _
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} (B : Y → UU l3)
   {ss : suspension-structure X Y}
-  (d-ss : dependent-suspension-structure ss B)
+  (d-ss : dependent-suspension-structure B ss)
   where
 
   refl-htpy-dependent-suspension-structure :

src/synthetic-homotopy-theory/dependent-universal-property-suspensions.lagda.md

@@ -59,7 +59,7 @@ dependent-ev-suspension :
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
   (susp-str : suspension-structure X Y) (B : Y → UU l3) →
   ((y : Y) → B y) →
-  dependent-suspension-structure susp-str B
+  dependent-suspension-structure B susp-str
 pr1 (dependent-ev-suspension susp-str B s) =
   s (north-suspension-structure susp-str)
 pr1 (pr2 (dependent-ev-suspension susp-str B s)) =
@@ -76,3 +76,23 @@ module _
   dependent-universal-property-suspension =
     (B : Y → UU l) → is-equiv (dependent-ev-suspension susp-str B)
 ```
+
+#### Coherence between `dependent-ev-suspension` and
+
+`dependent-cocone-map`
+
+```agda
+triangle-dependent-ev-suspension :
+    {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+    (susp-str : suspension-structure X Y) →
+    (B : Y → UU l3) →
+  (map-equiv (comparison-dependent-suspension-cocone susp-str B) ∘
+      dependent-cocone-map
+        ( const X unit star)
+        ( const X unit star)
+        ( cocone-suspension-structure X Y susp-str)
+        ( B))
+      ~
+        dependent-ev-suspension susp-str B
+triangle-dependent-ev-suspension {X = X} {Y = Y} susp-str B = refl-htpy
+```

src/synthetic-homotopy-theory/pushouts.lagda.md

@@ -15,7 +15,9 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels
 
+open import synthetic-homotopy-theory.26-descent
 open import synthetic-homotopy-theory.cocones-under-spans
+open import synthetic-homotopy-theory.dependent-universal-property-pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
@@ -143,6 +145,22 @@ is-pushout f g c = is-equiv (cogap f g c)
 
 ## Properties
 
+### The pushout of a span has the dependent universal property
+
+```agda
+dependent-up-pushout :
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) →
+  dependent-universal-property-pushout l4 f g (cocone-pushout f g)
+dependent-up-pushout {l4 = l4} f g =
+  dependent-universal-property-universal-property-pushout
+  ( f)
+  ( g)
+  ( cocone-pushout f g)
+  ( λ l → up-pushout f g)
+  ( l4)
+```
+
 ### Computation with the cogap map
 
 ```agda

src/synthetic-homotopy-theory/suspension-structures.lagda.md

@@ -166,7 +166,7 @@ htpy-map-inv-comparison-suspension-cocone-cocone-suspension-structure
   ( Z)
   ( x) =
     map-inv-equiv
-      ( equiv-ap-emb (emb-equiv (comparison-suspension-cocone X Z)))
+      ( ( equiv-ap-emb (emb-equiv (comparison-suspension-cocone X Z)))) {- replace with `equiv-ap` -}
       ( is-section-map-inv-equiv (comparison-suspension-cocone X Z) x)
 
 is-equiv-map-inv-comparison-suspension-cocone :