resolve merge conflict

src/elementary-number-theory/2-adic-decomposition.lagda.md

@@ -22,15 +22,18 @@ open import elementary-number-theory.strong-induction-natural-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
+open import foundation.embeddings
 open import foundation.equality-cartesian-product-types
 open import foundation.equality-dependent-pair-types
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
+open import foundation.propositional-maps
 open import foundation.propositions
 open import foundation.sets
 open import foundation.split-surjective-maps
 open import foundation.subtypes
 open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -363,3 +366,32 @@ is-contr-2-adic-decomposition-ℕ n H =
     ( is-prop-2-adic-decomposition-ℕ n)
     ( 2-adic-decomposition-is-nonzero-ℕ n H)
 ```
+
+### The 2-adic composition function is a propositional map
+
+```agda
+is-prop-map-2-adic-composition-ℕ :
+  is-prop-map (λ x → 2-adic-composition-ℕ (pr1 x) (pr2 x))
+is-prop-map-2-adic-composition-ℕ n =
+  is-prop-equiv
+    ( associative-Σ ℕ _ _)
+    ( is-prop-2-adic-decomposition-ℕ n)
+```
+
+### The 2-adic composition function is an embedding
+
+```agda
+is-emb-2-adic-composition-ℕ :
+  is-emb (λ x → 2-adic-composition-ℕ (pr1 x) (pr2 x))
+is-emb-2-adic-composition-ℕ =
+  is-emb-is-prop-map is-prop-map-2-adic-composition-ℕ
+```
+
+### The 2-adic composition function is injective
+
+```agda
+is-injective-2-adic-composition-ℕ :
+  is-injective (λ x → 2-adic-composition-ℕ (pr1 x) (pr2 x))
+is-injective-2-adic-composition-ℕ =
+  is-injective-is-emb is-emb-2-adic-composition-ℕ
+```

src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md

@@ -348,18 +348,18 @@ le-succ-leq-ℕ (succ-ℕ x) (succ-ℕ y) H = le-succ-leq-ℕ x y H
 
 ```agda
 eq-or-le-leq-ℕ :
-  (x y : ℕ) → x ≤-ℕ y → ((x ＝ y) + (x <-ℕ y))
+  (x y : ℕ) → x ≤-ℕ y → ((x ＝ y) + x <-ℕ y)
 eq-or-le-leq-ℕ zero-ℕ zero-ℕ H = inl refl
 eq-or-le-leq-ℕ zero-ℕ (succ-ℕ y) H = inr star
 eq-or-le-leq-ℕ (succ-ℕ x) (succ-ℕ y) H =
   map-coproduct (ap succ-ℕ) id (eq-or-le-leq-ℕ x y H)
 
 eq-or-le-leq-ℕ' :
-  (x y : ℕ) → x ≤-ℕ y → ((y ＝ x) + (x <-ℕ y))
+  (x y : ℕ) → x ≤-ℕ y → ((y ＝ x) + x <-ℕ y)
 eq-or-le-leq-ℕ' x y H = map-coproduct inv id (eq-or-le-leq-ℕ x y H)
 
 leq-eq-or-le-ℕ :
-  (x y : ℕ) → ((x ＝ y) + (x <-ℕ y)) → x ≤-ℕ y
+  (x y : ℕ) → ((x ＝ y) + x <-ℕ y) → x ≤-ℕ y
 leq-eq-or-le-ℕ x .x (inl refl) = refl-leq-ℕ x
 leq-eq-or-le-ℕ x y (inr l) = leq-le-ℕ x y l
 ```
@@ -374,6 +374,15 @@ le-leq-neq-ℕ {succ-ℕ x} {succ-ℕ y} l f =
   le-leq-neq-ℕ {x} {y} l (λ p → f (ap succ-ℕ p))
 ```
 
+### For any two natural numbers `x` and `y`, either `x < y` or `y ≤ x`
+
+```agda
+decide-le-leq-ℕ : (x y : ℕ) → x <-ℕ y + y ≤-ℕ x
+decide-le-leq-ℕ x zero-ℕ = inr star
+decide-le-leq-ℕ zero-ℕ (succ-ℕ _) = inl star
+decide-le-leq-ℕ (succ-ℕ x) (succ-ℕ y) = decide-le-leq-ℕ x y
+```
+
 ### `x < x + y` for any nonzero natural number `y`
 
 ```agda

src/elementary-number-theory/type-arithmetic-natural-numbers.lagda.md

@@ -16,6 +16,7 @@ open import elementary-number-theory.parity-natural-numbers
 open import elementary-number-theory.2-adic-decomposition
 
 open import foundation.action-on-identifications-functions
+open import foundation.contractible-maps
 open import foundation.dependent-pair-types
 open import foundation.function-types
 open import foundation.functoriality-cartesian-product-types
@@ -167,14 +168,28 @@ equiv-iterated-coproduct-ℕ (succ-ℕ n) =
 
 ### The product `ℕ × ℕ` is equivalent to `ℕ`
 
-A pairing function is a bijection between `ℕ × ℕ` and `ℕ`.
-
-## Definition
+The [2-adic composition map](elementary-number-theory.2-adic-decomposition.md) $\mathbb{N}\times\mathbb{N} \to \mathbb{N}$ is an [embedding](foundation-core.embeddings.md) which fits in a [commuting triangle](foundation-core.commuting-triangles-of-maps.md)
 
 ```text
