More fixities for Data and Codata (#1989)

Saransh-cpp · plt-amy · commit 657fa5af0f6d · 2023-07-21T13:07:42.000-03:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -31,51 +31,80 @@ Bug-fixes
 
 * The following operators were missing a fixity declaration, which has now
   been fixed -
-   ```
-  infix  -1 _$ⁿ_          (Data.Vec.N-ary)
-  infix  4 _≋_            (Data.Vec.Functional.Relation.Binary.Equality.Setoid)
-  infix  4 _≟_            (Reflection.AST.Definition)
-  infix  4 _≡ᵇ_           (Reflection.AST.Literal)
-  infix  4 _≈?_ _≟_ _≈_   (Reflection.AST.Meta)
-  infix  4 _≈?_ _≟_ _≈_   (Reflection.AST.Name)
-  infix  4 _≟-Telescope_  (Reflection.AST.Term)
-  infix  4 _≟_            (Reflection.AST.Argument.Information)
-  infix  4 _≟_            (Reflection.AST.Argument.Modality)
-  infix  4 _≟_            (Reflection.AST.Argument.Quantity)
-  infix  4 _≟_            (Reflection.AST.Argument.Relevance)
-  infix  4 _≟_            (Reflection.AST.Argument.Visibility)
-  infixr 8 _^_            (Function.Endomorphism.Propositional)
-  infixr 8 _^_            (Function.Endomorphism.Setoid)
-  infix  4 _≃_            (Function.HalfAdjointEquivalence)
-  infix  4 _≈_ _≈ᵢ_ _≤_   (Function.Metric.Bundles)
-  infixl 6 _∙_            (Function.Metric.Bundles)
-  infix  4 _≈_            (Function.Metric.Nat.Bundles)
-  infix  3 _←_ _↢_        (Function.Related)
-
-  infix  4 _ℕ<_ _ℕ≤infinity _ℕ≤_                            (Codata.Sized.Conat)
-  infix  6 _ℕ+_ _+ℕ_                                        (Codata.Sized.Conat)
-  infixl 4 _+ _*                                            (Data.List.Kleene.Base)
-  infixr 4 _++++_ _+++*_ _*+++_ _*++*_                      (Data.List.Kleene.Base)
-  infix  4 _[_]* _[_]+                                      (Data.List.Kleene.Base)
-  infix  4 _≢∈_                                             (Data.List.Membership.Propositional)
-  infixr 5 _`∷_                                             (Data.List.Reflection)
-  infix  4 _≡?_                                             (Data.List.Relation.Binary.Equality.DecPropositional)
-  infixr 5 _++ᵖ_                                            (Data.List.Relation.Binary.Prefix.Heterogeneous)
-  infixr 5 _++ˢ_                                            (Data.List.Relation.Binary.Suffix.Heterogeneous)
-  infixr 5 _++_ _++[]                                       (Data.List.Relation.Ternary.Appending.Propositional)
-  infixr 5 _∷=_                                             (Data.List.Relation.Unary.Any)
-  infixr 5 _++_                                             (Data.List.Ternary.Appending)
-  infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_           (Data.Product.Function.NonDependent.Propositional)
-  infixr 2 _×-⟶_                                           (Data.Product.Function.NonDependent.Setoid)
-  infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_   (Data.Product.Function.NonDependent.Setoid)
-  infixr 2 _×-surjection_ _×-inverse_                       (Data.Product.Function.NonDependent.Setoid)
-  infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_           (Data.Sum.Function.Propositional)
-  infixr 1 _⊎-⟶_                                           (Data.Sum.Function.Setoid)
-  infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_   (Data.Sum.Function.Setoid)
-  infixr 1 _⊎-surjection_ _⊎-inverse_                       (Data.Sum.Function.Setoid)
-  infix  8 _⁻¹                                              (Data.Parity.Base)
-  infixr 5 _`∷_                                             (Data.Vec.Reflection)
-  infixr 5 _∷=_                                             (Data.Vec.Membership.Setoid)
+  ```
+  infixr  5 _∷_                                              (Codata.Guarded.Stream)
+  infix   4 _[_]                                             (Codata.Guarded.Stream)
+  infixr  5 _∷_                                              (Codata.Guarded.Stream.Relation.Binary.Pointwise)
+  infix   4 _≈∞_                                             (Codata.Guarded.Stream.Relation.Binary.Pointwise)
+  infixr  5 _∷_                                              (Codata.Musical.Colist)
+  infix   4 _≈_                                              (Codata.Musical.Conat)
+  infixr  5 _∷_                                              (Codata.Musical.Colist.Bisimilarity)
+  infixr  5 _∷_                                              (Codata.Musical.Colist.Relation.Unary.All)
+  infixr  5 _∷_                                              (Codata.Sized.Colist)
+  infixr  5 _∷_                                              (Codata.Sized.Covec)
+  infixr  5 _∷_                                              (Codata.Sized.Cowriter)
+  infixl  1 _>>=_                                            (Codata.Sized.Cowriter)
+  infixr  5 _∷_                                              (Codata.Sized.Stream)
+  infixr  5 _∷_                                              (Codata.Sized.Colist.Bisimilarity)
+  infix   4 _ℕ≤?_                                            (Codata.Sized.Conat.Properties)
+  infixr  5 _∷_                                              (Codata.Sized.Covec.Bisimilarity)
+  infixr  5 _∷_                                              (Codata.Sized.Cowriter.Bisimilarity)
+  infixr  5 _∷_                                              (Codata.Sized.Stream.Bisimilarity)
+  infixr  8 _⇒_ _⊸_                                          (Data.Container.Core)
+  infixr -1 _<$>_ _<*>_                                      (Data.Container.FreeMonad)
+  infixl  1 _>>=_                                            (Data.Container.FreeMonad)
+  infix   5 _▷_                                              (Data.Container.Indexed)
+  infix   4 _≈_                                              (Data.Float.Base)
+  infixl  7 _⊓′_                                             (Data.Nat.Base)
+  infixl  6 _⊔′_                                             (Data.Nat.Base)
+  infixr  8 _^_                                              (Data.Nat.Base)
+  infix   4 _!≢0 _!*_!≢0                                     (Data.Nat.Properties)
+  infix   4 _≃?_                                             (Data.Rational.Unnormalised.Properties)
+  infix   4 _≈ₖᵥ_                                            (Data.Tree.AVL.Map.Membership.Propositional)
+  infix   4 _<_                                              (Induction.WellFounded)
+  infix  -1 _$ⁿ_                                             (Data.Vec.N-ary)
+  infix   4 _≋_                                              (Data.Vec.Functional.Relation.Binary.Equality.Setoid)
+  infix   4 _≟_                                              (Reflection.AST.Definition)
+  infix   4 _≡ᵇ_                                             (Reflection.AST.Literal)
+  infix   4 _≈?_ _≟_ _≈_                                     (Reflection.AST.Meta)
+  infix   4 _≈?_ _≟_ _≈_                                     (Reflection.AST.Name)
+  infix   4 _≟-Telescope_                                    (Reflection.AST.Term)
+  infix   4 _≟_                                              (Reflection.AST.Argument.Information)
+  infix   4 _≟_                                              (Reflection.AST.Argument.Modality)
+  infix   4 _≟_                                              (Reflection.AST.Argument.Quantity)
+  infix   4 _≟_                                              (Reflection.AST.Argument.Relevance)
+  infix   4 _≟_                                              (Reflection.AST.Argument.Visibility)
+  infixr  8 _^_                                              (Function.Endomorphism.Propositional)
+  infixr  8 _^_                                              (Function.Endomorphism.Setoid)
+  infix   4 _≃_                                              (Function.HalfAdjointEquivalence)
+  infix   4 _≈_ _≈ᵢ_ _≤_                                     (Function.Metric.Bundles)
+  infixl  6 _∙_                                              (Function.Metric.Bundles)
+  infix   4 _≈_                                              (Function.Metric.Nat.Bundles)
+  infix   3 _←_ _↢_                                          (Function.Related)
+  infix   4 _ℕ<_ _ℕ≤infinity _ℕ≤_                            (Codata.Sized.Conat)
+  infix   6 _ℕ+_ _+ℕ_                                        (Codata.Sized.Conat)
+  infixl  4 _+ _*                                            (Data.List.Kleene.Base)
+  infixr  4 _++++_ _+++*_ _*+++_ _*++*_                      (Data.List.Kleene.Base)
+  infix   4 _[_]* _[_]+                                      (Data.List.Kleene.Base)
+  infix   4 _≢∈_                                             (Data.List.Membership.Propositional)
+  infixr  5 _`∷_                                             (Data.List.Reflection)
+  infix   4 _≡?_                                             (Data.List.Relation.Binary.Equality.DecPropositional)
+  infixr  5 _++ᵖ_                                            (Data.List.Relation.Binary.Prefix.Heterogeneous)
+  infixr  5 _++ˢ_                                            (Data.List.Relation.Binary.Suffix.Heterogeneous)
+  infixr  5 _++_ _++[]                                       (Data.List.Relation.Ternary.Appending.Propositional)
+  infixr  5 _∷=_                                             (Data.List.Relation.Unary.Any)
+  infixr  5 _++_                                             (Data.List.Ternary.Appending)
+  infixr  2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_           (Data.Product.Function.NonDependent.Propositional)
+  infixr  2 _×-⟶_                                           (Data.Product.Function.NonDependent.Setoid)
+  infixr  2 _×-equivalence_ _×-injection_ _×-left-inverse_   (Data.Product.Function.NonDependent.Setoid)
+  infixr  2 _×-surjection_ _×-inverse_                       (Data.Product.Function.NonDependent.Setoid)
+  infixr  1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_           (Data.Sum.Function.Propositional)
+  infixr  1 _⊎-⟶_                                           (Data.Sum.Function.Setoid)
+  infixr  1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_   (Data.Sum.Function.Setoid)
+  infixr  1 _⊎-surjection_ _⊎-inverse_                       (Data.Sum.Function.Setoid)
+  infix   8 _⁻¹                                              (Data.Parity.Base)
+  infixr  5 _`∷_                                             (Data.Vec.Reflection)
+  infixr  5 _∷=_                                             (Data.Vec.Membership.Setoid)
   ```
 
 * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer
diff --git a/src/Codata/Guarded/Stream.agda b/src/Codata/Guarded/Stream.agda
@@ -28,6 +28,8 @@ private
 ------------------------------------------------------------------------
 -- Type
 
+infixr 5 _∷_
+
 record Stream (A : Set a) : Set a where
   coinductive
   constructor _∷_
@@ -69,6 +71,8 @@ lookup : Stream A → ℕ → A
 lookup xs zero    = head xs
 lookup xs (suc n) = lookup (tail xs) n
 
+infix 4 _[_]
+
 _[_] : Stream A → ℕ → A
 _[_] = lookup
 
diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
@@ -25,6 +25,8 @@ private
 ------------------------------------------------------------------------
 -- Bisimilarity
 
+infixr 5 _∷_
+
 record Pointwise (_∼_ : REL A B ℓ) (as : Stream A) (bs : Stream B) : Set ℓ where
   coinductive
   constructor _∷_
@@ -191,4 +193,6 @@ module pw-Reasoning (S : Setoid a ℓ) where
 module ≈-Reasoning {a} {A : Set a} where
 
   open pw-Reasoning (P.setoid A) public
+
+  infix 4 _≈∞_
   _≈∞_ = `Pointwise∞
diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda
@@ -215,6 +215,8 @@ data Finite {A : Set a} : Colist A → Set a where
   []  : Finite []
   _∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs)
 
