Janitorial work on equivalences and embeddings (#1085)

Extracts changes made in #1078 to parts of the library outside of
`modal-type-theory`.

src/elementary-number-theory/powers-of-two.lagda.md

@@ -184,8 +184,8 @@ is-split-surjective-pairing-map n =
 ### Pairing function is injective
 
 ```agda
-is-injecitve-pairing-map : is-injective pairing-map
-is-injecitve-pairing-map {u , v} {u' , v'} p =
+is-injective-pairing-map : is-injective pairing-map
+is-injective-pairing-map {u , v} {u' , v'} p =
   ( eq-pair' (is-pair-expansion-unique u u' v v' q))
   where
   r = is-successor-is-nonzero-ℕ (is-nonzero-pair-expansion u v)
@@ -203,6 +203,6 @@ is-equiv-pairing-map : is-equiv pairing-map
 is-equiv-pairing-map =
   is-equiv-is-split-surjective-is-injective
     pairing-map
-    is-injecitve-pairing-map
+    is-injective-pairing-map
     is-split-surjective-pairing-map
 ```

src/foundation-core.lagda.md

@@ -40,6 +40,7 @@ open import foundation-core.negation public
 open import foundation-core.operations-span-diagrams public
 open import foundation-core.operations-spans public
 open import foundation-core.path-split-maps public
+open import foundation-core.postcomposition-dependent-functions public
 open import foundation-core.postcomposition-functions public
 open import foundation-core.precomposition-dependent-functions public
 open import foundation-core.precomposition-functions public

src/foundation-core/equivalences.lagda.md

@@ -174,15 +174,11 @@ module _
   where
 
   is-equiv-is-invertible' : is-invertible f → is-equiv f
-  pr1 (pr1 (is-equiv-is-invertible' (g , H , K))) = g
-  pr2 (pr1 (is-equiv-is-invertible' (g , H , K))) = H
-  pr1 (pr2 (is-equiv-is-invertible' (g , H , K))) = g
-  pr2 (pr2 (is-equiv-is-invertible' (g , H , K))) = K
+  is-equiv-is-invertible' (g , H , K) = ((g , H) , (g , K))
 
   is-equiv-is-invertible :
     (g : B → A) (H : f ∘ g ~ id) (K : g ∘ f ~ id) → is-equiv f
-  is-equiv-is-invertible g H K =
-    is-equiv-is-invertible' (g , H , K)
+  is-equiv-is-invertible g H K = is-equiv-is-invertible' (g , H , K)
 
   is-retraction-map-section-is-equiv :
     (H : is-equiv f) → is-retraction f (map-section-is-equiv H)
@@ -206,27 +202,33 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
   where
 
+  is-equiv-is-coherently-invertible :
+    is-coherently-invertible f → is-equiv f
+  is-equiv-is-coherently-invertible H =
+    is-equiv-is-invertible' (is-invertible-is-coherently-invertible H)
+
+  is-equiv-is-transpose-coherently-invertible :
+    is-transpose-coherently-invertible f → is-equiv f
+  is-equiv-is-transpose-coherently-invertible H =
+    is-equiv-is-invertible'
+      ( is-invertible-is-transpose-coherently-invertible H)
+```
+
+The following maps are not simple constructions and should not be computed with.
+Therefore, we mark them as `abstract`.
+
+```agda
   abstract
     is-coherently-invertible-is-equiv :
       is-equiv f → is-coherently-invertible f
     is-coherently-invertible-is-equiv =
       is-coherently-invertible-is-invertible ∘ is-invertible-is-equiv
 
-    is-equiv-is-coherently-invertible :
-      is-coherently-invertible f → is-equiv f
-    is-equiv-is-coherently-invertible H =
-      is-equiv-is-invertible' (is-invertible-is-coherently-invertible H)
-
+  abstract
     is-transpose-coherently-invertible-is-equiv :
       is-equiv f → is-transpose-coherently-invertible f
     is-transpose-coherently-invertible-is-equiv =
       is-transpose-coherently-invertible-is-invertible ∘ is-invertible-is-equiv
-
-    is-equiv-is-transpose-coherently-invertible :
-      is-transpose-coherently-invertible f → is-equiv f
-    is-equiv-is-transpose-coherently-invertible H =
-      is-equiv-is-invertible'
-        ( is-invertible-is-transpose-coherently-invertible H)
 ```
 
 ### Structure obtained from being coherently invertible
@@ -421,10 +423,8 @@ module _
   abstract
     is-equiv-comp :
       (g : B → X) (h : A → B) → is-equiv h → is-equiv g → is-equiv (g ∘ h)
-    pr1 (is-equiv-comp g h (sh , rh) (sg , rg)) =
-      section-comp g h sh sg
-    pr2 (is-equiv-comp g h (sh , rh) (sg , rg)) =
-      retraction-comp g h rg rh
+    pr1 (is-equiv-comp g h (sh , rh) (sg , rg)) = section-comp g h sh sg
+    pr2 (is-equiv-comp g h (sh , rh) (sg , rg)) = retraction-comp g h rg rh
 
   equiv-comp : B ≃ X → A ≃ B → A ≃ X
   pr1 (equiv-comp g h) = map-equiv g ∘ map-equiv h
@@ -688,7 +688,7 @@ module _
   pr2 (equiv-ap e x y) = is-emb-is-equiv (is-equiv-map-equiv e) x y
 
   map-inv-equiv-ap :
-    (e : A ≃ B) (x y : A) → (map-equiv e x ＝ map-equiv e y) → (x ＝ y)
+    (e : A ≃ B) (x y : A) → map-equiv e x ＝ map-equiv e y → x ＝ y
   map-inv-equiv-ap e x y = map-inv-equiv (equiv-ap e x y)
 ```
 

src/foundation-core/injective-maps.lagda.md

@@ -19,6 +19,7 @@ open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositional-maps
 open import foundation-core.propositions
+open import foundation-core.retractions
 open import foundation-core.sections
 open import foundation-core.sets
 ```
@@ -106,26 +107,28 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
 
-  abstract
-    is-injective-is-equiv : {f : A → B} → is-equiv f → is-injective f
-    is-injective-is-equiv H {x} {y} p =
-      ( inv (is-retraction-map-inv-is-equiv H x)) ∙
-      ( ( ap (map-inv-is-equiv H) p) ∙
-        ( is-retraction-map-inv-is-equiv H y))
+  is-injective-is-equiv : {f : A → B} → is-equiv f → is-injective f
+  is-injective-is-equiv {f} H =
+    is-injective-retraction f (retraction-is-equiv H)
 
-  abstract
-    is-injective-equiv : (e : A ≃ B) → is-injective (map-equiv e)
-    is-injective-equiv (pair f H) = is-injective-is-equiv H
+  is-injective-equiv : (e : A ≃ B) → is-injective (map-equiv e)
+  is-injective-equiv e = is-injective-is-equiv (is-equiv-map-equiv e)
 
+abstract
+  is-injective-map-inv-equiv :
+    {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B) →
+    is-injective (map-inv-equiv e)
+  is-injective-map-inv-equiv e =
+    is-injective-is-equiv (is-equiv-map-inv-equiv e)
+```
+
+### Injective maps that have a section are equivalences
+
+```agda
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2}
   where
 
-  abstract
-    is-injective-map-inv-equiv : (e : A ≃ B) → is-injective (map-inv-equiv e)
-    is-injective-map-inv-equiv e =
-      is-injective-is-equiv (is-equiv-map-inv-equiv e)
-
   is-equiv-is-injective : {f : A → B} → section f → is-injective f → is-equiv f
   is-equiv-is-injective {f} (pair g G) H =
     is-equiv-is-invertible g G (λ x → H (G (f x)))

src/foundation-core/invertible-maps.lagda.md

@@ -319,15 +319,12 @@ repeat the proof to avoid cyclic dependencies.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B}
-  (H : is-invertible f) {x y : A}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-invertible f)
   where
 
-  is-injective-is-invertible : f x ＝ f y → x ＝ y
-  is-injective-is-invertible p =
-    ( inv (is-retraction-map-inv-is-invertible H x)) ∙
-    ( ( ap (map-inv-is-invertible H) p) ∙
-      ( is-retraction-map-inv-is-invertible H y))
+  is-injective-is-invertible : {x y : A} → f x ＝ f y → x ＝ y
+  is-injective-is-invertible =
+    is-injective-retraction f (retraction-is-invertible H)
 ```
 
 ## See also

src/foundation-core/postcomposition-dependent-functions.lagda.md

@@ -0,0 +1,50 @@
+# Postcomposition of dependent functions
+
+```agda
+module foundation-core.postcomposition-dependent-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+```
+
+</details>
+
+## Idea
+
+Given a type `A` and a family of maps `f : {a : A} → X a → Y a`, the
+{{#concept "postcomposition function" Disambiguation="of dependent functions by a family of maps" Agda=postcomp-Π}}
+of dependent functions `(a : A) → X a` by the family of maps `f`
+
+```text
+  postcomp-Π A f : ((a : A) → X a) → ((a : A) → Y a)
+```
+
+is defined by `λ h x → f (h x)`.
+
+Note that, since the definition of the family of maps `f` depends on the base
+`A`, postcomposition of dependent functions does not generalize
+[postcomposition of functions](foundation-core.postcomposition-functions.md) in
+the same way that
+[precomposition of dependent functions](foundation-core.precomposition-dependent-functions.md)
+generalizes
+[precomposition of functions](foundation-core.precomposition-functions.md). If
+`A` can vary while keeping `f` fixed, we have necessarily reduced to the case of
+[postcomposition of functions](foundation-core.postcomposition-functions.md).
+
+## Definitions
+
+### Postcomposition of dependent functions
+
+```agda
+module _
+  {l1 l2 l3 : Level} (A : UU l1) {X : A → UU l2} {Y : A → UU l3}
+  where
+
+  postcomp-Π : ({a : A} → X a → Y a) → ((a : A) → X a) → ((a : A) → Y a)
+  postcomp-Π f = f ∘_
+```

src/foundation-core/postcomposition-functions.lagda.md

@@ -7,8 +7,9 @@ module foundation-core.postcomposition-functions where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.postcomposition-dependent-functions
 open import foundation.universe-levels
+
+open import foundation-core.postcomposition-dependent-functions
 ```
 
 </details>

src/foundation-core/retractions.lagda.md

@@ -75,24 +75,39 @@ identifications.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B)
+  (r : B → A) (H : r ∘ i ~ id)
+  where
+
+  is-injective-has-retraction :
+    {x y : A} → i x ＝ i y → x ＝ y
+  is-injective-has-retraction {x} {y} p = inv (H x) ∙ (ap r p ∙ H y)
+
+  is-retraction-is-injective-has-retraction :
+    {x y : A} → is-injective-has-retraction ∘ ap i {x} {y} ~ id
+  is-retraction-is-injective-has-retraction {x} refl = left-inv (H x)
+
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (i : A → B) (R : retraction i)
   where
 
-  ap-retraction :
-    (i : A → B) (r : B → A) (H : r ∘ i ~ id)
-    (x y : A) → i x ＝ i y → x ＝ y
-  ap-retraction i r H x y p =
-      ( inv (H x)) ∙ ((ap r p) ∙ (H y))
-
-  is-retraction-ap-retraction :
-    (i : A → B) (r : B → A) (H : r ∘ i ~ id)
-    (x y : A) → ((ap-retraction i r H x y) ∘ (ap i {x} {y})) ~ id
-  is-retraction-ap-retraction i r H x .x refl = left-inv (H x)
-
-  retraction-ap :
-    (i : A → B) → retraction i → (x y : A) → retraction (ap i {x} {y})
-  pr1 (retraction-ap i (pair r H) x y) = ap-retraction i r H x y
-  pr2 (retraction-ap i (pair r H) x y) = is-retraction-ap-retraction i r H x y
+  is-injective-retraction :
+    {x y : A} → i x ＝ i y → x ＝ y
+  is-injective-retraction =
+    is-injective-has-retraction i
+      ( map-retraction i R)
+      ( is-retraction-map-retraction i R)
+
+  is-retraction-is-injective-retraction :
+    {x y : A} → is-injective-retraction ∘ ap i {x} {y} ~ id
+  is-retraction-is-injective-retraction =
+    is-retraction-is-injective-has-retraction i
+      ( map-retraction i R)
+      ( is-retraction-map-retraction i R)
+
+  retraction-ap : {x y : A} → retraction (ap i {x} {y})
+  pr1 retraction-ap = is-injective-retraction
+  pr2 retraction-ap = is-retraction-is-injective-retraction
 ```
 
 ### Composites of retractions are retractions

src/foundation-core/transport-along-identifications.lagda.md

@@ -120,7 +120,7 @@ tr-Id-left refl p = refl
 tr-Id-right :
   {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : a ＝ b) →
   tr (a ＝_) q p ＝ (p ∙ q)
-tr-Id-right refl refl = refl
+tr-Id-right refl p = inv right-unit
 ```
 
 ### Substitution law for transport

src/foundation/equivalences.lagda.md

@@ -238,14 +238,14 @@ module _
 Consider a commuting diagram of maps
 
 ```text
-       i
-    A ---> X
-    |    ∧ |
-    |   /  |
-  f |  h   | g
-    V /    V
-    B ---> Y
-       j
+         i
+    A ------> X
+    |       ∧ |
+  f |     /   | g
+    |   h     |
+    ∨ /       ∨
+    B ------> Y.
+         j
 ```
 
 The **6-for-2 property of equivalences** asserts that if `i` and `j` are

src/foundation/functoriality-cartesian-product-types.lagda.md

@@ -224,9 +224,9 @@ module _
   (f : A → C) (g : B → D)
   where
 
-  is-equiv-left-factor-is-equiv-map-product-is-inhabited-right-factor' :
-    (d : D) → is-equiv (map-product f g) → is-equiv f
-  is-equiv-left-factor-is-equiv-map-product-is-inhabited-right-factor'
+  is-equiv-left-factor-is-equiv-map-product' :
+    D → is-equiv (map-product f g) → is-equiv f
+  is-equiv-left-factor-is-equiv-map-product'
     d is-equiv-fg =
     is-equiv-is-contr-map
       ( λ x →
@@ -239,9 +239,9 @@ module _
             ( is-equiv-map-compute-fiber-map-product f g (x , d))
             ( is-contr-map-is-equiv is-equiv-fg (x , d))))
 
-  is-equiv-right-factor-is-equiv-map-product-is-inhabited-left-factor' :
-    (c : C) → is-equiv (map-product f g) → is-equiv g
-  is-equiv-right-factor-is-equiv-map-product-is-inhabited-left-factor'
+  is-equiv-right-factor-is-equiv-map-product' :
+    C → is-equiv (map-product f g) → is-equiv g
+  is-equiv-right-factor-is-equiv-map-product'
     c is-equiv-fg =
     is-equiv-is-contr-map
       ( λ y →

src/foundation/mere-embeddings.lagda.md

@@ -67,12 +67,12 @@ transitive-leq-Large-Preorder mere-emb-Large-Preorder X Y Z =
 ```agda
 antisymmetric-mere-emb :
   {l1 l2 : Level} {X : UU l1} {Y : UU l2} →
-  (LEM (l1 ⊔ l2)) → mere-emb X Y → mere-emb Y X → mere-equiv X Y
+  LEM (l1 ⊔ l2) → mere-emb X Y → mere-emb Y X → mere-equiv X Y
 antisymmetric-mere-emb lem f g =
   apply-universal-property-trunc-Prop f
-    (mere-equiv-Prop _ _)
-    λ f' →
+    ( mere-equiv-Prop _ _)
+    ( λ f' →
       apply-universal-property-trunc-Prop g
-      (mere-equiv-Prop _ _)
-      λ g' → unit-trunc-Prop (Cantor-Schröder-Bernstein-Escardó lem f' g')
+        ( mere-equiv-Prop _ _)
+        ( λ g' → unit-trunc-Prop (Cantor-Schröder-Bernstein-Escardó lem f' g')))
 ```