Merge branch 'master' into refactor-up-limits

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-core/equivalences.lagda.md

@@ -479,7 +479,7 @@ module _
 
   htpy-map-inv-is-equiv :
     {f g : A → B} (G : f ~ g) (H : is-equiv f) (K : is-equiv g) →
-    (map-inv-is-equiv H) ~ (map-inv-is-equiv K)
+    map-inv-is-equiv H ~ map-inv-is-equiv K
   htpy-map-inv-is-equiv G H K b =
     ( inv
       ( is-retraction-map-inv-is-equiv K (map-inv-is-equiv H b))) ∙

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/foundation/universal-property-unit-type.lagda.md

@@ -63,6 +63,11 @@ equiv-universal-property-unit :
 pr1 (equiv-universal-property-unit Y) = ev-star' Y
 pr2 (equiv-universal-property-unit Y) = universal-property-unit Y
 
+inv-equiv-universal-property-unit :
+  {l : Level} (Y : UU l) → Y ≃ (unit → Y)
+inv-equiv-universal-property-unit Y =
+  inv-equiv (equiv-universal-property-unit Y)
+
 abstract
   is-equiv-point-is-contr :
     {l1 : Level} {X : UU l1} (x : X) →

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

@@ -88,7 +88,7 @@ module _
             ( λ V →
               ( equiv-prod
                 ( id-equiv)
-                ( ( inv-equiv universal-property-product) ∘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))

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

@@ -260,25 +260,19 @@ pr2 (pr2 suspension-structure-sphere-0-𝕊¹) = map-sphere-0-eq-base-𝕊¹
 
 circle-sphere-1 : sphere 1 → 𝕊¹
 circle-sphere-1 =
-  map-inv-up-suspension
-    ( sphere 0)
-    ( 𝕊¹)
+  cogap-suspension
     ( suspension-structure-sphere-0-𝕊¹)
 
 circle-sphere-1-north-sphere-1-eq-base-𝕊¹ :
-  Id (circle-sphere-1 (north-sphere 1)) base-𝕊¹
+  circle-sphere-1 (north-sphere 1) ＝ base-𝕊¹
 circle-sphere-1-north-sphere-1-eq-base-𝕊¹ =
-  up-suspension-north-suspension
-    ( sphere 0)
-    ( 𝕊¹)
+  compute-north-cogap-suspension
     ( suspension-structure-sphere-0-𝕊¹)
 
 circle-sphere-1-south-sphere-1-eq-base-𝕊¹ :
   Id (circle-sphere-1 (south-sphere 1)) base-𝕊¹
 circle-sphere-1-south-sphere-1-eq-base-𝕊¹ =
-  up-suspension-south-suspension
-    ( sphere 0)
-    ( 𝕊¹)
+  compute-south-cogap-suspension
     ( suspension-structure-sphere-0-𝕊¹)
 ```
 
@@ -313,7 +307,8 @@ apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 :
     ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n)))
     ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1)
     ( sphere-1-circle-sphere-1-south-sphere-1)
-apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n =
+apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1
+  n =
   ( inv
     ( assoc
       ( ap sphere-1-circle (ap circle-sphere-1 (meridian-suspension n)))
@@ -330,9 +325,7 @@ apply-up-suspension-meridian-suspension-sphere-1-circle-sphere-1 n =
     ( λ x →
       ( ap sphere-1-circle x) ∙
       ( sphere-1-circle-base-𝕊¹-eq-south-sphere-1))
-    ( up-suspension-meridian-suspension
-      ( sphere 0)
-      ( 𝕊¹)
+    ( compute-meridian-cogap-suspension
       ( suspension-structure-sphere-0-𝕊¹)
       ( n)))
 
@@ -433,7 +426,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
+  dependent-cogap-suspension
     ( λ x → (sphere-1-circle (circle-sphere-1 x)) ＝ x)
     ( dependent-suspension-structure-sphere-1-circle-sphere-1)
 ```
@@ -470,8 +463,9 @@ apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle =
   ( identification-left-whisk
     ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1))))
     ( inv
-      ( up-suspension-meridian-suspension
-        (sphere 0) 𝕊¹ suspension-structure-sphere-0-𝕊¹ (one-Fin 1)))) ∙
+      ( compute-meridian-cogap-suspension
+          ( suspension-structure-sphere-0-𝕊¹)
+          ( one-Fin 1)))) ∙
   ( inv
     ( assoc
       ( inv (ap circle-sphere-1 (meridian-suspension (one-Fin 1))))
@@ -501,9 +495,7 @@ apply-up-suspension-meridian-zero-suspension-circle-sphere-1-circle =
   ( identification-left-whisk
     ( ap circle-sphere-1 (meridian-suspension (zero-Fin 1)))
     ( apply-up-suspension-meridian-one-suspension-circle-sphere-1-circle)) ∙
-  ( up-suspension-meridian-suspension
-    ( sphere 0)
-    ( 𝕊¹)
+  ( compute-meridian-cogap-suspension
     ( suspension-structure-sphere-0-𝕊¹)
     ( zero-Fin 1))
 

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

@@ -96,7 +96,7 @@ module _
                 ( cocone-pushout
                   ( vertical-map-span-cocone-cofork f g)
                   ( horizontal-map-span-cocone-cofork f g))))
-            ( dependent-up-pushout
+            ( dup-pushout
               ( vertical-map-span-cocone-cofork f g)
               ( horizontal-map-span-cocone-cofork f g)
               ( P)))

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

@@ -153,7 +153,7 @@ module _
 
   dependent-cocone-dependent-suspension-structure :
     dependent-suspension-structure B c →
-    dependent-suspension-cocone B (cocone-suspension-structure X Y c)
+    dependent-suspension-cocone B (suspension-cocone-suspension-structure c)
   pr1 (dependent-cocone-dependent-suspension-structure d) t =
     north-dependent-suspension-structure d
   pr1 (pr2 (dependent-cocone-dependent-suspension-structure d)) t =
@@ -164,7 +164,7 @@ module _
   equiv-dependent-suspension-structure-suspension-cocone :
     ( dependent-suspension-cocone
       ( B)
-      ( cocone-suspension-structure X Y c)) ≃
+      ( suspension-cocone-suspension-structure c)) ≃
     ( dependent-suspension-structure B c)
   equiv-dependent-suspension-structure-suspension-cocone =
     ( equiv-Σ

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)
+        ( suspension-cocone-suspension-structure s)
+        ( B))) ~
     ( dependent-ev-suspension s B)
   triangle-dependent-ev-suspension s B = refl-htpy
 ```

src/synthetic-homotopy-theory/functoriality-suspensions.lagda.md

@@ -50,17 +50,17 @@ module _
 
   map-suspension : suspension A → suspension B
   map-suspension =
-    map-inv-up-suspension A (suspension B) map-suspension-structure
+    cogap-suspension map-suspension-structure
 
   compute-north-map-suspension :
     map-suspension (north-suspension) ＝ north-suspension
   compute-north-map-suspension =
-    up-suspension-north-suspension A (suspension B) map-suspension-structure
+    compute-north-cogap-suspension map-suspension-structure
 
   compute-south-map-suspension :
     map-suspension (south-suspension) ＝ south-suspension
   compute-south-map-suspension =
-    up-suspension-south-suspension A (suspension B) map-suspension-structure
+    compute-south-cogap-suspension map-suspension-structure
 
   compute-meridian-map-suspension :
     (a : A) →
@@ -70,8 +70,7 @@ module _
       ( meridian-suspension (f a))
       ( compute-south-map-suspension)
   compute-meridian-map-suspension =
-    up-suspension-meridian-suspension A
-      ( suspension B)
+    compute-meridian-cogap-suspension
       ( map-suspension-structure)
 ```