Replace symbol for similarity

src/foundation/images-subtypes.lagda.md

@@ -205,7 +205,7 @@ module _
 **Proof:** The asserted similarity follows at once from the similarity
 
 ```text
-  pullback-subtype (g ∘ f) ≈ pullback-subtype g ∘ pullback-subtype f
+  pullback-subtype (g ∘ f) ≍ pullback-subtype g ∘ pullback-subtype f
 ```
 
 via the image-pullback Galois connection.

src/group-theory/minkowski-multiplication-semigroups.lagda.md

@@ -229,13 +229,13 @@ module _
     sim-subtype
       ( minkowski-mul-Semigroup G A B)
       ( minkowski-mul-Semigroup G A' B')
-  preserves-sim-minkowski-mul-Semigroup A≈A' B≈B' =
+  preserves-sim-minkowski-mul-Semigroup A≍A' B≍B' =
     transitive-sim-subtype
       ( minkowski-mul-Semigroup G A B)
       ( minkowski-mul-Semigroup G A B')
       ( minkowski-mul-Semigroup G A' B')
-      ( preserves-sim-left-minkowski-mul-Semigroup G B' A A' A≈A')
-      ( preserves-sim-right-minkowski-mul-Semigroup G A B B' B≈B')
+      ( preserves-sim-left-minkowski-mul-Semigroup G B' A A' A≍A')
+      ( preserves-sim-right-minkowski-mul-Semigroup G A B B' B≍B')
 ```
 
 ## External links

src/order-theory/commuting-squares-of-galois-connections-large-posets.lagda.md

@@ -41,9 +41,9 @@ Consider a diagram of
 between [large posets](order-theory.large-posets.md). We say that the diagram
 **commutes** if there is a
 [similarity](order-theory.similarity-of-order-preserving-maps-large-posets.md)
-`LJ ∘ LF ≈ LG ∘ LI`. This condition is
+`LJ ∘ LF ≍ LG ∘ LI`. This condition is
 [equivalent](foundation.logical-equivalences.md) the condition that there is a
-similarity `UF ∘ UJ ≈ UI ∘ UG`.
+similarity `UF ∘ UJ ≍ UI ∘ UG`.
 
 ## Definitions
 

src/order-theory/galois-connections-large-posets.lagda.md

@@ -454,8 +454,8 @@ module _
 ### A homotopy between lower adjoints of a Galois connection induces a homotopy between upper adjoints, and vice versa
 
 **Proof:** Consider two Galois connections `LG ⊣ UG` and `LH ⊣ UH` between `P`
-and `Q`, and suppose that `LG ~ LH`. Then there is a similarity `LG ≈ LH`, and
-this induces a similarity `UG ≈ UH`. In other words, we obtain that
+and `Q`, and suppose that `LG ~ LH`. Then there is a similarity `LG ≍ LH`, and
+this induces a similarity `UG ≍ UH`. In other words, we obtain that
 
 ```text
   UG y ~ UH y

src/order-theory/similarity-of-elements-large-posets.lagda.md

@@ -30,8 +30,10 @@ are said to be **similar** if both `x ≤ y` and `y ≤ x` hold. Note that the
 similarity relation is defined across universe levels, and that only similar
 elements of the same universe level are equal.
 
-In informal writing we will use the notation `x ≈ y` to assert that `x` and `y`
-are similar elements in a poset `P`.
+**Notation.** In informal writing we will use the notation `x ≍ y` to assert
+that `x` and `y` are similar elements in a poset `P`. The symbol `≍` is the
+unicode symbol [Equivalent To](https://codepoints.net/U+224d) (agda-input:
+`\asymp`).
 
 ## Definition
 

src/order-theory/similarity-of-elements-large-preorders.lagda.md

@@ -23,8 +23,10 @@ open import order-theory.large-preorders
 Two elements `x` and `y` of a [large preorder](order-theory.large-preorders.md)
 `P` are said to be **similar** if both `x ≤ y` and `y ≤ x` hold.
 
-In informal writing we will use the notation `x ≈ y` to assert that `x` and `y`
-are similar elements in a preorder `P`.
+**Notation.** In informal writing we will use the notation `x ≍ y` to assert
+that `x` and `y` are similar elements in a preorder `P`. The symbol `≍` is the
+unicode symbol [Equivalent To](https://codepoints.net/U+224d) (agda-input:
+`\asymp`).
 
 ## Definition
 

src/order-theory/similarity-of-elements-large-strict-orders.lagda.md

@@ -45,8 +45,10 @@ We refer to the first condition as
 and the second condition as
 {{#concept "similarity from above" Disambiguation="of elements of a large strict order" Agda=sim-from-above-Large-Strict-Order}}.
 
-In informal writing we will use the notation `x ≈ y` to assert that `x` and `y`
-are similar elements in a large strict order `A`.
+**Notation.** In informal writing we will use the notation `x ≍ y` to assert
+that `x` and `y` are similar elements in a large strict order `A`. The symbol
+`≍` is the unicode symbol [Equivalent To](https://codepoints.net/U+224d)
+(agda-input: `\asymp`).
 
 ## Definitions
 

src/order-theory/similarity-of-elements-large-strict-preorders.lagda.md

@@ -45,8 +45,10 @@ We refer to the first condition as
 and the second condition as
 {{#concept "similarity from above" Disambiguation="of elements of a large strict preorder" Agda=sim-from-above-Large-Strict-Preorder}}.
 
-In informal writing we will use the notation `x ≈ y` to assert that `x` and `y`
-are similar elements in a large strict preorder `P`.
+**Notation.** In informal writing we will use the notation `x ≍ y` to assert
+that `x` and `y` are similar elements in a large strict preorder `P`. The symbol
+`≍` is the unicode symbol [Equivalent To](https://codepoints.net/U+224d)
+(agda-input: `\asymp`).
 
 ## Definitions
 

src/order-theory/similarity-of-elements-strict-orders.lagda.md

@@ -43,8 +43,10 @@ We refer to the first condition as
 and the second condition as
 {{#concept "similarity from above" Disambiguation="of elements of a strict order" Agda=sim-from-above-Strict-Order}}.
 
-In informal writing we will use the notation `x ≈ y` to assert that `x` and `y`
-are similar elements in a strict order `A`.
+**Notation.** In informal writing we will use the notation `x ≍ y` to assert
+that `x` and `y` are similar elements in a strict order `A`. The symbol `≍` is
+the unicode symbol [Equivalent To](https://codepoints.net/U+224d) (agda-input:
+`\asymp`).
 
 ## Definitions
 

src/order-theory/similarity-of-elements-strict-preorders.lagda.md

@@ -42,8 +42,10 @@ We refer to the first condition as
 and the second condition as
 {{#concept "similarity from above" Disambiguation="of elements of a strict preorder" Agda=sim-from-above-Strict-Preorder}}.
 
-In informal writing we will use the notation `x ≈ y` to assert that `x` and `y`
-are similar elements in a strict preorder `P`.
+**Notation.** In informal writing we will use the notation `x ≍ y` to assert
+that `x` and `y` are similar elements in a strict preorder `P`. The symbol `≍`
+is the unicode symbol [Equivalent To](https://codepoints.net/U+224d)
+(agda-input: `\asymp`).
 
 ## Definitions
 

src/order-theory/similarity-of-order-preserving-maps-large-posets.lagda.md

@@ -31,12 +31,13 @@ In other words, a **similarity of order preserving maps** between `f` and `g`
 consists of an assignment `x ↦ h x` where
 
 ```text
-  h x : f x ≈ g x
+  h x : f x ≍ g x
 ```
 
 for each `x : type-Large-Poset P`. In informal writing we will use the notation
-`f ≈ g` to assert that the order preserving map `f` is similar to the order
-preserving map `g`.
+`f ≍ g` to assert that the order preserving map `f` is similar to the order
+preserving map `g`. The symbol `≍` is the unicode symbol
+[Equivalent To](https://codepoints.net/U+224d) (agda-input: `\asymp`).
 
 ## Definitions
 

src/order-theory/similarity-of-order-preserving-maps-large-preorders.lagda.md

@@ -30,12 +30,13 @@ each specified with their own universe level reindexing functions. We say that
 and `g` consists of an assignment `x ↦ h x` where
 
 ```text
-  h x : f x ≈ g x
+  h x : f x ≍ g x
 ```
 
 for each `x : type-Large-Preorder P`. In informal writing we will use the
-notation `f ≈ g` to assert that the order preserving map `f` is similar to the
-order preserving map `g`.
+notation `f ≍ g` to assert that the order preserving map `f` is similar to the
+order preserving map `g`. The symbol `≍` is the unicode symbol
+[Equivalent To](https://codepoints.net/U+224d) (agda-input: `\asymp`).
 
 ## Definitions
 

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

@@ -268,12 +268,12 @@ module _
       map-tot-exists (λ (qy , _) → map-product (ly⊆lx qy) id)
 
     preserves-sim-left-add-ℝ : sim-ℝ x y → sim-ℝ (z +ℝ x) (z +ℝ y)
-    preserves-sim-left-add-ℝ x≈y =
+    preserves-sim-left-add-ℝ x≍y =
       binary-tr
         ( sim-ℝ)
         ( commutative-add-ℝ x z)
         ( commutative-add-ℝ y z)
-        ( preserves-sim-right-add-ℝ x≈y)
+        ( preserves-sim-right-add-ℝ x≍y)
 ```
 
 ### Swapping laws for addition on real numbers
@@ -340,11 +340,11 @@ module _
     reflects-sim-right-add-ℝ x+z≈y+z =
       similarity-reasoning-ℝ
         x
-        ~ℝ (x +ℝ z) +ℝ neg-ℝ z
+        ≍ℝ (x +ℝ z) +ℝ neg-ℝ z
           by symmetric-sim-ℝ (cancel-right-add-diff-ℝ x z)
-        ~ℝ (y +ℝ z) +ℝ neg-ℝ z
+        ≍ℝ (y +ℝ z) +ℝ neg-ℝ z
           by preserves-sim-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z≈y+z
-        ~ℝ y by cancel-right-add-diff-ℝ y z
+        ≍ℝ y by cancel-right-add-diff-ℝ y z
 
     reflects-sim-left-add-ℝ : sim-ℝ (z +ℝ x) (z +ℝ y) → sim-ℝ x y
     reflects-sim-left-add-ℝ z+x≈z+y =
@@ -441,19 +441,19 @@ module _
       eq-sim-ℝ
         ( similarity-reasoning-ℝ
           neg-ℝ (x +ℝ y)
-          ~ℝ neg-ℝ (x +ℝ y) +ℝ x +ℝ neg-ℝ x
+          ≍ℝ neg-ℝ (x +ℝ y) +ℝ x +ℝ neg-ℝ x
             by symmetric-sim-ℝ (cancel-right-add-diff-ℝ _ x)
-          ~ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ neg-ℝ x) +ℝ y) +ℝ neg-ℝ y
+          ≍ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ neg-ℝ x) +ℝ y) +ℝ neg-ℝ y
             by symmetric-sim-ℝ (cancel-right-add-diff-ℝ _ y)
-          ~ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ y) +ℝ neg-ℝ x) +ℝ neg-ℝ y
+          ≍ℝ (((neg-ℝ (x +ℝ y) +ℝ x) +ℝ y) +ℝ neg-ℝ x) +ℝ neg-ℝ y
             by sim-eq-ℝ (ap (_+ℝ neg-ℝ y) (right-swap-add-ℝ _ (neg-ℝ x) y))
-          ~ℝ ((neg-ℝ (x +ℝ y) +ℝ (x +ℝ y)) +ℝ neg-ℝ x) +ℝ neg-ℝ y
+          ≍ℝ ((neg-ℝ (x +ℝ y) +ℝ (x +ℝ y)) +ℝ neg-ℝ x) +ℝ neg-ℝ y
             by
               sim-eq-ℝ
                 ( ap
                   ( _+ℝ neg-ℝ y)
                   ( ap (_+ℝ neg-ℝ x) (associative-add-ℝ _ _ _)))
-          ~ℝ (zero-ℝ +ℝ neg-ℝ x) +ℝ neg-ℝ y
+          ≍ℝ (zero-ℝ +ℝ neg-ℝ x) +ℝ neg-ℝ y
             by
               preserves-sim-right-add-ℝ
                 ( neg-ℝ y)
@@ -464,7 +464,7 @@ module _
                   ( _)
                   ( _)
                   ( left-inverse-law-add-ℝ _))
-          ~ℝ neg-ℝ x +ℝ neg-ℝ y
+          ≍ℝ neg-ℝ x +ℝ neg-ℝ y
             by sim-eq-ℝ (ap (_+ℝ neg-ℝ y) (left-unit-law-add-ℝ _)))
 ```
 

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

@@ -193,8 +193,8 @@ abstract
       ( preserves-sim-abs-ℝ
         ( similarity-reasoning-ℝ
           x -ℝ y +ℝ y -ℝ z
-          ~ℝ (x -ℝ y +ℝ y) -ℝ z by sim-eq-ℝ (inv (associative-add-ℝ _ _ _))
-          ~ℝ x -ℝ z by
+          ≍ℝ (x -ℝ y +ℝ y) -ℝ z by sim-eq-ℝ (inv (associative-add-ℝ _ _ _))
+          ≍ℝ x -ℝ z by
             preserves-sim-right-add-ℝ
               ( neg-ℝ z)
               ( x -ℝ y +ℝ y)

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

@@ -47,9 +47,9 @@ opaque
   sim-ℝ : {l1 l2 : Level} → ℝ l1 → ℝ l2 → UU (l1 ⊔ l2)
   sim-ℝ x y = type-Prop (sim-prop-ℝ x y)
 
-infix 6 _~ℝ_
-_~ℝ_ : {l1 l2 : Level} → ℝ l1 → ℝ l2 → UU (l1 ⊔ l2)
-_~ℝ_ = sim-ℝ
+infix 6 _≍ℝ_
+_≍ℝ_ : {l1 l2 : Level} → ℝ l1 → ℝ l2 → UU (l1 ⊔ l2)
+_≍ℝ_ = sim-ℝ
 ```
 
 ## Properties
@@ -65,7 +65,7 @@ module _
     unfolding sim-ℝ
 
     sim-lower-cut-iff-sim-ℝ :
-      sim-subtype (lower-cut-ℝ x) (lower-cut-ℝ y) ↔ (x ~ℝ y)
+      sim-subtype (lower-cut-ℝ x) (lower-cut-ℝ y) ↔ (x ≍ℝ y)
     sim-lower-cut-iff-sim-ℝ = id-iff
 ```
 
@@ -79,14 +79,14 @@ module _
   opaque
     unfolding sim-ℝ
 
-    sim-sim-upper-cut-ℝ : sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y) → (x ~ℝ y)
+    sim-sim-upper-cut-ℝ : sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y) → (x ≍ℝ y)
     sim-sim-upper-cut-ℝ = sim-lower-cut-sim-upper-cut-ℝ x y
 
-    sim-upper-cut-sim-ℝ : (x ~ℝ y) → sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y)
+    sim-upper-cut-sim-ℝ : (x ≍ℝ y) → sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y)
     sim-upper-cut-sim-ℝ = sim-upper-cut-sim-lower-cut-ℝ x y
 
   sim-upper-cut-iff-sim-ℝ :
-    sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y) ↔ (x ~ℝ y)
+    sim-subtype (upper-cut-ℝ x) (upper-cut-ℝ y) ↔ (x ≍ℝ y)
   sim-upper-cut-iff-sim-ℝ = (sim-sim-upper-cut-ℝ , sim-upper-cut-sim-ℝ)
 ```
 
@@ -96,10 +96,10 @@ module _
 opaque
   unfolding sim-ℝ
 
-  refl-sim-ℝ : {l : Level} → (x : ℝ l) → x ~ℝ x
+  refl-sim-ℝ : {l : Level} → (x : ℝ l) → x ≍ℝ x
   refl-sim-ℝ x = refl-sim-subtype (lower-cut-ℝ x)
 
-  sim-eq-ℝ : {l : Level} → {x y : ℝ l} → x ＝ y → x ~ℝ y
+  sim-eq-ℝ : {l : Level} → {x y : ℝ l} → x ＝ y → x ≍ℝ y
   sim-eq-ℝ {_} {x} {y} x=y = tr (sim-ℝ x) x=y (refl-sim-ℝ x)
 ```
 
@@ -110,7 +110,7 @@ opaque
   unfolding sim-ℝ
 
   symmetric-sim-ℝ :
-    {l1 l2 : Level} → {x : ℝ l1} {y : ℝ l2} → x ~ℝ y → y ~ℝ x
+    {l1 l2 : Level} → {x : ℝ l1} {y : ℝ l2} → x ≍ℝ y → y ≍ℝ x
   symmetric-sim-ℝ {x = x} {y = y} =
     symmetric-sim-subtype (lower-cut-ℝ x) (lower-cut-ℝ y)
 ```
@@ -124,7 +124,7 @@ opaque
   transitive-sim-ℝ :
     {l1 l2 l3 : Level} →
     (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
-    y ~ℝ z → x ~ℝ y → x ~ℝ z
+    y ≍ℝ z → x ≍ℝ y → x ≍ℝ z
   transitive-sim-ℝ x y z =
     transitive-sim-subtype (lower-cut-ℝ x) (lower-cut-ℝ y) (lower-cut-ℝ z)
 ```
@@ -135,7 +135,7 @@ opaque
 opaque
   unfolding sim-ℝ
 
-  eq-sim-ℝ : {l : Level} → {x y : ℝ l} → x ~ℝ y → x ＝ y
+  eq-sim-ℝ : {l : Level} → {x y : ℝ l} → x ≍ℝ y → x ＝ y
   eq-sim-ℝ {x = x} {y = y} H = eq-eq-lower-cut-ℝ x y (eq-sim-subtype _ _ H)
 ```
 
@@ -146,8 +146,8 @@ the following way:
 
 ```text
 similarity-reasoning-ℝ
-  x ~ℝ y by sim-1
-    ~ℝ z by sim-2
+  x ≍ℝ y by sim-1
+    ≍ℝ z by sim-2
 ```
 
 ```agda
@@ -166,5 +166,5 @@ opaque
     sim-ℝ x y → {l3 : Level} → (u : ℝ l3) → sim-ℝ y u → sim-ℝ x u
   step-similarity-reasoning-ℝ {x = x} {y = y} p u q = transitive-sim-ℝ x y u q p
 
-  syntax step-similarity-reasoning-ℝ p u q = p ~ℝ u by q
+  syntax step-similarity-reasoning-ℝ p u q = p ≍ℝ u by q
 ```

src/trees/ranks-of-elements-w-types.lagda.md

@@ -47,11 +47,11 @@ module _
   _≼-𝕎_ : 𝕎 A B → 𝕎 A B → UU (l1 ⊔ l2)
   x ≼-𝕎 y = type-Prop (x ≼-𝕎-Prop y)
 
-  _≈-𝕎-Prop_ : (x y : 𝕎 A B) → Prop (l1 ⊔ l2)
-  x ≈-𝕎-Prop y = product-Prop (x ≼-𝕎-Prop y) (y ≼-𝕎-Prop x)
+  _≍-𝕎-Prop_ : (x y : 𝕎 A B) → Prop (l1 ⊔ l2)
+  x ≍-𝕎-Prop y = product-Prop (x ≼-𝕎-Prop y) (y ≼-𝕎-Prop x)
 
-  _≈-𝕎_ : (x y : 𝕎 A B) → UU (l1 ⊔ l2)
-  x ≈-𝕎 y = type-Prop (x ≈-𝕎-Prop y)
+  _≍-𝕎_ : (x y : 𝕎 A B) → UU (l1 ⊔ l2)
+  x ≍-𝕎 y = type-Prop (x ≍-𝕎-Prop y)
 ```
 
 ### Strict rank comparison