Dependent universal property of suspensions (#718)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

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

@@ -22,6 +22,7 @@ open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-systems
 open import foundation.identity-types
+open import foundation.injective-maps
 open import foundation.structure-identity-principle
 open import foundation.transport
 open import foundation.type-arithmetic-dependent-pair-types
@@ -113,105 +114,196 @@ module _
 ```agda
 module _
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
-  (ss : suspension-structure X Y)
   (B : Y → UU l3)
+  (c : suspension-structure X Y)
   where
 
   dependent-suspension-structure : UU (l1 ⊔ l3)
   dependent-suspension-structure =
-    Σ ( B (north-suspension-structure ss))
+    Σ ( B (north-suspension-structure c))
       ( λ N →
-        Σ ( B (south-suspension-structure ss))
+        Σ ( B (south-suspension-structure c))
           ( λ S →
             (x : X) →
             dependent-identification
               ( B)
-              ( meridian-suspension-structure ss x)
+              ( meridian-suspension-structure c x)
               ( N)
               ( S)))
 
 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)
+  {c : suspension-structure X Y}
+  (d : dependent-suspension-structure B c)
   where
 
-  north-dependent-suspension-structure : B (north-suspension-structure ss)
-  north-dependent-suspension-structure = pr1 (d-ss)
+  north-dependent-suspension-structure : B (north-suspension-structure c)
+  north-dependent-suspension-structure = pr1 (d)
 
-  south-dependent-suspension-structure : B (south-suspension-structure ss)
-  south-dependent-suspension-structure = (pr1 ∘ pr2) (d-ss)
+  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 ss x)
+      ( meridian-suspension-structure c x)
       ( north-dependent-suspension-structure)
       ( south-dependent-suspension-structure)
-  meridian-dependent-suspension-structure = (pr2 ∘ pr2) (d-ss)
+  meridian-dependent-suspension-structure = (pr2 ∘ pr2) (d)
 ```
 
 ## Properties
 
 #### Equivalence between dependent suspension structures and dependent suspension cocones
 
-Soon TODO
+```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 (cocone-suspension-structure X Y 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)
+      ( cocone-suspension-structure X Y 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)))
+      ( λ N-susp-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)))
+                ( N-susp-c))
+              ( s)))
+          ( equiv-dependent-universal-property-unit
+            ( const unit (UU l3) (B (south-suspension-structure c))))
+          ( λ S-susp-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-map-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)
-  {ss : suspension-structure X Y}
-  (d-ss d-ss' : dependent-suspension-structure ss B)
+  {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-ss ＝
-        north-dependent-suspension-structure d-ss')
+    Σ ( north-dependent-suspension-structure d ＝
+        north-dependent-suspension-structure d')
       ( λ N-htpy →
-        Σ ( south-dependent-suspension-structure d-ss ＝
-            south-dependent-suspension-structure d-ss')
+        Σ ( south-dependent-suspension-structure d ＝
+            south-dependent-suspension-structure d')
           ( λ S-htpy →
             (x : X) →
             coherence-square-identifications
-              ( meridian-dependent-suspension-structure d-ss x)
+              ( meridian-dependent-suspension-structure d x)
               ( S-htpy)
               ( ap
-                ( tr B (meridian-suspension-structure ss x))
+                ( tr B (meridian-suspension-structure c x))
                 ( N-htpy))
-              ( meridian-dependent-suspension-structure d-ss' x)))
+              ( meridian-dependent-suspension-structure d' 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)
+  {c : suspension-structure X Y}
+  (d : dependent-suspension-structure B c)
   where
 
   extensionality-dependent-suspension-structure :
-    ( d-ss' : dependent-suspension-structure ss B) →
-    ( d-ss ＝ d-ss') ≃
-    ( htpy-dependent-suspension-structure B d-ss d-ss')
+    ( 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-ss ＝ S)
+        Σ (south-dependent-suspension-structure d ＝ S)
           ( λ S-htpy →
             (x : X) →
             coherence-square-identifications
-              ( meridian-dependent-suspension-structure d-ss x)
+              ( meridian-dependent-suspension-structure d x)
               ( S-htpy)
-              ( ap (tr B (meridian-suspension-structure ss x)) N-htpy)
+              ( ap (tr B (meridian-suspension-structure c x)) N-htpy)
               ( m x)))
       ( refl)
       ( refl , λ x → right-unit)
       ( λ N → id-equiv)
       ( extensionality-Σ
         ( λ m S-htpy →
           (x : X) →
-          ( meridian-dependent-suspension-structure d-ss x ∙ S-htpy) ＝
+          ( meridian-dependent-suspension-structure d x ∙ S-htpy) ＝
           ( m x))
         ( refl)
         ( λ x → right-unit)
@@ -221,32 +313,32 @@ 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}
+  {c : suspension-structure X Y}
+  {d d' : dependent-suspension-structure B c}
   where
 
   htpy-eq-dependent-suspension-structure :
-    (d-ss ＝ d-ss') →
-    htpy-dependent-suspension-structure B d-ss d-ss'
+    (d ＝ d') →
+    htpy-dependent-suspension-structure B d d'
   htpy-eq-dependent-suspension-structure =
     map-equiv
-      ( extensionality-dependent-suspension-structure B d-ss d-ss')
+      ( extensionality-dependent-suspension-structure B d d')
 
   eq-htpy-dependent-suspension-structure :
-    htpy-dependent-suspension-structure B d-ss d-ss' →
-    d-ss ＝ d-ss'
+    htpy-dependent-suspension-structure B d d' →
+    d ＝ d'
   eq-htpy-dependent-suspension-structure =
     map-inv-equiv
-      ( extensionality-dependent-suspension-structure B d-ss d-ss')
+      ( extensionality-dependent-suspension-structure B d d')
 
 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)
+  {c : suspension-structure X Y}
+  (d : dependent-suspension-structure B c)
   where
 
   refl-htpy-dependent-suspension-structure :
-    htpy-dependent-suspension-structure B d-ss d-ss
+    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

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

@@ -57,22 +57,45 @@ This is the dependent analog of the
 ```agda
 dependent-ev-suspension :
   {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
-  (susp-str : suspension-structure X Y) (B : Y → UU l3) →
+  (s : suspension-structure X Y) (B : Y → UU l3) →
   ((y : Y) → B y) →
-  dependent-suspension-structure susp-str B
-pr1 (dependent-ev-suspension susp-str B s) =
-  s (north-suspension-structure susp-str)
-pr1 (pr2 (dependent-ev-suspension susp-str B s)) =
-  s (south-suspension-structure susp-str)
-pr2 (pr2 (dependent-ev-suspension susp-str B s)) =
-  (apd s) ∘ (meridian-suspension-structure susp-str)
+  dependent-suspension-structure B s
+pr1 (dependent-ev-suspension s B f) =
+  f (north-suspension-structure s)
+pr1 (pr2 (dependent-ev-suspension s B f)) =
+  f (south-suspension-structure s)
+pr2 (pr2 (dependent-ev-suspension s B f)) =
+  (apd f) ∘ (meridian-suspension-structure s)
 
 module _
   (l : Level) {l1 l2 : Level} {X : UU l1} {Y : UU l2}
-  (susp-str : suspension-structure X Y)
+  (s : suspension-structure X Y)
   where
 
   dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l)
   dependent-universal-property-suspension =
-    (B : Y → UU l) → is-equiv (dependent-ev-suspension susp-str B)
+    (B : Y → UU l) → is-equiv (dependent-ev-suspension s B)
+```
+
+#### Coherence between `dependent-ev-suspension` and
+
+`dependent-cocone-map`
+
+```agda
+module _
+  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
+  where
+
+  triangle-dependent-ev-suspension :
+    (s : suspension-structure X Y) →
+    (B : Y → UU l3) →
+    ( ( map-equiv
+      ( equiv-dependent-suspension-structure-suspension-cocone s B)) ∘
+    ( dependent-cocone-map
+      ( const X unit star)
+      ( const X unit star)
+      ( cocone-suspension-structure X Y s)
+      ( B))) ~
+    ( dependent-ev-suspension s B)
+  triangle-dependent-ev-suspension s 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,25 @@ is-pushout f g c = is-equiv (cogap f g c)
 
 ## Properties
 
+### The pushout of a span has the dependent universal property
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  where
+
+  dependent-up-pushout :
+    (f : S → A) (g : S → B) →
+    dependent-universal-property-pushout l4 f g (cocone-pushout f g)
+  dependent-up-pushout 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