Refactor universal property of suspensions

src/elementary-number-theory/integers.lagda.md

@@ -202,7 +202,7 @@ pr2 equiv-pred-ℤ = is-equiv-pred-ℤ
 ```agda
 is-injective-succ-ℤ : is-injective succ-ℤ
 is-injective-succ-ℤ {x} {y} p =
-  inv (is-retraction-pred-ℤ x) ∙ (ap pred-ℤ p ∙ is-retraction-pred-ℤ y)
+  inv (is-retraction-pred-ℤ x) ∙ ap pred-ℤ p ∙ is-retraction-pred-ℤ y
 
 has-no-fixed-points-succ-ℤ : (x : ℤ) → succ-ℤ x ≠ x
 has-no-fixed-points-succ-ℤ (inl zero-ℕ) ()
@@ -309,7 +309,8 @@ is-set-is-positive-ℤ (inr (inl x)) = is-set-empty
 is-set-is-positive-ℤ (inr (inr x)) = is-set-unit
 
 is-positive-ℤ-Set : ℤ → Set lzero
-is-positive-ℤ-Set z = pair (is-positive-ℤ z) (is-set-is-positive-ℤ z)
+pr1 (is-positive-ℤ-Set z) = is-positive-ℤ z
+pr2 (is-positive-ℤ-Set z) = is-set-is-positive-ℤ z
 
 positive-ℤ : UU lzero
 positive-ℤ = Σ ℤ is-positive-ℤ
@@ -409,8 +410,8 @@ pr2 equiv-nonnegative-int-ℕ = is-equiv-nonnegative-int-ℕ
 is-injective-nonnegative-int-ℕ : is-injective nonnegative-int-ℕ
 is-injective-nonnegative-int-ℕ {x} {y} p =
   ( inv (is-retraction-nat-nonnegative-ℤ x)) ∙
-  ( ( ap nat-nonnegative-ℤ p) ∙
-    ( is-retraction-nat-nonnegative-ℤ y))
+  ( ap nat-nonnegative-ℤ p) ∙
+  ( is-retraction-nat-nonnegative-ℤ y)
 
 decide-is-nonnegative-ℤ :
   {x : ℤ} → (is-nonnegative-ℤ x) + (is-nonnegative-ℤ (neg-ℤ x))
@@ -431,17 +432,16 @@ succ-int-ℕ (succ-ℕ x) = refl
 
 ```agda
 is-injective-neg-ℤ : is-injective neg-ℤ
-is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ (ap neg-ℤ p ∙ neg-neg-ℤ y)
+is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y
 
-is-zero-is-zero-neg-ℤ :
-  (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x
+is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x
 is-zero-is-zero-neg-ℤ (inr (inl star)) H = refl
 ```
 
 ## See also
 
-1. We show in
-   [`structured-types.initial-pointed-type-equipped-with-automorphism`](structured-types.initial-pointed-type-equipped-with-automorphism.md)
-   that ℤ is the initial pointed type equipped with an automorphism.
-2. The group of integers is constructed in
-   [`elementary-number-theory.group-of-integers`](elementary-number-theory.group-of-integers.md).
+- We show in
+  [`structured-types.initial-pointed-type-equipped-with-automorphism`](structured-types.initial-pointed-type-equipped-with-automorphism.md)
+  that ℤ is the initial pointed type equipped with an automorphism.
+- The group of integers is constructed in
+  [`elementary-number-theory.group-of-integers`](elementary-number-theory.group-of-integers.md).

src/foundation/unit-type.lagda.md

@@ -49,7 +49,7 @@ ind-unit p star = p
 
 ```agda
 terminal-map : {l : Level} {A : UU l} → A → unit
-terminal-map = const _ unit star
+terminal-map {A = A} = const A unit star
 ```
 
 ### Points as maps out of the unit type

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

@@ -433,7 +433,7 @@ pr2 (pr2 dependent-suspension-structure-sphere-1-circle-sphere-1) =
 sphere-1-circle-sphere-1 : section sphere-1-circle
 pr1 sphere-1-circle-sphere-1 = circle-sphere-1
 pr2 sphere-1-circle-sphere-1 =
-  map-inv-dependent-up-suspension
+  map-inv-dup-suspension
     ( λ x → (sphere-1-circle (circle-sphere-1 x)) ＝ x)
     ( dependent-suspension-structure-sphere-1-circle-sphere-1)
 ```

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

@@ -43,16 +43,21 @@ pr1 (dependent-ev-suspension s B f) =
 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)