+infixr 5 _∷_
+
 module Finite-injective where
 
  ∷-injective : ∀ {x : A} {xs p q} → (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
diff --git a/src/Codata/Musical/Colist/Bisimilarity.agda b/src/Codata/Musical/Colist/Bisimilarity.agda
@@ -27,6 +27,8 @@ data _≈_ {A : Set a} : Rel (Colist A) a where
   []  :                                       []     ≈ []
   _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys
 
+infixr 5 _∷_
+
 -- The equality relation forms a setoid.
 
 setoid : Set a → Setoid _ _
diff --git a/src/Codata/Musical/Colist/Relation/Unary/All.agda b/src/Codata/Musical/Colist/Relation/Unary/All.agda
@@ -23,3 +23,5 @@ private
 data All {A : Set a} (P : Pred A p) : Pred (Colist A) (a ⊔ p) where
   []  : All P []
   _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)
+
+infixr 5 _∷_
diff --git a/src/Codata/Musical/Conat.agda b/src/Codata/Musical/Conat.agda
@@ -34,6 +34,8 @@ fromℕ-injective {suc m} {suc n} eq = P.cong suc (fromℕ-injective (P.cong pre
 ------------------------------------------------------------------------
 -- Equality
 
+infix 4 _≈_
+
 data _≈_ : Coℕ → Coℕ → Set where
   zero :                                 zero  ≈ zero
   suc  : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n
diff --git a/src/Codata/Sized/Colist.agda b/src/Codata/Sized/Colist.agda
@@ -42,6 +42,8 @@ data Colist (A : Set a) (i : Size) : Set a where
   []  : Colist A i
   _∷_ : A → Thunk (Colist A) i → Colist A i
 
+infixr 5 _∷_
+
 ------------------------------------------------------------------------
 -- Relationship to Cowriter.
 
diff --git a/src/Codata/Sized/Colist/Bisimilarity.agda b/src/Codata/Sized/Colist/Bisimilarity.agda
@@ -32,6 +32,8 @@ data Bisim {A : Set a} {B : Set b} (R : REL A B r) (i : Size) :
   _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys →
         Bisim R i (x ∷ xs) (y ∷ ys)
 
+infixr 5 _∷_
+
 module _ {R : Rel A r} where
 
  reflexive : Reflexive R → Reflexive (Bisim R i)
diff --git a/src/Codata/Sized/Conat/Properties.agda b/src/Codata/Sized/Conat/Properties.agda
@@ -29,6 +29,8 @@ private
 sℕ≤s⁻¹ : ∀ {m n} → suc m ℕ≤ suc n → m ℕ≤ n .force
 sℕ≤s⁻¹ (sℕ≤s p) = p
 
+infix 4 _ℕ≤?_
+
 _ℕ≤?_ : Decidable _ℕ≤_
 zero  ℕ≤? n     = yes zℕ≤n
 suc m ℕ≤? zero  = no (λ ())
diff --git a/src/Codata/Sized/Covec.agda b/src/Codata/Sized/Covec.agda
@@ -29,6 +29,8 @@ data Covec (A : Set a) (i : Size) : Conat ∞ → Set a where
   []  : Covec A i zero
   _∷_ : ∀ {n} → A → Thunk (λ i → Covec A i (n .force)) i → Covec A i (suc n)
 
+infixr 5 _∷_
+
 head : ∀ {n i} → Covec A i (suc n) → A
 head (x ∷ _) = x
 
diff --git a/src/Codata/Sized/Covec/Bisimilarity.agda b/src/Codata/Sized/Covec/Bisimilarity.agda
@@ -22,6 +22,7 @@ data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
   _∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys →
         Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys)
 
+infixr 5 _∷_
 
 module _ {a r} {A : Set a} {R : A → A → Set r} where
 
diff --git a/src/Codata/Sized/Cowriter.agda b/src/Codata/Sized/Cowriter.agda
@@ -39,6 +39,8 @@ data Cowriter (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where
   [_] : A → Cowriter W A i
   _∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i
 
+infixr 5 _∷_
+
 ------------------------------------------------------------------------
 -- Relationship to Delay.
 
@@ -101,6 +103,8 @@ ap : ∀ {i} → Cowriter W (A → X) i → Cowriter W A i → Cowriter W X i
 ap [ f ]    ca = map₂ f ca
 ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca
 
+infixl 1 _>>=_
+
 _>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i
 [ a ]    >>= f = f a
 (w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f
diff --git a/src/Codata/Sized/Cowriter/Bisimilarity.agda b/src/Codata/Sized/Cowriter/Bisimilarity.agda
@@ -33,6 +33,8 @@ data Bisim {V : Set v} {W : Set w} {A : Set a} {B : Set b}
   _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R S) i xs ys →
         Bisim R S i (x ∷ xs) (y ∷ ys)
 
+infixr 5 _∷_
+
 module _ {R : Rel W r} {S : Rel A s}
          (refl^R : Reflexive R) (refl^S : Reflexive S) where
 
diff --git a/src/Codata/Sized/Stream.agda b/src/Codata/Sized/Stream.agda
@@ -34,6 +34,8 @@ private
 data Stream (A : Set a) (i : Size) : Set a where
   _∷_ : A → Thunk (Stream A) i → Stream A i
 
+infixr 5 _∷_
+
 ------------------------------------------------------------------------
 -- Creating streams
 
diff --git a/src/Codata/Sized/Stream/Bisimilarity.agda b/src/Codata/Sized/Stream/Bisimilarity.agda
@@ -30,6 +30,8 @@ data Bisim {A : Set a} {B : Set b} (R : REL A B r) i :
   _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys →
         Bisim R i (x ∷ xs) (y ∷ ys)
 
+infixr 5 _∷_
+
 module _ {R : Rel A r} where
 
  reflexive : Reflexive R → Reflexive (Bisim R i)
diff --git a/src/Data/Container/Core.agda b/src/Data/Container/Core.agda
@@ -38,6 +38,8 @@ map f = Prod.map₂ (f ∘_)
 
 -- Representation of container morphisms.
 
+infixr 8 _⇒_ _⊸_
+
 record _⇒_ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂)
            : Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂) where
   constructor _▷_
