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,77 @@ 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
+
+  compute-dependent-suspension-cocone :
+    ( dependent-suspension-structure B ss) ≃
+    ( dependent-suspension-cocone
+      ( B)
+      ( cocone-suspension-structure X Y ss))
+  compute-dependent-suspension-cocone =
+    inv-equiv
+      ( 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-compute-dependent-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure :
+    map-equiv compute-dependent-suspension-cocone ~
+    dependent-cocone-dependent-suspension-structure
+  htpy-map-inv-compute-dependent-suspension-cocone-cocone-dependent-cocone-dependent-suspension-structure
+    ( dss) =
+      map-inv-equiv
+        ( equiv-ap
+          ( inv-equiv compute-dependent-suspension-cocone)
+          ( map-equiv compute-dependent-suspension-cocone dss)
+          ( dependent-cocone-dependent-suspension-structure dss))
+        ( is-retraction-map-inv-equiv compute-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 +246,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 +319,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 +339,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-inv-equiv (compute-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

@@ -131,55 +131,59 @@ cocone-suspension-structure X Y (pair N (pair S merid)) =
       ( const unit Y S)
       ( merid))
 
-comparison-suspension-cocone :
+compute-suspension-cocone :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
-  suspension-cocone X Z ≃ suspension-structure X Z
-comparison-suspension-cocone X Z =
-  equiv-Σ
-    ( λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2))
-    ( equiv-universal-property-unit Z)
-    ( λ z1 →
-      equiv-Σ
-        ( λ z2 → (x : X) → Id (z1 star) z2)
-        ( equiv-universal-property-unit Z)
-        ( λ z2 → id-equiv))
-
-map-comparison-suspension-cocone :
+  suspension-structure X Z ≃ suspension-cocone X Z
+compute-suspension-cocone X Z =
+  inv-equiv
+    ( equiv-Σ
+      ( λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2))
+      ( equiv-universal-property-unit Z)
+      ( λ z1 →
+        equiv-Σ
+          ( λ z2 → (x : X) → Id (z1 star) z2)
+          ( equiv-universal-property-unit Z)
+          ( λ z2 → id-equiv)))
+
+map-compute-suspension-cocone :
+  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
+  suspension-structure X Z → suspension-cocone X Z
+map-compute-suspension-cocone X Z =
+  map-equiv (compute-suspension-cocone X Z)
+
+is-equiv-map-compute-suspension-cocone :
+  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
+  is-equiv (map-compute-suspension-cocone X Z)
+is-equiv-map-compute-suspension-cocone X Z =
+  is-equiv-map-equiv (compute-suspension-cocone X Z)
+
+map-inv-compute-suspension-cocone :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
   suspension-cocone X Z → suspension-structure X Z
-map-comparison-suspension-cocone X Z =
-  map-equiv (comparison-suspension-cocone X Z)
+map-inv-compute-suspension-cocone X Z =
+  map-inv-equiv (compute-suspension-cocone X Z)
 
-is-equiv-map-comparison-suspension-cocone :
+is-equiv-map-inv-compute-suspension-cocone :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
-  is-equiv (map-comparison-suspension-cocone X Z)
-is-equiv-map-comparison-suspension-cocone X Z =
-  is-equiv-map-equiv (comparison-suspension-cocone X Z)
+  is-equiv (map-inv-compute-suspension-cocone X Z)
+is-equiv-map-inv-compute-suspension-cocone X Z =
+  is-equiv-map-inv-equiv (compute-suspension-cocone X Z)
 
-htpy-map-inv-comparison-suspension-cocone-cocone-suspension-structure :
+htpy-comparison-suspension-cocone-suspension-structure :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
-    ( map-inv-equiv (comparison-suspension-cocone X Z))
+    ( map-compute-suspension-cocone X Z)
   ~
     ( cocone-suspension-structure X Z)
-htpy-map-inv-comparison-suspension-cocone-cocone-suspension-structure
+htpy-comparison-suspension-cocone-suspension-structure
   ( X)
   ( Z)
-  ( x) =
+  ( ss) =
     map-inv-equiv
-      ( equiv-ap-emb (emb-equiv (comparison-suspension-cocone X Z)))
-      ( is-section-map-inv-equiv (comparison-suspension-cocone X Z) x)
-
-is-equiv-map-inv-comparison-suspension-cocone :
-  {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
-  is-equiv (cocone-suspension-structure X Z)
-is-equiv-map-inv-comparison-suspension-cocone X Z =
-  is-equiv-htpy
-    ( map-inv-equiv (comparison-suspension-cocone X Z))
-    ( inv-htpy
-      ( htpy-map-inv-comparison-suspension-cocone-cocone-suspension-structure
-        ( X)
-        ( Z)))
-    ( is-equiv-map-inv-equiv (comparison-suspension-cocone X Z))
+      ( equiv-ap
+        ( inv-equiv (compute-suspension-cocone X Z))
+        ( map-equiv (compute-suspension-cocone X Z) ss)
+        ( cocone-suspension-structure X Z ss))
+      ( is-retraction-map-inv-equiv (compute-suspension-cocone X Z) ss)
 ```
 
 #### Characterization of equalities in `suspension-structure`