+  apd f ∘ meridian-suspension-structure s
 
 module _
-  (l : Level) {l1 l2 : Level} {X : UU l1} {Y : UU l2}
+  {l1 l2 : Level} {X : UU l1} {Y : UU l2}
   (s : suspension-structure X Y)
   where
 
-  dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l)
-  dependent-universal-property-suspension =
+  dependent-universal-property-suspension-Level :
+    (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l)
+  dependent-universal-property-suspension-Level l =
     (B : Y → UU l) → is-equiv (dependent-ev-suspension s B)
+
+  dependent-universal-property-suspension : UUω
+  dependent-universal-property-suspension =
+    {l : Level} → dependent-universal-property-suspension-Level l
 ```
 
 #### Coherence between `dependent-ev-suspension` and `dependent-cocone-map`
@@ -66,12 +71,12 @@ module _
     (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))) ~
+        ( 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/suspension-structures.lagda.md

@@ -51,9 +51,9 @@ h : (x : X) → (f ∘ (const X unit star)) x ＝ (g ∘ (const X unit star)) x
 ```
 
 Using the
-[universal property of `unit`](foundation.universal-property-unit-type.md), we
-can characterize suspension cocones as equivalent to a selection of "north" and
-"south" poles
+[universal property of the unit type](foundation.universal-property-unit-type.md),
+we can characterize suspension cocones as equivalent to a selection of "north"
+and "south" poles
 
 ```text
 north , south : Y
@@ -74,7 +74,7 @@ We call this type of structure `suspension-structure`.
 ```agda
 suspension-cocone :
   {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2)
-suspension-cocone X Y = cocone (const X unit star) (const X unit star) Y
+suspension-cocone X Y = cocone (terminal-map {A = X}) (terminal-map {A = X}) Y
 ```
 
 ### Suspension structures on a type
@@ -154,13 +154,9 @@ is-equiv-map-inv-equiv-suspension-structure-suspension-cocone X Z =
 
 htpy-comparison-suspension-cocone-suspension-structure :
   {l1 l2 : Level} (X : UU l1) (Z : UU l2) →
-    ( map-inv-equiv-suspension-structure-suspension-cocone X Z)
-  ~
-    ( cocone-suspension-structure X Z)
-htpy-comparison-suspension-cocone-suspension-structure
-  ( X)
-  ( Z)
-  ( s) =
+  ( map-inv-equiv-suspension-structure-suspension-cocone X Z) ~
+  ( cocone-suspension-structure X Z)
+htpy-comparison-suspension-cocone-suspension-structure X Z s =
   is-injective-map-equiv
     ( equiv-suspension-structure-suspension-cocone X Z)
     ( is-section-map-inv-equiv
@@ -178,9 +174,9 @@ module _
   htpy-suspension-structure :
     (c c' : suspension-structure X Z) → UU (l1 ⊔ l2)
   htpy-suspension-structure c c' =
-    Σ ( (north-suspension-structure c) ＝ (north-suspension-structure c'))
+    Σ ( north-suspension-structure c ＝ north-suspension-structure c')
       ( λ p →
-        Σ ( ( south-suspension-structure c) ＝ ( south-suspension-structure c'))
+        Σ ( south-suspension-structure c ＝ south-suspension-structure c')
           ( λ q →
             ( x : X) →
             ( meridian-suspension-structure c x ∙ q) ＝
@@ -267,9 +263,7 @@ module _
   ind-htpy-suspension-structure :
     { l : Level}
     ( P :
-      ( c' : suspension-structure X Z) →
-      ( htpy-suspension-structure c c') →
-      UU l) →
+      (c' : suspension-structure X Z) → htpy-suspension-structure c c' → UU l) →
     ( P c refl-htpy-suspension-structure) →
     ( c' : suspension-structure X Z)
     ( H : htpy-suspension-structure c c') →
@@ -300,11 +294,11 @@ module _
   ap-pr1-eq-htpy-suspension-structure =
     ind-htpy-suspension-structure
       ( λ c' H → (ap (pr1) (eq-htpy-suspension-structure H)) ＝ (pr1 H))
-      ( (ap
+      ( ap
         ( ap pr1)
         ( is-retraction-map-inv-equiv
           ( extensionality-suspension-structure c c)
-          ( refl))))
+          ( refl)))
 
   ap-pr1∘pr2-eq-htpy-suspension-structure :
     (c' : suspension-structure X Z) (H : htpy-suspension-structure c c') →