diff --git a/src/Data/Container/FreeMonad.agda b/src/Data/Container/FreeMonad.agda
@@ -103,6 +103,9 @@ module _ {P : Set ℓ}
  foldr : C ⋆ X → P
  foldr = induction (Function.const P) algP (algI ∘ -,_ ∘ □.proof)
 
+infixr -1 _<$>_ _<*>_
+infixl 1 _>>=_
+
 _<$>_ : (X → Y) → C ⋆ X → C ⋆ Y
 f <$> t = foldr (pure ∘ f) impure t
 
diff --git a/src/Data/Container/Indexed.agda b/src/Data/Container/Indexed.agda
@@ -31,6 +31,8 @@ open Container public
 -- Abbreviation for the commonly used level one version of indexed
 -- containers.
 
+infix 5 _▷_
+
 _▷_ : Set → Set → Set₁
 I ▷ O = Container I O zero zero
 
@@ -103,6 +105,8 @@ module _ {i₁ i₂ o₁ o₂}
 
 module _ {i o c r} {I : Set i} {O : Set o} where
 
+  infixr 8 _⇒_ _⊸_ _⇒C_
+
   _⇒_ : B.Rel (Container I O c r) _
   C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂
 
diff --git a/src/Data/Float/Base.agda b/src/Data/Float/Base.agda
@@ -65,5 +65,7 @@ open import Agda.Builtin.Float public
   ; primFloatATanh             to atanh
   )
 