-pairing-map : ℕ × ℕ → ℕ
-pairing-map (u , v) =
-  pr1 (is-successor-is-nonzero-ℕ (is-nonzero-pair-expansion u v))
+                  ℕ × ℕ -----> ℕ
+                      \       /
+  2-adic-composition-ℕ \     / succ-ℕ
+                        \   /
+                         ∨ ∨
+                          ℕ.
+```
+
+Since the [image](foundation.images.md) of the 2-adic composition function consists precisely of the [nonzero natural numbers](elementary-number-theory.nonzero-natural-numbers.md), the top map in this triangle is an equivalence.
+
+```agda
+pairing-map-ℕ : ℕ × ℕ → ℕ
+pairing-map-ℕ (u , v) =
+  pr1 (is-successor-is-nonzero-ℕ (is-nonzero-2-adic-composition-ℕ u v))
+
+compute-succ-pairing-map-ℕ :
+  (x : ℕ × ℕ) → succ-ℕ (pairing-map-ℕ x) ＝ 2-adic-composition-ℕ (pr1 x) (pr2 x)
+compute-succ-pairing-map-ℕ (u , v) =
+  inv (pr2 (is-successor-is-nonzero-ℕ (is-nonzero-2-adic-composition-ℕ u v)))
 ```
 
 ### Pairing function is split surjective
@@ -220,7 +235,7 @@ is-equiv-pairing-map =
     is-split-surjective-pairing-map
 ```
 
-```agda
+```text
 ℕ×ℕ≃ℕ : (ℕ × ℕ) ≃ ℕ
 ℕ×ℕ≃ℕ = pair pairing-map is-equiv-pairing-map
 
@@ -233,7 +248,7 @@ is-equiv-map-ℕ-to-ℕ×ℕ = is-equiv-map-inv-is-equiv (pr2 ℕ×ℕ≃ℕ)
 
 ### The iterated coproduct `ℕ × ℕ × ... × ℕ` is equivalent to `ℕ` for any n
 
-```agda
+```text
 equiv-iterated-product-ℕ :
   (n : ℕ) → (iterate n (_×_ ℕ) ℕ) ≃ ℕ
 equiv-iterated-product-ℕ zero-ℕ = id-equiv

src/foundation/complements-subtypes.lagda.md

@@ -77,3 +77,19 @@ neg-hom-powerset =
     ( λ P x → neg-Prop (P x))
     ( λ P Q f x → map-neg (f x))
 ```
+
+### Complementation reverses the containment order on subsets
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  {A : UU l1}
+  (B : subtype l2 A)
+  (C : subtype l3 A)
+  where
+
+  reverses-order-complement-subtype :
+    B ⊆ C →
+    complement-subtype C ⊆ complement-subtype B
+  reverses-order-complement-subtype B⊆C x x∉C x∈B = x∉C (B⊆C x x∈B)
+```

src/group-theory/abelian-groups.lagda.md

@@ -256,9 +256,21 @@ module _
   {l : Level} (A : Ab l)
   where
 
+  equiv-left-conjugation-Ab : (x : type-Ab A) → type-Ab A ≃ type-Ab A
+  equiv-left-conjugation-Ab = equiv-left-conjugation-Group (group-Ab A)
+
+  equiv-right-conjugation-Ab : (x : type-Ab A) → type-Ab A ≃ type-Ab A
+  equiv-right-conjugation-Ab = equiv-right-conjugation-Group (group-Ab A)
+
   equiv-conjugation-Ab : (x : type-Ab A) → type-Ab A ≃ type-Ab A
   equiv-conjugation-Ab = equiv-conjugation-Group (group-Ab A)
 
+  left-conjugation-Ab : (x : type-Ab A) → type-Ab A → type-Ab A
+  left-conjugation-Ab = left-conjugation-Group (group-Ab A)
+
+  right-conjugation-Ab : (x : type-Ab A) → type-Ab A → type-Ab A
+  right-conjugation-Ab = right-conjugation-Group (group-Ab A)
+
   conjugation-Ab : (x : type-Ab A) → type-Ab A → type-Ab A
   conjugation-Ab = conjugation-Group (group-Ab A)
 
@@ -267,6 +279,10 @@ module _
 
   conjugation-Ab' : (x : type-Ab A) → type-Ab A → type-Ab A
   conjugation-Ab' = conjugation-Group' (group-Ab A)
