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/products-of-tuples-of-types.lagda.md

@@ -38,13 +38,4 @@ pr-product-tuple-types :
   {l : Level} {n : ℕ} (A : tuple-types l n) (i : Fin n) →
   product-tuple-types n A → A i
 pr-product-tuple-types A i f = f i
-
-{-
-equiv-universal-property-product-tuple-types :
-  {l : Level} {n : ℕ} (A : tuple-types l (succ-ℕ n)) (i : Fin (succ-ℕ n)) →
-  ( product-tuple-types (succ-ℕ n) A) ≃
-  ( ( product-tuple-types n {!!}) × A i)
-equiv-universal-property-product-tuple-types A i =
-  {!!}
-  -}
 ```

src/foundation/unit-type.lagda.md

@@ -25,7 +25,7 @@ open import foundation-core.truncation-levels
 
 ## Idea
 
-The unit type is inductively generated by one point.
+The **unit type** is a type inductively generated by a single point.
 
 ## Definition
 
@@ -41,22 +41,30 @@ record unit : UU lzero where
 ### The induction principle of the unit type
 
 ```agda
-ind-unit : {l : Level} {P : unit → UU l} → P star → ((x : unit) → P x)
+ind-unit : {l : Level} {P : unit → UU l} → P star → (x : unit) → P x
 ind-unit p star = p
 ```
 
 ### The terminal map out of a type
 
 ```agda
-terminal-map : {l : Level} {A : UU l} → A → unit
-terminal-map = const _ unit star
+module _
+  {l : Level} {A : UU l}
+  where
+
+  terminal-map : A → unit
+  terminal-map = const A unit star
 ```
 
 ### Points as maps out of the unit type
 
 ```agda
-point : {l : Level} {A : UU l} → A → (unit → A)
-point a = const unit _ a
+module _
+  {l : Level} {A : UU l}
+  where
+
+  point : A → (unit → A)
+  point = const unit A
 ```
 
 ### Raising the universe level of the unit type

src/foundation/universal-property-cartesian-product-types.lagda.md

@@ -36,24 +36,35 @@ product
 ### The universal property of cartesian products as pullbacks
 
 ```agda
-universal-property-product :
+map-up-product :
   {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} →
-  ((x : X) → A x × B x) ≃ (((x : X) → A x) × ((x : X) → B x))
-pr1 universal-property-product f = (λ x → pr1 (f x)) , (λ x → pr2 (f x))
-pr2 universal-property-product =
+  ((x : X) → A x × B x) → (((x : X) → A x) × ((x : X) → B x))
+pr1 (map-up-product f) x = pr1 (f x)
+pr2 (map-up-product f) x = pr2 (f x)
+
+up-product :
+  {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} →
+  is-equiv (map-up-product {A = A} {B})
+up-product =
   is-equiv-is-invertible
     ( λ (f , g) → (λ x → (f x , g x)))
     ( refl-htpy)
     ( refl-htpy)
 
-module _
-  {l1 l2 : Level} (A : UU l1) (B : UU l2)
-  where
+equiv-up-product :
+  {l1 l2 l3 : Level} {X : UU l1} {A : X → UU l2} {B : X → UU l3} →
+  ((x : X) → A x × B x) ≃ (((x : X) → A x) × ((x : X) → B x))
+pr1 equiv-up-product = map-up-product
+pr2 equiv-up-product = up-product
 ```
 
 We construct the cone for two maps into the unit type.
 
 ```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : UU l2)
+  where
+
   cone-prod : cone (const A unit star) (const B unit star) (A × B)
   pr1 cone-prod = pr1
   pr1 (pr2 cone-prod) = pr2

src/species/composition-cauchy-series-species-of-types.lagda.md

@@ -88,8 +88,8 @@ module _
             ( λ V →
               ( equiv-prod
                 ( id-equiv)
-                ( ( inv-equiv universal-property-product) ∘e
-                  ( equiv-prod id-equiv equiv-ev-pair))) ∘e
+                ( inv-equiv equiv-up-product ∘e
+                  equiv-prod id-equiv equiv-ev-pair)) ∘e
               ( left-unit-law-Σ-is-contr
                 ( is-torsorial-equiv' (Σ U V))
                 ( Σ U V , id-equiv))))))) ∘e

src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md

@@ -159,8 +159,7 @@ module _
             ( λ B →
               ( equiv-prod
                 ( id-equiv)
-                ( universal-property-product ∘e
-                  equiv-postcomp X (C2 A B))) ∘e
+                ( equiv-up-product ∘e equiv-postcomp X (C2 A B))) ∘e
               left-unit-law-Σ-is-contr
                 ( is-torsorial-equiv-subuniverse'
                   ( P)

src/species/products-dirichlet-series-species-of-types.lagda.md

@@ -110,8 +110,7 @@ module _
             ( λ B →
               ( equiv-prod
                 ( id-equiv)
-                ( universal-property-product ∘e
-                  equiv-postcomp X (C1 A B))) ∘e
+                ( equiv-up-product ∘e equiv-postcomp X (C1 A B))) ∘e
               ( left-unit-law-Σ-is-contr
                 ( is-torsorial-equiv' (A × B))
                 ( A × B , id-equiv))))) ∘e

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,16 @@ 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 : UUω
   dependent-universal-property-suspension =
-    (B : Y → UU l) → is-equiv (dependent-ev-suspension s B)
+    {l : Level} (B : Y → UU l) → is-equiv (dependent-ev-suspension s B)
 ```
 
 #### Coherence between `dependent-ev-suspension` and `dependent-cocone-map`
@@ -66,12 +66,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') →