Standardize an "is zero" predicate on the real numbers

src/complex-numbers/complex-numbers.lagda.md

@@ -67,14 +67,14 @@ eq-ℂ = eq-pair
 
 ```agda
 complex-ℝ : {l : Level} → ℝ l → ℂ l
-complex-ℝ {l} a = (a , raise-ℝ l zero-ℝ)
+complex-ℝ {l} a = (a , raise-zero-ℝ l)
 ```
 
 ### The imaginary embedding of real numbers into the complex numbers
 
 ```agda
 im-complex-ℝ : {l : Level} → ℝ l → ℂ l
-im-complex-ℝ {l} a = (raise-ℝ l zero-ℝ , a)
+im-complex-ℝ {l} a = (raise-zero-ℝ l , a)
 ```
 
 ### The canonical embedding of Gaussian integers into the complex numbers

src/complex-numbers/magnitude-complex-numbers.lagda.md

@@ -239,7 +239,7 @@ abstract
   magnitude-complex-ℝ {l} x =
     equational-reasoning
       real-sqrt-ℝ⁰⁺
-        ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ (raise-ℝ l zero-ℝ))
+        ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ (raise-zero-ℝ l))
       ＝
         real-sqrt-ℝ⁰⁺
           ( nonnegative-square-ℝ x +ℝ⁰⁺ nonnegative-square-ℝ zero-ℝ)

src/linear-algebra/normed-real-vector-spaces.lagda.md

@@ -40,6 +40,7 @@ open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.saturation-inequality-nonnegative-real-numbers
 open import real-numbers.similarity-real-numbers
+open import real-numbers.zero-real-numbers
 ```
 
 </details>
@@ -68,16 +69,16 @@ module _
   {l1 l2 : Level} (V : ℝ-Vector-Space l1 l2) (p : seminorm-ℝ-Vector-Space V)
   where
 
-  is-norm-prop-seminorm-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-norm-prop-seminorm-ℝ-Vector-Space : Prop (l1 ⊔ l2)
   is-norm-prop-seminorm-ℝ-Vector-Space =
     Π-Prop
       ( type-ℝ-Vector-Space V)
       ( λ v →
         hom-Prop
-          ( Id-Prop (ℝ-Set l1) (pr1 p v) (raise-ℝ l1 zero-ℝ))
+          ( is-zero-prop-ℝ (pr1 p v))
           ( is-zero-prop-ℝ-Vector-Space V v))
 
-  is-norm-seminorm-ℝ-Vector-Space : UU (lsuc l1 ⊔ l2)
+  is-norm-seminorm-ℝ-Vector-Space : UU (l1 ⊔ l2)
   is-norm-seminorm-ℝ-Vector-Space =
     type-Prop is-norm-prop-seminorm-ℝ-Vector-Space
 
@@ -209,13 +210,13 @@ module _
 
   is-extensional-norm-Normed-ℝ-Vector-Space :
     (v : type-Normed-ℝ-Vector-Space) →
-    map-norm-Normed-ℝ-Vector-Space v ＝ raise-ℝ l1 zero-ℝ →
+    is-zero-ℝ (map-norm-Normed-ℝ-Vector-Space v) →
     v ＝ zero-Normed-ℝ-Vector-Space
   is-extensional-norm-Normed-ℝ-Vector-Space = pr2 norm-Normed-ℝ-Vector-Space
 
   is-extensional-dist-Normed-ℝ-Vector-Space :
     (v w : type-Normed-ℝ-Vector-Space) →
-    dist-Normed-ℝ-Vector-Space v w ＝ raise-ℝ l1 zero-ℝ →
+    is-zero-ℝ (dist-Normed-ℝ-Vector-Space v w) →
     v ＝ w
   is-extensional-dist-Normed-ℝ-Vector-Space v w |v-w|=0 =
     eq-is-zero-right-subtraction-Ab
@@ -224,11 +225,11 @@ module _
         ( diff-Normed-ℝ-Vector-Space v w)
         ( |v-w|=0))
 
-  commutative-dist-Normed-ℝ-Vector-Space :
+  symmetric-dist-Normed-ℝ-Vector-Space :
     (v w : type-Normed-ℝ-Vector-Space) →
     dist-Normed-ℝ-Vector-Space v w ＝ dist-Normed-ℝ-Vector-Space w v
-  commutative-dist-Normed-ℝ-Vector-Space =
-    commutative-dist-Seminormed-ℝ-Vector-Space
+  symmetric-dist-Normed-ℝ-Vector-Space =
+    symmetric-dist-Seminormed-ℝ-Vector-Space
       ( seminormed-vector-space-Normed-ℝ-Vector-Space)
 ```
 