+
+  left-right-conjugation-Ab :
+    (x : type-Ab A) → left-conjugation-Ab x ~ right-conjugation-Ab x
+  left-right-conjugation-Ab = left-right-conjugation-Group (group-Ab A)
 ```
 
 ### Commutators in an abelian group
@@ -596,11 +612,21 @@ module _
   {l : Level} (A : Ab l)
   where
 
-  is-identity-conjugation-Ab :
-    (x : type-Ab A) → conjugation-Ab A x ~ id
-  is-identity-conjugation-Ab x y =
+  is-identity-left-conjugation-Ab :
+    (x : type-Ab A) → left-conjugation-Ab A x ~ id
+  is-identity-left-conjugation-Ab x y =
     ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙
     ( is-retraction-right-subtraction-Ab A x y)
+
+  is-identity-right-conjugation-Ab :
+    (x : type-Ab A) → right-conjugation-Ab A x ~ id
+  is-identity-right-conjugation-Ab x =
+    inv-htpy (left-right-conjugation-Ab A x) ∙h
+    is-identity-left-conjugation-Ab x
+
+  is-identity-conjugation-Ab :
+    (x : type-Ab A) → conjugation-Ab A x ~ id
+  is-identity-conjugation-Ab = is-identity-left-conjugation-Ab
 ```
 
 ### Laws for conjugation and addition

src/group-theory/conjugation.lagda.md

@@ -51,12 +51,27 @@ module _
   {l : Level} (G : Group l)
   where
 
-  equiv-conjugation-Group : (x : type-Group G) → type-Group G ≃ type-Group G
-  equiv-conjugation-Group x =
+  equiv-left-conjugation-Group :
+    (x : type-Group G) → type-Group G ≃ type-Group G
+  equiv-left-conjugation-Group x =
     equiv-mul-Group' G (inv-Group G x) ∘e equiv-mul-Group G x
 
+  equiv-right-conjugation-Group :
+    (x : type-Group G) → type-Group G ≃ type-Group G
+  equiv-right-conjugation-Group x =
+    equiv-mul-Group G x ∘e equiv-mul-Group' G (inv-Group G x)
+
+  equiv-conjugation-Group : (x : type-Group G) → type-Group G ≃ type-Group G
+  equiv-conjugation-Group = equiv-left-conjugation-Group
+
+  left-conjugation-Group : (x : type-Group G) → type-Group G → type-Group G
+  left-conjugation-Group x = map-equiv (equiv-left-conjugation-Group x)
+
+  right-conjugation-Group : (x : type-Group G) → type-Group G → type-Group G
+  right-conjugation-Group x = map-equiv (equiv-right-conjugation-Group x)
+
   conjugation-Group : (x : type-Group G) → type-Group G → type-Group G
-  conjugation-Group x = map-equiv (equiv-conjugation-Group x)
+  conjugation-Group = left-conjugation-Group
 
   equiv-conjugation-Group' : (x : type-Group G) → type-Group G ≃ type-Group G
   equiv-conjugation-Group' x =
@@ -66,6 +81,19 @@ module _
   conjugation-Group' x = map-equiv (equiv-conjugation-Group' x)
 ```
 
+### Left and right conjugation are equivalent
+
+```agda
+module _
+  {l : Level} (G : Group l)
+  where
+
+  left-right-conjugation-Group :
+    (x : type-Group G) →
+    left-conjugation-Group G x ~ right-conjugation-Group G x
+  left-right-conjugation-Group x y = associative-mul-Group G x y (inv-Group G x)
+```
+
 ### The conjugation action of a group on itself
 
 ```agda

src/group-theory/groups.lagda.md

@@ -495,6 +495,38 @@ module _
   is-unit-right-div-eq-Group refl = right-inverse-law-mul-Group G _
 ```
 
+### If `xy = 1`, `y ＝ x⁻¹`
+
+```agda
+  unique-right-inv-Group :
+    (x y : type-Group G) →
+    is-unit-Group G (mul-Group G x y) →
+    y ＝ inv-Group G x
+  unique-right-inv-Group x y xy=1 =
+    equational-reasoning
+      y
+      ＝ left-div-Group x (unit-Group G)
+        by transpose-eq-mul-Group' xy=1
+      ＝ inv-Group G x
+        by right-unit-law-mul-Group G (inv-Group G x)
+```
+
+### If `xy = 1`, `x ＝ y⁻¹`
+
+```agda
+  unique-left-inv-Group :
+    (x y : type-Group G) →
+    is-unit-Group G (mul-Group G x y) →
+    x ＝ inv-Group G y
+  unique-left-inv-Group x y xy=1 =
+    equational-reasoning
+      x
+      ＝ right-div-Group (unit-Group G) y
+        by transpose-eq-mul-Group xy=1
+      ＝ inv-Group G y
+        by left-unit-law-mul-Group G (inv-Group G y)
+```
+
 ### The inverse of `x⁻¹y` is `y⁻¹x`
 
 ```agda

src/real-numbers.lagda.md

@@ -10,4 +10,5 @@ open import real-numbers.dedekind-real-numbers public
 open import real-numbers.metric-space-of-real-numbers public
 open import real-numbers.negation-real-numbers public
 open import real-numbers.rational-real-numbers public
+open import real-numbers.strict-inequality-real-numbers public
 ```