Addition on real numbers (#1336)

Decided I'm just going to fold it all together.  Depends on #1306.

Author: lowasser

src/elementary-number-theory/addition-rational-numbers.lagda.md

@@ -13,6 +13,7 @@ open import elementary-number-theory.addition-integer-fractions
 open import elementary-number-theory.addition-integers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
+open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.reduced-integer-fractions
 
@@ -161,6 +162,21 @@ abstract
     commutative-add-ℚ x (neg-ℚ x) ∙ left-inverse-law-add-ℚ x
 ```
 
+### If `p + q = 0`, then `p = -q`
+
+```agda
+abstract
+  unique-left-neg-ℚ : (p q : ℚ) → p +ℚ q ＝ zero-ℚ → p ＝ neg-ℚ q
+  unique-left-neg-ℚ p q p+q=0 =
+    equational-reasoning
+      p
+      ＝ p +ℚ zero-ℚ by inv (right-unit-law-add-ℚ p)
+      ＝ p +ℚ (q +ℚ neg-ℚ q) by ap (p +ℚ_) (inv (right-inverse-law-add-ℚ q))
+      ＝ (p +ℚ q) +ℚ neg-ℚ q by inv (associative-add-ℚ _ _ _)
+      ＝ zero-ℚ +ℚ neg-ℚ q by ap (_+ℚ neg-ℚ q) p+q=0
+      ＝ neg-ℚ q by left-unit-law-add-ℚ _
+```
+
 ### The negatives of rational numbers distribute over addition
 
 ```agda
@@ -276,6 +292,15 @@ abstract
   succ-rational-ℤ = add-rational-ℤ one-ℤ
 ```
 
+### The embedding of the successor of a natural number is the successor of its embedding
+
+```agda
+abstract
+  succ-rational-int-ℕ :
+    (n : ℕ) → succ-ℚ (rational-ℤ (int-ℕ n)) ＝ rational-ℤ (int-ℕ (succ-ℕ n))
+  succ-rational-int-ℕ n = succ-rational-ℤ _ ∙ ap rational-ℤ (succ-int-ℕ n)
+```
+
 ## See also
 
 - The additive group structure on the rational numbers is defined in

src/elementary-number-theory/positive-rational-numbers.lagda.md

@@ -205,13 +205,14 @@ module _
   (x y : ℚ) (H : le-ℚ x y)
   where
 
-  is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x)
-  is-positive-diff-le-ℚ =
-    is-positive-le-zero-ℚ
-      ( y -ℚ x)
-      ( backward-implication
-        ( iff-translate-diff-le-zero-ℚ x y)
-        ( H))
+  abstract
+    is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x)
+    is-positive-diff-le-ℚ =
+      is-positive-le-zero-ℚ
+        ( y -ℚ x)
+        ( backward-implication
+          ( iff-translate-diff-le-zero-ℚ x y)
+          ( H))
 
   positive-diff-le-ℚ : ℚ⁺
   positive-diff-le-ℚ = y -ℚ x , is-positive-diff-le-ℚ
@@ -656,12 +657,13 @@ mediant-zero-ℚ⁺ x =
         ( rational-ℚ⁺ x)
         ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))))
 
-le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
-le-mediant-zero-ℚ⁺ x =
-  le-right-mediant-ℚ
-    ( zero-ℚ)
-    ( rational-ℚ⁺ x)
-    ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))
+abstract
+  le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
+  le-mediant-zero-ℚ⁺ x =
+    le-right-mediant-ℚ
+      ( zero-ℚ)
+      ( rational-ℚ⁺ x)
+      ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))
 ```
 
 ### Any positive rational number is the sum of two positive rational numbers
@@ -678,16 +680,40 @@ module _
   right-summand-split-ℚ⁺ =
     le-diff-ℚ⁺ (mediant-zero-ℚ⁺ x) x (le-mediant-zero-ℚ⁺ x)
 
-  eq-add-split-ℚ⁺ :
-    left-summand-split-ℚ⁺ +ℚ⁺ right-summand-split-ℚ⁺ ＝ x
-  eq-add-split-ℚ⁺ =
-    right-diff-law-add-ℚ⁺ (mediant-zero-ℚ⁺ x) x (le-mediant-zero-ℚ⁺ x)
+  abstract
+    eq-add-split-ℚ⁺ :
+      left-summand-split-ℚ⁺ +ℚ⁺ right-summand-split-ℚ⁺ ＝ x
+    eq-add-split-ℚ⁺ =
+      right-diff-law-add-ℚ⁺ (mediant-zero-ℚ⁺ x) x (le-mediant-zero-ℚ⁺ x)
 
   split-ℚ⁺ : Σ ℚ⁺ (λ u → Σ ℚ⁺ (λ v → u +ℚ⁺ v ＝ x))
   split-ℚ⁺ =
     left-summand-split-ℚ⁺ ,
     right-summand-split-ℚ⁺ ,
     eq-add-split-ℚ⁺
+
+  abstract
+    le-add-split-ℚ⁺ :
+      (p q r s : ℚ) →
+      le-ℚ p (q +ℚ rational-ℚ⁺ left-summand-split-ℚ⁺) →
+      le-ℚ r (s +ℚ rational-ℚ⁺ right-summand-split-ℚ⁺) →
+      le-ℚ (p +ℚ r) ((q +ℚ s) +ℚ rational-ℚ⁺ x)
+    le-add-split-ℚ⁺ p q r s p<q+left r<s+right =
+      tr
+        ( le-ℚ (p +ℚ r))
+        ( interchange-law-add-add-ℚ
+          ( q)
+          ( rational-ℚ⁺ left-summand-split-ℚ⁺)
+          ( s)
+          ( rational-ℚ⁺ right-summand-split-ℚ⁺) ∙
+          ap ((q +ℚ s) +ℚ_) (ap rational-ℚ⁺ eq-add-split-ℚ⁺))
+        ( preserves-le-add-ℚ
+          { p}
+          { q +ℚ rational-ℚ⁺ left-summand-split-ℚ⁺}
+          { r}
+          { s +ℚ rational-ℚ⁺ right-summand-split-ℚ⁺}
+          ( p<q+left)
+          ( r<s+right))
 ```
 
 ### Any two positive rational numbers have a positive rational number strictly less than both

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

@@ -127,12 +127,13 @@ module _
   (x y z : ℚ)
   where
 
-  transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z
-  transitive-le-ℚ =
-    transitive-le-fraction-ℤ
-      ( fraction-ℚ x)
-      ( fraction-ℚ y)
-      ( fraction-ℚ z)
+  abstract
+    transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z
+    transitive-le-ℚ =
+      transitive-le-fraction-ℤ
+        ( fraction-ℚ x)
+        ( fraction-ℚ y)
+        ( fraction-ℚ z)
 ```
 
 ### Concatenation rules for inequality and strict inequality on the rational numbers
@@ -320,15 +321,16 @@ module _
 ### Addition on the rational numbers preserves strict inequality
 
 ```agda
-preserves-le-add-ℚ :
-  {a b c d : ℚ} → le-ℚ a b → le-ℚ c d → le-ℚ (a +ℚ c) (b +ℚ d)
-preserves-le-add-ℚ {a} {b} {c} {d} H K =
-  transitive-le-ℚ
-    ( a +ℚ c)
-    ( b +ℚ c)
-    ( b +ℚ d)
-    ( preserves-le-right-add-ℚ b c d K)
-    ( preserves-le-left-add-ℚ c a b H)
+abstract
+  preserves-le-add-ℚ :
+    {a b c d : ℚ} → le-ℚ a b → le-ℚ c d → le-ℚ (a +ℚ c) (b +ℚ d)
+  preserves-le-add-ℚ {a} {b} {c} {d} H K =
+    transitive-le-ℚ
+      ( a +ℚ c)
+      ( b +ℚ c)
+      ( b +ℚ d)
+      ( preserves-le-right-add-ℚ b c d K)
+      ( preserves-le-left-add-ℚ c a b H)
 ```
 
 ### The rational numbers have no lower or upper bound

src/foundation.lagda.md

@@ -205,6 +205,7 @@ open import foundation.functoriality-cartesian-product-types public
 open import foundation.functoriality-coproduct-types public
 open import foundation.functoriality-dependent-function-types public
 open import foundation.functoriality-dependent-pair-types public
+open import foundation.functoriality-disjunction public
 open import foundation.functoriality-fibers-of-maps public
 open import foundation.functoriality-function-types public
 open import foundation.functoriality-morphisms-arrows public

src/foundation/functoriality-disjunction.lagda.md

@@ -0,0 +1,36 @@
+# Functoriality of disjunction
+
+```agda
+module foundation.functoriality-disjunction where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.disjunction
+open import foundation.function-types
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Any two implications `f : A ⇒ B` and `g : C ⇒ D` induce an implication
+`map-disjunction f g : (A ∨ B) ⇒ (C ∨ D)`.
+
+## Definitions
+
+### The functorial action of disjunction
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (A : Prop l1) (B : Prop l2) (C : Prop l3) (D : Prop l4)
+  (f : type-Prop (A ⇒ B)) (g : type-Prop (C ⇒ D))
+  where
+
+  map-disjunction : type-Prop ((A ∨ C) ⇒ (B ∨ D))
+  map-disjunction =
+    elim-disjunction (B ∨ D) (inl-disjunction ∘ f) (inr-disjunction ∘ g)
+```

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

@@ -612,17 +612,18 @@ module _
   {l : Level} (A : Ab l)
   where
 
-  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
+  abstract
+    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

src/logic/functoriality-existential-quantification.lagda.md

@@ -7,10 +7,11 @@ module logic.functoriality-existential-quantification where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.dependent-pair-types
 open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.logical-equivalences
 open import foundation.universe-levels
-
-open import foundation-core.function-types
 ```
 
 </details>
@@ -107,6 +108,19 @@ module _
   map-tot-exists g = map-exists C id g
 ```
 
+### The functorial action of existential quantification on families of logical equivalences
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
+  where
+
+  iff-tot-exists :
+    (g : (x : A) → B x ↔ C x) → exists-structure A B ↔ exists-structure A C
+  pr1 (iff-tot-exists g) = map-tot-exists (forward-implication ∘ g)
+  pr2 (iff-tot-exists g) = map-tot-exists (backward-implication ∘ g)
+```
+
 ### The functorial action of existential quantification on maps of the base
 
 ```agda

src/real-numbers.lagda.md

@@ -7,10 +7,12 @@ module real-numbers where
 
 open import real-numbers.absolute-value-real-numbers public
 open import real-numbers.addition-lower-dedekind-real-numbers public
+open import real-numbers.addition-real-numbers public
 open import real-numbers.addition-upper-dedekind-real-numbers public
 open import real-numbers.apartness-real-numbers public
 open import real-numbers.arithmetically-located-dedekind-cuts public
 open import real-numbers.dedekind-real-numbers public
+open import real-numbers.difference-real-numbers public
 open import real-numbers.inequality-lower-dedekind-real-numbers public
 open import real-numbers.inequality-real-numbers public
 open import real-numbers.inequality-upper-dedekind-real-numbers public