@@ -241,28 +242,19 @@ module _
 
   refl-norm-Normed-ℝ-Vector-Space :
     (v : type-Normed-ℝ-Vector-Space V) →
-    sim-ℝ zero-ℝ (dist-Normed-ℝ-Vector-Space V v v)
-  refl-norm-Normed-ℝ-Vector-Space v =
-    inv-tr
-      ( sim-ℝ zero-ℝ)
-      ( is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space
-        ( seminormed-vector-space-Normed-ℝ-Vector-Space V)
-        ( v))
-      ( sim-raise-ℝ l1 zero-ℝ)
+    is-zero-ℝ (dist-Normed-ℝ-Vector-Space V v v)
+  refl-norm-Normed-ℝ-Vector-Space =
+    is-zero-diagonal-dist-Seminormed-ℝ-Vector-Space
+      ( seminormed-vector-space-Normed-ℝ-Vector-Space V)
 
   metric-Normed-ℝ-Vector-Space : Metric l1 (set-Normed-ℝ-Vector-Space V)
   metric-Normed-ℝ-Vector-Space =
     ( nonnegative-dist-Normed-ℝ-Vector-Space V ,
       refl-norm-Normed-ℝ-Vector-Space ,
-      ( λ v w → eq-ℝ⁰⁺ _ _ (commutative-dist-Normed-ℝ-Vector-Space V v w)) ,
+      ( λ v w → eq-ℝ⁰⁺ _ _ (symmetric-dist-Normed-ℝ-Vector-Space V v w)) ,
       triangular-dist-Seminormed-ℝ-Vector-Space
         ( seminormed-vector-space-Normed-ℝ-Vector-Space V) ,
-      ( λ v w 0~dvw →
-        is-extensional-dist-Normed-ℝ-Vector-Space V v w
-          ( eq-sim-ℝ
-            ( transitive-sim-ℝ _ _ _
-              ( sim-raise-ℝ l1 zero-ℝ)
-              ( symmetric-sim-ℝ 0~dvw)))))
+      is-extensional-dist-Normed-ℝ-Vector-Space V)
 
   metric-space-Normed-ℝ-Vector-Space : Metric-Space l2 l1
   metric-space-Normed-ℝ-Vector-Space =
@@ -287,7 +279,7 @@ normed-real-vector-space-ℝ :
 normed-real-vector-space-ℝ l =
   ( real-vector-space-ℝ l ,
     ( abs-ℝ , triangle-inequality-abs-ℝ , abs-mul-ℝ) ,
-    eq-raise-zero-eq-raise-zero-abs-ℝ)
+    λ x |x|~0 → eq-raise-zero-is-zero-ℝ (is-zero-is-zero-abs-ℝ x |x|~0))
 
 abstract
   eq-metric-space-normed-real-vector-space-metric-space-ℝ :
@@ -341,7 +333,7 @@ module _
                         ( _)
                         ( _))
                 ＝ dist-Normed-ℝ-Vector-Space V x y
-                  by commutative-dist-Normed-ℝ-Vector-Space V y x)))
+                  by symmetric-dist-Normed-ℝ-Vector-Space V y x)))
 ```
 
 ### Left addition is an isometry in the metric space of a normed vector space

src/linear-algebra/orthogonality-bilinear-forms-real-vector-spaces.lagda.md

@@ -17,6 +17,7 @@ open import linear-algebra.real-vector-spaces
 
 open import real-numbers.dedekind-real-numbers
 open import real-numbers.rational-real-numbers
+open import real-numbers.zero-real-numbers
 ```
 
 </details>
@@ -40,15 +41,12 @@ module _
   where
 
   is-orthogonal-prop-bilinear-form-ℝ-Vector-Space :
-    Relation-Prop (lsuc l1) (type-ℝ-Vector-Space V)
+    Relation-Prop l1 (type-ℝ-Vector-Space V)
   is-orthogonal-prop-bilinear-form-ℝ-Vector-Space v w =
-    Id-Prop
-      ( ℝ-Set l1)
-      ( map-bilinear-form-ℝ-Vector-Space V B v w)
-      ( raise-zero-ℝ l1)
+    is-zero-prop-ℝ (map-bilinear-form-ℝ-Vector-Space V B v w)
 
   is-orthogonal-bilinear-form-ℝ-Vector-Space :
