dependent-universal-property-pushout↔universal-property-pushout

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

@@ -27,6 +27,7 @@ open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.dependent-cocones-under-spans
 open import synthetic-homotopy-theory.dependent-pullback-property-pushouts
 open import synthetic-homotopy-theory.induction-principle-pushouts
+open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
 </details>
@@ -128,22 +129,23 @@ htpy-eq-dependent-cocone-map f g c ind-c {P} h h' p =
 dependent-universal-property-pushout-induction-principle-pushout :
   {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
   (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
-  ((l : Level) → induction-principle-pushout l f g c) →
-  ((l : Level) → dependent-universal-property-pushout l f g c)
+  ({l : Level} → induction-principle-pushout l f g c) →
+  ({l : Level} → dependent-universal-property-pushout l f g c)
 dependent-universal-property-pushout-induction-principle-pushout
-  f g c ind-c l P =
+  f g c ind-c P =
   is-equiv-is-invertible
-    ( ind-induction-principle-pushout f g c (ind-c l) P)
-    ( pr2 (ind-c l P))
+    ( ind-induction-principle-pushout f g c ind-c P)
+    ( pr2 (ind-c P))
     ( λ h →
-      eq-htpy (htpy-eq-dependent-cocone-map f g c
-        ( ind-c l)
-        ( ind-induction-principle-pushout f g c
-          ( ind-c l)
-          ( P)
-          ( dependent-cocone-map f g c P h))
-        ( h)
-        ( pr2 (ind-c l P) (dependent-cocone-map f g c P h))))
+      eq-htpy
+        ( htpy-eq-dependent-cocone-map f g c
+          ( ind-c)
+          ( ind-induction-principle-pushout f g c
+            ( ind-c)
+            ( P)
+            ( dependent-cocone-map f g c P h))
+          ( h)
+          ( pr2 (ind-c P) (dependent-cocone-map f g c P h))))
 ```
 
 #### The dependent universal property of pushouts implies the induction principle of pushouts
@@ -152,11 +154,10 @@ dependent-universal-property-pushout-induction-principle-pushout
 induction-principle-pushout-dependent-universal-property-pushout :
   {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
   (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
-  ((l : Level) → dependent-universal-property-pushout l f g c) →
-  ((l : Level) → induction-principle-pushout l f g c)
+  ({l : Level} → dependent-universal-property-pushout l f g c) →
+  ({l : Level} → induction-principle-pushout l f g c)
 induction-principle-pushout-dependent-universal-property-pushout
-  f g c dup-c l P =
-  pr1 (dup-c l P)
+  f g c dup-c P = pr1 (dup-c P)
 ```
 
 ### The dependent pullback property of pushouts is equivalent to the dependent universal property of pushouts
@@ -183,10 +184,10 @@ triangle-dependent-pullback-property-pushout f g (pair i (pair j H)) P h =
 dependent-pullback-property-dependent-universal-property-pushout :
   {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
   (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
-  ((l : Level) → dependent-universal-property-pushout l f g c) →
-  ((l : Level) → dependent-pullback-property-pushout l f g c)
+  ({l : Level} → dependent-universal-property-pushout l f g c) →
+  ({l : Level} → dependent-pullback-property-pushout l f g c)
 dependent-pullback-property-dependent-universal-property-pushout
-  f g (pair i (pair j H)) I l P =
+  f g (pair i (pair j H)) I P =
   let c = (pair i (pair j H)) in
   is-equiv-top-map-triangle
     ( dependent-cocone-map f g c P)
@@ -200,7 +201,7 @@ dependent-pullback-property-dependent-universal-property-pushout
       ( λ h →
         is-equiv-tot-is-fiberwise-equiv
           ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))
-    ( I l P)
+    ( I P)
 ```
 
 #### The dependent pullback property of pushouts implies the dependent universal property of pushouts
@@ -228,3 +229,29 @@ dependent-universal-property-dependent-pullback-property-pushout
         is-equiv-tot-is-fiberwise-equiv
           ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))
 ```
+
+### The non-dependent and dependent universal property of pushouts are logically equivalent
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
+  (f : S → A) (g : S → B) (c : cocone f g X)
+  where
+
+  universal-property-dependent-universal-property-pushout :
+    ({l : Level} → dependent-universal-property-pushout l f g c) →
+    ({l : Level} → universal-property-pushout l f g c)
+  universal-property-dependent-universal-property-pushout dup-c {l} =
+    universal-property-pushout-pullback-property-pushout l f g c
+      ( pullback-property-dependent-pullback-property-pushout f g c
+        ( dependent-pullback-property-dependent-universal-property-pushout f g c
+          ( dup-c)))
+
+  dependent-universal-property-universal-property-pushout :
+    ({l : Level} → universal-property-pushout l f g c) →
+    ({l : Level} → dependent-universal-property-pushout l f g c)
+  dependent-universal-property-universal-property-pushout up-c =
+    dependent-universal-property-dependent-pullback-property-pushout f g c
+      ( dependent-pullback-property-pullback-property-pushout f g c
+        ( pullback-property-pushout-universal-property-pushout f g c up-c))
+```