Use superscript and add missing fixity (#1807)

Author: Akshobhya1234

src/Algebra/Bundles.agda

@@ -1305,6 +1305,10 @@ record Loop  c ℓ : Set (suc (c ⊔ ℓ)) where
     using (_≉_; ∙-rawMagma; \\-rawMagma; //-rawMagma)
 
 record LeftBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infixl 7 _\\_
+  infixl 7 _//_
+  infix  4 _≈_
   field
     Carrier : Set c
     _≈_     : Rel Carrier ℓ
@@ -1323,6 +1327,10 @@ record LeftBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
     using (quasigroup)
 
 record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infixl 7 _\\_
+  infixl 7 _//_
+  infix  4 _≈_
   field
     Carrier : Set c
     _≈_     : Rel Carrier ℓ
@@ -1341,6 +1349,10 @@ record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
     using (quasigroup)
 
 record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infixl 7 _\\_
+  infixl 7 _//_
+  infix  4 _≈_
   field
     Carrier : Set c
     _≈_     : Rel Carrier ℓ

src/Algebra/Construct/DirectProduct.agda

@@ -117,8 +117,8 @@ alternativeMagma : AlternativeMagma a ℓ₁ → AlternativeMagma b ℓ₂ → A
 alternativeMagma G H = record
   { isAlternativeMagma = record
     { isMagma = Magma.isMagma (magma G.magma H.magma)
-    ; alter = (λ x y → G.leftAlternative , H.leftAlternative <*> x <*> y)
-            , (λ x y → G.rightAlternative , H.rightAlternative <*> x <*> y)
+    ; alter = (λ x y → G.alternativeˡ , H.alternativeˡ <*> x <*> y)
+            , (λ x y → G.alternativeʳ , H.alternativeʳ <*> x <*> y)
     }
   } where module G = AlternativeMagma G; module H = AlternativeMagma H
 
@@ -142,8 +142,8 @@ semimedialMagma : SemimedialMagma a ℓ₁ → SemimedialMagma b ℓ₂ → Semi
 semimedialMagma G H = record
   { isSemimedialMagma = record
     { isMagma = Magma.isMagma (magma G.magma H.magma)
-    ; semiMedial = (λ x y z → G.leftSemimedial , H.leftSemimedial <*> x <*> y <*> z)
-                 , ((λ x y z → G.rightSemimedial , H.rightSemimedial <*> x <*> y <*> z))
+    ; semiMedial = (λ x y z → G.semimedialˡ , H.semimedialˡ <*> x <*> y <*> z)
+                 , ((λ x y z → G.semimedialʳ , H.semimedialʳ <*> x <*> y <*> z))
     }
   } where module G = SemimedialMagma G; module H = SemimedialMagma H
 

src/Algebra/Properties/CommutativeSemigroup.agda

@@ -142,17 +142,17 @@ xy∙xx≈x∙yxx x y = assoc x y ((x ∙ x))
 ------------------------------------------------------------------------------
 -- commutative semigroup is left/right/middle semiMedial
 
-leftSemimedial : LeftSemimedial _∙_
-leftSemimedial x y z = begin
+semimedialˡ : LeftSemimedial _∙_
+semimedialˡ x y z = begin
   (x ∙ x) ∙ (y ∙ z) ≈⟨ assoc x x (y ∙ z) ⟩
   x ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (sym (assoc x y z)) ⟩
   x ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
   x ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
   x ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc x y ((x ∙ z))) ⟩
   (x ∙ y) ∙ (x ∙ z) ∎
 
-rightSemimedial : RightSemimedial _∙_
-rightSemimedial x y z = begin
+semimedialʳ : RightSemimedial _∙_
+semimedialʳ x y z = begin
   (y ∙ z) ∙ (x ∙ x) ≈⟨ assoc y z (x ∙ x) ⟩
   y ∙ (z ∙ (x ∙ x)) ≈⟨ ∙-congˡ (sym (assoc z x x)) ⟩
   y ∙ ((z ∙ x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm z x)) ⟩

src/Algebra/Properties/Semigroup.agda

@@ -17,14 +17,14 @@ open import Data.Product
 x∙yz≈xy∙z : ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ y) ∙ z
 x∙yz≈xy∙z x y z = sym (assoc x y z)
 
-leftAlternative : LeftAlternative _∙_
-leftAlternative x y = assoc x x y
+alternativeˡ : LeftAlternative _∙_
+alternativeˡ x y = assoc x x y
 
-rightAlternative : RightAlternative _∙_
-rightAlternative x y = sym (assoc x y y)
+alternativeʳ : RightAlternative _∙_
+alternativeʳ x y = sym (assoc x y y)
 
 alternative : Alternative _∙_
-alternative = leftAlternative , rightAlternative
+alternative = alternativeˡ , alternativeʳ
 
 flexible : Flexible _∙_
 flexible x y = assoc x y x

src/Algebra/Structures.agda

@@ -67,11 +67,11 @@ record IsAlternativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
 
   open IsMagma isMagma public
 
-  leftAlternative : LeftAlternative ∙
-  leftAlternative = proj₁ alter
+  alternativeˡ : LeftAlternative ∙
+  alternativeˡ = proj₁ alter
 
-  rightAlternative : RightAlternative ∙
-  rightAlternative = proj₂ alter
+  alternativeʳ : RightAlternative ∙
+  alternativeʳ = proj₂ alter
 
 record IsFlexibleMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
   field
@@ -94,11 +94,11 @@ record IsSemimedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
 
   open IsMagma isMagma public
 
-  leftSemimedial : LeftSemimedial ∙
-  leftSemimedial = proj₁ semiMedial
+  semimedialˡ : LeftSemimedial ∙
+  semimedialˡ = proj₁ semiMedial
 
-  rightSemimedial : RightSemimedial ∙
-  rightSemimedial = proj₂ semiMedial
+  semimedialʳ : RightSemimedial ∙
+  semimedialʳ = proj₂ semiMedial
 
 record IsSelectiveMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
   field