+infix 4 _≈_
+
 _≈_ : Rel Float _
 _≈_ = _≡_ on Maybe.map Word.toℕ ∘ toWord
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
@@ -132,8 +132,8 @@ pred : ℕ → ℕ
 pred n = n ∸ 1
 
 infix  8 _!
-infixl 7 _⊓_ _/_ _%_
-infixl 6 _+⋎_ _⊔_
+infixl 7 _⊓_ _⊓′_ _/_ _%_
+infixl 6 _+⋎_ _⊔_ _⊔′_
 
 -- Argument-swapping addition. Used by Data.Vec._⋎_.
 
@@ -192,6 +192,8 @@ parity (suc (suc n)) = parity n
 
 -- Naïve exponentiation
 
+infixr 8 _^_
+
 _^_ : ℕ → ℕ → ℕ
 x ^ zero  = 1
 x ^ suc n = x * x ^ n
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
@@ -1948,6 +1948,8 @@ n≡⌈n+n/2⌉ (suc n′@(suc n)) =
 1≤n! zero    = ≤-refl
 1≤n! (suc n) = *-mono-≤ (m≤m+n 1 n) (1≤n! n)
 
+infix 4 _!≢0 _!*_!≢0
+
 _!≢0 : ∀ n → NonZero (n !)
 n !≢0 = >-nonZero (1≤n! n)
 
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
@@ -91,6 +91,8 @@ drop-*≡* (*≡* eq) = eq
      ↥ z ℤ.* ↧ x ℤ.* ↧ y ∎))
   where open ≡-Reasoning
 
+infix 4 _≃?_
+
 _≃?_ : Decidable _≃_
 p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p)
 
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -49,6 +49,8 @@ private
     x x′ y y′ : V
     kx : Key × V
 
+infix 4 _≈ₖᵥ_
+
 _≈ₖᵥ_ : Rel (Key × V) _
 _≈ₖᵥ_ = _≈_ ×ᴿ _≡_
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
@@ -184,6 +184,7 @@ module Lexicographic {A : Set a} {B : A → Set b}
                      (RelA : Rel A ℓ₁)
                      (RelB : ∀ x → Rel (B x) ℓ₂) where
 
+  infix 4 _<_
   data _<_ : Rel (Σ A B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
     left  : ∀ {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA   x₁ x₂) → (x₁ , y₁) < (x₂ , y₂)
     right : ∀ {x y₁ y₂}     (y₁<y₂ : RelB x y₁ y₂) → (x  , y₁) < (x  , y₂)