-    Relation (lsuc l1) (type-ℝ-Vector-Space V)
+    Relation l1 (type-ℝ-Vector-Space V)
   is-orthogonal-bilinear-form-ℝ-Vector-Space =
     type-Relation-Prop is-orthogonal-prop-bilinear-form-ℝ-Vector-Space
 ```

src/linear-algebra/orthogonality-real-inner-product-spaces.lagda.md

@@ -24,6 +24,7 @@ open import real-numbers.raising-universe-levels-real-numbers
 open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
 open import real-numbers.square-roots-nonnegative-real-numbers
+open import real-numbers.zero-real-numbers
 ```
 
 </details>
@@ -47,14 +48,14 @@ module _
   where
 
   is-orthogonal-prop-ℝ-Inner-Product-Space :
-    Relation-Prop (lsuc l1) (type-ℝ-Inner-Product-Space V)
+    Relation-Prop l1 (type-ℝ-Inner-Product-Space V)
   is-orthogonal-prop-ℝ-Inner-Product-Space =
     is-orthogonal-prop-bilinear-form-ℝ-Vector-Space
       ( vector-space-ℝ-Inner-Product-Space V)
       ( bilinear-form-inner-product-ℝ-Inner-Product-Space V)
 
   is-orthogonal-ℝ-Inner-Product-Space :
-    Relation (lsuc l1) (type-ℝ-Inner-Product-Space V)
+    Relation l1 (type-ℝ-Inner-Product-Space V)
   is-orthogonal-ℝ-Inner-Product-Space =
     type-Relation-Prop is-orthogonal-prop-ℝ-Inner-Product-Space
 ```
@@ -95,8 +96,15 @@ module _
           ⟨ v +V w ,V v +V w ⟩
           ＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ ⟨ v ,V w ⟩ +ℝ ⟨ w ,V w ⟩
             by squared-norm-add-ℝ-Inner-Product-Space V v w
-          ＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ raise-ℝ l1 zero-ℝ +ℝ ⟨ w ,V w ⟩
-            by ap-add-ℝ (ap-add-ℝ refl (ap-mul-ℝ refl v∙w=0)) refl
+          ＝ ⟨ v ,V v ⟩ +ℝ real-ℕ 2 *ℝ raise-zero-ℝ l1 +ℝ ⟨ w ,V w ⟩
+            by
+              ap-add-ℝ
+                ( ap-add-ℝ
+                  ( refl)
+                  ( ap-mul-ℝ
+                    ( refl)
+                    ( eq-raise-zero-is-zero-ℝ v∙w=0)))
+                ( refl)
           ＝ ⟨ v ,V v ⟩ +ℝ zero-ℝ +ℝ ⟨ w ,V w ⟩
             by
               ap-add-ℝ
@@ -124,8 +132,7 @@ module _
     norm-add-orthogonal-ℝ-Inner-Product-Space v w v∙w=0 =
       ap
         ( real-sqrt-ℝ⁰⁺)
-        ( eq-ℝ⁰⁺ _ _
-          ( pythagorean-theorem-ℝ-Inner-Product-Space v w v∙w=0))
+        ( eq-ℝ⁰⁺ _ _ (pythagorean-theorem-ℝ-Inner-Product-Space v w v∙w=0))
 ```
 
 ### Orthogonality is preserved by scalar multiplication
@@ -144,22 +151,22 @@ module _
     preserves-is-orthogonal-left-mul-ℝ-Inner-Product-Space c v w v·w=0 =
       let
         ⟨_,V_⟩ = inner-product-ℝ-Inner-Product-Space V
-        _+V_ = add-ℝ-Inner-Product-Space V
         _*V_ = mul-ℝ-Inner-Product-Space V
       in
-        equational-reasoning
-          ⟨ c *V v ,V w ⟩
-          ＝ c *ℝ ⟨ v ,V w ⟩
-            by
-              preserves-scalar-mul-left-inner-product-ℝ-Inner-Product-Space
+        similarity-reasoning-ℝ
+        ⟨ c *V v ,V w ⟩
+        ~ℝ c *ℝ ⟨ v ,V w ⟩
+          by
+            sim-eq-ℝ
+              ( preserves-scalar-mul-left-inner-product-ℝ-Inner-Product-Space
                 ( V)
-                ( _)
-                ( _)
-                ( _)
-          ＝ c *ℝ raise-ℝ l1 zero-ℝ
-            by ap-mul-ℝ refl v·w=0
-          ＝ raise-ℝ l1 zero-ℝ
-            by right-raise-zero-law-mul-ℝ c
+                ( c)
+                ( v)
+                ( w))
+        ~ℝ c *ℝ zero-ℝ
+          by preserves-sim-left-mul-ℝ c _ _ v·w=0
+        ~ℝ zero-ℝ
+          by right-zero-law-mul-ℝ c
 ```
 
 ## References

src/linear-algebra/real-inner-product-spaces-are-normed.lagda.md

@@ -42,6 +42,7 @@ open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
 open import real-numbers.square-roots-nonnegative-real-numbers
 open import real-numbers.squares-real-numbers
+open import real-numbers.zero-real-numbers
 ```
 
 </details>
