Apartness for real numbers (#1296)

Apartness from 0, for example, implies a real is multiplicatively
invertible.

---------

Co-authored-by: Fredrik Bakke <[email protected]>

src/foundation.lagda.md

@@ -257,6 +257,7 @@ open import foundation.iterating-families-of-maps public
 open import foundation.iterating-functions public
 open import foundation.iterating-involutions public
 open import foundation.kernel-span-diagrams-of-maps public
+open import foundation.large-apartness-relations public
 open import foundation.large-binary-relations public
 open import foundation.large-dependent-pair-types public
 open import foundation.large-homotopies public

src/foundation/large-apartness-relations.lagda.md

@@ -0,0 +1,102 @@
+# Large apartness relations
+
+```agda
+module foundation.large-apartness-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.disjunction
+open import foundation.identity-types
+open import foundation.large-binary-relations
+open import foundation.negated-equality
+open import foundation.negation
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "large apartness relation" WD="apartness relation" WDID=Q4779193 Agda=Large-Apartness-Relation}}
+on a family of types indexed by universe levels `A` is a
+[large binary relation](foundation.large-binary-relations.md) `R` which is
+
+- **Antireflexive:** For any `a : A` we have `¬ (R a a)`
+- **Symmetric:** For any `a b : A` we have `R a b → R b a`
+- **Cotransitive:** For any `a b c : A` we have `R a b → R a c ∨ R b c`.
+
+This is analogous to the notion of small
+[apartness relations](foundation.apartness-relations.md).
+
+## Definitions
+
+```agda
+record Large-Apartness-Relation
+  {α : Level → Level} (β : Level → Level → Level)
+  (A : (l : Level) → UU (α l)) : UUω
+  where
+
+  field
+    apart-prop-Large-Apartness-Relation : Large-Relation-Prop β A
+    antirefl-Large-Apartness-Relation :
+      is-antireflexive-Large-Relation-Prop A apart-prop-Large-Apartness-Relation
+    symmetric-Large-Apartness-Relation :
+      is-symmetric-Large-Relation-Prop A apart-prop-Large-Apartness-Relation
+    cotransitive-Large-Apartness-Relation :
+      is-cotransitive-Large-Relation-Prop A apart-prop-Large-Apartness-Relation
+
+  apart-Large-Apartness-Relation : Large-Relation β A
+  apart-Large-Apartness-Relation a b =
+    type-Prop (apart-prop-Large-Apartness-Relation a b)
+
+  consistent-Large-Apartness-Relation :
+    {l : Level} →
+    (a b : A l) →
+    a ＝ b → ¬ (apart-Large-Apartness-Relation a b)
+  consistent-Large-Apartness-Relation a .a refl =
+    antirefl-Large-Apartness-Relation a
+
+open Large-Apartness-Relation public
+```
+
+### Type families equipped with large apartness relations
+
+```agda
+record Type-Family-With-Large-Apartness
+  (α : Level → Level) (β : Level → Level → Level) : UUω
+  where
+
+  field
+    type-family-Type-Family-With-Large-Apartness : (l : Level) → UU (α l)
+    large-apartness-relation-Type-Family-With-Large-Apartness :
+      Large-Apartness-Relation β type-family-Type-Family-With-Large-Apartness
+
+  large-rel-Type-Family-With-Large-Apartness :
+    Large-Relation-Prop β type-family-Type-Family-With-Large-Apartness
+  large-rel-Type-Family-With-Large-Apartness =
+    Large-Apartness-Relation.apart-prop-Large-Apartness-Relation
+      large-apartness-relation-Type-Family-With-Large-Apartness
+
+open Type-Family-With-Large-Apartness public
+```
+
+## Properties
+
+### If two elements are apart, then they are nonequal
+
+```agda
+module _
+  {α : Level → Level} {β : Level → Level → Level}
+  {A : (l : Level) → UU (α l)} (R : Large-Apartness-Relation β A)
+  where
+
+  nonequal-apart-Large-Apartness-Relation :
+    {l : Level} {a b : A l} → apart-Large-Apartness-Relation R a b → a ≠ b
+  nonequal-apart-Large-Apartness-Relation {a = a} p refl =
+    antirefl-Large-Apartness-Relation R a p
+```

src/foundation/large-binary-relations.lagda.md

@@ -8,10 +8,13 @@ module foundation.large-binary-relations where
 
 ```agda
 open import foundation.binary-relations
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.disjunction
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
+open import foundation-core.negation
 open import foundation-core.propositions
 ```
 
@@ -125,6 +128,10 @@ module _
   is-antisymmetric-Large-Relation =
     {l : Level} → is-antisymmetric (relation-Large-Relation A R l)
 
+  is-antireflexive-Large-Relation : UUω
+  is-antireflexive-Large-Relation =
+    {l : Level} → (a : A l) → ¬ (R a a)
+
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (A : (l : Level) → UU (α l))
@@ -146,6 +153,17 @@ module _
   is-antisymmetric-Large-Relation-Prop : UUω
   is-antisymmetric-Large-Relation-Prop =
     is-antisymmetric-Large-Relation A (large-relation-Large-Relation-Prop A R)
+
+  is-antireflexive-Large-Relation-Prop : UUω
+  is-antireflexive-Large-Relation-Prop =
+    is-antireflexive-Large-Relation A (large-relation-Large-Relation-Prop A R)
+
+  is-cotransitive-Large-Relation-Prop : UUω
+  is-cotransitive-Large-Relation-Prop =
+    {l1 l2 l3 : Level} →
+    (a : A l1) (b : A l2) (c : A l3) →
+    type-Prop (R a b) →
+    type-Prop ((R a c) ∨ (R c b))
 ```
 
 ## See also

src/real-numbers.lagda.md

@@ -5,6 +5,7 @@
 ```agda
 module real-numbers where
 
+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.inequality-real-numbers public

src/real-numbers/apartness-real-numbers.lagda.md

@@ -0,0 +1,109 @@
+# Apartness of real numbers
+
+```agda
+module real-numbers.apartness-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.apartness-relations
+open import foundation.disjunction
+open import foundation.empty-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.large-apartness-relations
+open import foundation.large-binary-relations
+open import foundation.negated-equality
+open import foundation.negation
+open import foundation.propositions
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.strict-inequality-real-numbers
+```
+
+</details>
+
+## Idea
+
+Two [real numbers](real-numbers.dedekind-real-numbers.md) are
+[apart](foundation.large-apartness-relations.md) if one is
+[strictly less](real-numbers.strict-inequality-real-numbers.md) than the other.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (x : ℝ l1)
+  (y : ℝ l2)
+  where
+
+  apart-ℝ-Prop : Prop (l1 ⊔ l2)
+  apart-ℝ-Prop = le-ℝ-Prop x y ∨ le-ℝ-Prop y x
+
+  apart-ℝ : UU (l1 ⊔ l2)
+  apart-ℝ = type-Prop apart-ℝ-Prop
+```
+
+## Properties
+
+### Apartness is antireflexive
+
+```agda
+antireflexive-apart-ℝ : {l : Level} → (x : ℝ l) → ¬ (apart-ℝ x x)
+antireflexive-apart-ℝ x =
+  elim-disjunction empty-Prop (irreflexive-le-ℝ x) (irreflexive-le-ℝ x)
+```
+
+### Apartness is symmetric
+
+```agda
+symmetric-apart-ℝ :
+  {l1 l2 : Level} → (x : ℝ l1) (y : ℝ l2) → apart-ℝ x y → apart-ℝ y x
+symmetric-apart-ℝ x y =
+  elim-disjunction (apart-ℝ-Prop y x) inr-disjunction inl-disjunction
+```
+
+### Apartness is cotransitive
+
+```agda
+cotransitive-apart-ℝ : is-cotransitive-Large-Relation-Prop ℝ apart-ℝ-Prop
+cotransitive-apart-ℝ x y z =
+  elim-disjunction
+    ( apart-ℝ-Prop x z ∨ apart-ℝ-Prop z y)
+    ( λ x<y →
+      elim-disjunction
+        ( apart-ℝ-Prop x z ∨ apart-ℝ-Prop z y)
+        ( inl-disjunction ∘ inl-disjunction)
+        ( inr-disjunction ∘ inl-disjunction)
+        ( cotransitive-le-ℝ x y z x<y))
+    ( λ y<x →
+      elim-disjunction
+        ( apart-ℝ-Prop x z ∨ apart-ℝ-Prop z y)
+        ( inr-disjunction ∘ inr-disjunction)
+        ( inl-disjunction ∘ inr-disjunction)
+        ( cotransitive-le-ℝ y x z y<x))
+```
+
+### Apartness on the reals is a large apartness relation
+
+```agda
+large-apartness-relation-ℝ : Large-Apartness-Relation _⊔_ ℝ
+apart-prop-Large-Apartness-Relation large-apartness-relation-ℝ =
+  apart-ℝ-Prop
+antirefl-Large-Apartness-Relation large-apartness-relation-ℝ =
+  antireflexive-apart-ℝ
+symmetric-Large-Apartness-Relation large-apartness-relation-ℝ =
+  symmetric-apart-ℝ
+cotransitive-Large-Apartness-Relation large-apartness-relation-ℝ =
+  cotransitive-apart-ℝ
+```
+
+### Apart real numbers are nonequal
+
+```agda
+nonequal-apart-ℝ : {l : Level} (x y : ℝ l) → apart-ℝ x y → x ≠ y
+nonequal-apart-ℝ x y =
+  nonequal-apart-Large-Apartness-Relation large-apartness-relation-ℝ
+```

src/real-numbers/strict-inequality-real-numbers.lagda.md

@@ -21,6 +21,7 @@ open import foundation.empty-types
 open import foundation.existential-quantification
 open import foundation.function-types
 open import foundation.identity-types
+open import foundation.large-binary-relations
 open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositions
@@ -46,20 +47,14 @@ presence of a [rational number](elementary-number-theory.rational-numbers.md)
 between them. This is the definition used in {{#cite UF13}}, section 11.2.1.
 
 ```agda
-module _
-  {l1 l2 : Level}
-  (x : ℝ l1)
-  (y : ℝ l2)
-  where
+le-ℝ-Prop : Large-Relation-Prop _⊔_ ℝ
+le-ℝ-Prop x y = ∃ ℚ (λ q → upper-cut-ℝ x q ∧ lower-cut-ℝ y q)
 
-  le-ℝ-Prop : Prop (l1 ⊔ l2)
-  le-ℝ-Prop = ∃ ℚ (λ q → upper-cut-ℝ x q ∧ lower-cut-ℝ y q)
+le-ℝ : Large-Relation _⊔_ ℝ
+le-ℝ x y = type-Prop (le-ℝ-Prop x y)
 
-  le-ℝ : UU (l1 ⊔ l2)
-  le-ℝ = type-Prop le-ℝ-Prop
-
-  is-prop-le-ℝ : is-prop le-ℝ
-  is-prop-le-ℝ = is-prop-type-Prop le-ℝ-Prop
+is-prop-le-ℝ : {l1 l2 : Level} → (x : ℝ l1) (y : ℝ l2) → is-prop (le-ℝ x y)
+is-prop-le-ℝ x y = is-prop-type-Prop (le-ℝ-Prop x y)
 ```
 
 ## Properties
@@ -377,6 +372,25 @@ module _
           ( forward-implication (is-rounded-lower-cut-ℝ y q) q∈ly))
 ```
 
+### Strict inequality on the real numbers is cotransitive
+
+```agda
+cotransitive-le-ℝ : is-cotransitive-Large-Relation-Prop ℝ le-ℝ-Prop
+cotransitive-le-ℝ x y z =
+  elim-exists
+    ( le-ℝ-Prop x z ∨ le-ℝ-Prop z y)
+    ( λ q (x<q , q<y) →
+      elim-exists
+        ( le-ℝ-Prop x z ∨ le-ℝ-Prop z y)
+        ( λ p (p<q , x<p) →
+          elim-disjunction
+            ( le-ℝ-Prop x z ∨ le-ℝ-Prop z y)
+            ( λ p<z → inl-disjunction (intro-exists p (x<p , p<z)))
+            ( λ z<q → inr-disjunction (intro-exists q (z<q , q<y)))
+            ( is-located-lower-upper-cut-ℝ z p q p<q))
+        ( forward-implication (is-rounded-upper-cut-ℝ x q) x<q))
+```
+
 ## References
 
 {{#bibliography}}