@@ -145,23 +146,17 @@ module _
   abstract
     is-extensional-norm-ℝ-Inner-Product-Space :
       (v : type-ℝ-Inner-Product-Space V) →
-      (norm-ℝ-Inner-Product-Space V v ＝ raise-ℝ l1 zero-ℝ) →
+      is-zero-ℝ (norm-ℝ-Inner-Product-Space V v) →
       is-zero-ℝ-Inner-Product-Space V v
     is-extensional-norm-ℝ-Inner-Product-Space v ∥v∥=0 =
       is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space
         ( V)
         ( v)
-        ( equational-reasoning
-          squared-norm-ℝ-Inner-Product-Space V v
-          ＝ square-ℝ (norm-ℝ-Inner-Product-Space V v)
-            by
-              inv
-                ( eq-real-square-sqrt-ℝ⁰⁺
-                  ( nonnegative-squared-norm-ℝ-Inner-Product-Space V v))
-          ＝ square-ℝ (raise-ℝ l1 zero-ℝ)
-            by ap square-ℝ ∥v∥=0
-          ＝ raise-ℝ l1 zero-ℝ
-            by square-raise-zero-ℝ l1)
+        ( tr
+          ( is-zero-ℝ)
+          ( eq-real-square-sqrt-ℝ⁰⁺
+            ( nonnegative-squared-norm-ℝ-Inner-Product-Space V v))
+          ( is-zero-square-is-zero-ℝ ∥v∥=0))
 
   norm-normed-vector-space-ℝ-Inner-Product-Space :
     norm-ℝ-Vector-Space (vector-space-ℝ-Inner-Product-Space V)

src/linear-algebra/real-inner-product-spaces.lagda.md

@@ -44,6 +44,7 @@ open import real-numbers.rational-real-numbers
 open import real-numbers.similarity-real-numbers
 open import real-numbers.square-roots-nonnegative-real-numbers
 open import real-numbers.squares-real-numbers
+open import real-numbers.zero-real-numbers
 ```
 
 </details>
@@ -74,16 +75,13 @@ module _
       ( type-ℝ-Vector-Space V)
       ( λ v → is-nonnegative-prop-ℝ (map-bilinear-form-ℝ-Vector-Space V B v v))
 
-  is-extensional-prop-bilinear-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
+  is-extensional-prop-bilinear-form-ℝ-Vector-Space : Prop (l1 ⊔ l2)
   is-extensional-prop-bilinear-form-ℝ-Vector-Space =
     Π-Prop
       ( type-ℝ-Vector-Space V)
       ( λ v →
         hom-Prop
-          ( Id-Prop
-            ( ℝ-Set l1)
-            ( map-bilinear-form-ℝ-Vector-Space V B v v)
-            ( raise-ℝ l1 zero-ℝ))
+          ( is-zero-prop-ℝ (map-bilinear-form-ℝ-Vector-Space V B v v))
           ( is-zero-prop-ℝ-Vector-Space V v))
 
   is-inner-product-prop-bilinear-form-ℝ-Vector-Space : Prop (lsuc l1 ⊔ l2)
@@ -217,7 +215,7 @@ module _
 
   is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space :
     (v : type-ℝ-Inner-Product-Space) →
-    inner-product-ℝ-Inner-Product-Space v v ＝ raise-zero-ℝ l1 →
+    is-zero-ℝ (inner-product-ℝ-Inner-Product-Space v v) →
     v ＝ zero-ℝ-Inner-Product-Space
   is-extensional-diagonal-inner-product-ℝ-Inner-Product-Space =
     pr2 (pr2 (pr2 (pr2 V)))
@@ -602,7 +600,7 @@ is-inner-product-bilinear-form-mul-ℝ :
 is-inner-product-bilinear-form-mul-ℝ l =
   ( commutative-mul-ℝ ,
     is-nonnegative-square-ℝ ,
-    eq-zero-eq-zero-square-ℝ)
+    λ x x²=0 → eq-raise-zero-is-zero-ℝ (is-zero-is-zero-square-ℝ x x²=0))
 
 real-inner-product-space-ℝ : (l : Level) → ℝ-Inner-Product-Space l (lsuc l)
 real-inner-product-space-ℝ l =