PDF cleanup: rename union symbol

src/Axiom/Set/Map.agda

@@ -153,22 +153,22 @@ singletonᵐ a b = ❴ (a , b) ❵
 ❴ k , v ❵ᵐ = singletonᵐ k v
 
 module Unionᵐ (sp-∈ : spec-∈ A) where
-  infixr 6 _∪ᵐˡ_
+  infixr 6 _∪ˡ_
 
-  _∪ᵐˡ'_ : Rel A B → Rel A B → Rel A B
-  m ∪ᵐˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m'
+  _∪ˡ'_ : Rel A B → Rel A B → Rel A B
+  m ∪ˡ' m' = m ∪ filter (sp-∘ (sp-¬ (sp-∈ {dom m})) proj₁) m'
 
-  _∪ᵐˡ_ : Map A B → Map A B → Map A B
-  m ∪ᵐˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m')
+  _∪ˡ_ : Map A B → Map A B → Map A B
+  m ∪ˡ m' = disj-∪ m (filterᵐ (sp-∘ (sp-¬ sp-∈) proj₁) m')
       (∈⇔P -⟨ (λ where x (_ , refl , hy) → proj₁ (∈⇔P hy) (∈⇔P x)) ⟩- ∈⇔P)
 
-  disjoint-∪ᵐˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ᵐˡ' R' ≡ᵉ R ∪ R'
-  disjoint-∪ᵐˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔
+  disjoint-∪ˡ-∪ : (H : disjoint (dom R) (dom R')) → R ∪ˡ' R' ≡ᵉ R ∪ R'
+  disjoint-∪ˡ-∪ disj = from ≡ᵉ⇔≡ᵉ' λ _ → mk⇔
     (∈-∪⁺ ∘′ map₂ (proj₂ ∘′ ∈⇔P) ∘′ ∈⇔P)
     (∈⇔P ∘′ map₂ (to ∈-filter ∘′ (λ h → (flip disj (∈-map⁺'' h)) , h)) ∘ ∈⇔P)
 
   insert : Map A B → A → B → Map A B
-  insert m a b = ❴ a , b ❵ᵐ ∪ᵐˡ m
+  insert m a b = ❴ a , b ❵ᵐ ∪ˡ m
 
   insertIfJust : ⦃ DecEq A ⦄ → A → Maybe B → Map A B → Map A B
   insertIfJust x nothing  m  = m
@@ -281,7 +281,7 @@ module Restrictionᵐ (sp-∈ : spec-∈ A) where
 
   -- map only values in X
   mapValueRestricted : (B → B) → Map A B → Set A → Map A B
-  mapValueRestricted f m X = mapValues f (m ∣ X) ∪ᵐˡ m
+  mapValueRestricted f m X = mapValues f (m ∣ X) ∪ˡ m
 
   -- map only value at a
   mapSingleValue : (B → B) → Map A B → A → Map A B

src/Axiom/Set/Sum.agda

@@ -125,20 +125,20 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
 
     open Unionᵐ sp-∈
 
-    ∪ᵐˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ᵐˡ' R')
-    ∪ᵐˡ-finite Rᶠ R'ᶠ = ∪-preserves-finite Rᶠ
+    ∪ˡ-finite : {R R' : Rel A B} → finite R → finite R' → finite (R ∪ˡ' R')
+    ∪ˡ-finite Rᶠ R'ᶠ = ∪-preserves-finite Rᶠ
                       $ filter-finite (sp-∘ (sp-¬ sp-∈) _) (¬? ∘ ∈-A-dec ∘ _) R'ᶠ
 
-    _∪ᵐˡᶠ_ : FinMap A B → FinMap A B → FinMap A B
-    (_ , hX , Xᶠ) ∪ᵐˡᶠ (_ , hY , Yᶠ) =
-      toFinMap ((_ , hX) ∪ᵐˡ (_ , hY)) (∪ᵐˡ-finite Xᶠ Yᶠ)
+    _∪ˡᶠ_ : FinMap A B → FinMap A B → FinMap A B
+    (_ , hX , Xᶠ) ∪ˡᶠ (_ , hY , Yᶠ) =
+      toFinMap ((_ , hX) ∪ˡ (_ , hY)) (∪ˡ-finite Xᶠ Yᶠ)
 
     indexedSumᵐ-∪ : ∀ {X Y : FinMap A B} {f}
       → disjoint (dom (toRel X)) (dom (toRel Y))
-      → indexedSumᵐ f (X ∪ᵐˡᶠ Y) ≈ indexedSumᵐ f X ∙ indexedSumᵐ f Y
+      → indexedSumᵐ f (X ∪ˡᶠ Y) ≈ indexedSumᵐ f X ∙ indexedSumᵐ f Y
     indexedSumᵐ-∪ {X = X'@(X , _ , Xᶠ)} {Y'@(Y , _ , Yᶠ)} {f} disj = begin
-      indexedSumᵐ f (X' ∪ᵐˡᶠ Y')    ≈⟨ indexedSum-cong {x = -, ∪ᵐˡ-finite Xᶠ Yᶠ} {(X ∪ Y) ᶠ}
-                                         $ disjoint-∪ᵐˡ-∪ disj ⟩
+      indexedSumᵐ f (X' ∪ˡᶠ Y')    ≈⟨ indexedSum-cong {x = -, ∪ˡ-finite Xᶠ Yᶠ} {(X ∪ Y) ᶠ}
+                                         $ disjoint-∪ˡ-∪ disj ⟩
       indexedSum f ((X ∪ Y) ᶠ)      ≈⟨ indexedSum-∪ (disjoint-dom⇒disjoint disj) ⟩
       indexedSumᵐ f X' ∙ indexedSumᵐ f Y' ∎
       where instance _ = Xᶠ
@@ -147,14 +147,14 @@ module _ ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq B ⦄ where
     indexedSumᵐ-partition : ∀ {m m₁ m₂ : FinMap A B} {f} → toRel m ≡ toRel m₁ ⨿ toRel m₂
                           → indexedSumᵐ f m ≈ indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂
     indexedSumᵐ-partition {m} {m₁} {m₂} {f} m≡m₁∪m₂ = begin
-      indexedSumᵐ f m                     ≈⟨ indexedSumᵐ-cong {x = m} {m₁ ∪ᵐˡᶠ m₂} helper ⟩
-      indexedSumᵐ f (m₁ ∪ᵐˡᶠ m₂)          ≈⟨ indexedSumᵐ-∪ {X = m₁} {Y = m₂} disj-dom' ⟩
-      indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂ ∎
+      indexedSumᵐ f m                     ≈⟨ indexedSumᵐ-cong {x = m} {m₁ ∪ˡᶠ m₂} helper ⟩
+      indexedSumᵐ f (m₁ ∪ˡᶠ m₂)           ≈⟨ indexedSumᵐ-∪ {X = m₁} {Y = m₂} disj-dom' ⟩
+      indexedSumᵐ f m₁ ∙ indexedSumᵐ f m₂  ∎
       where module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence
             disj-dom' = disj-dom {m = toMap m} {toMap m₁} {toMap m₂} m≡m₁∪m₂
 
-            helper : toRel m ≡ᵉ toRel (m₁ ∪ᵐˡᶠ m₂)
-            helper = ≡ᵉ.trans (proj₁ m≡m₁∪m₂) (≡ᵉ.sym $ disjoint-∪ᵐˡ-∪ disj-dom')
+            helper : toRel m ≡ᵉ toRel (m₁ ∪ˡᶠ m₂)
+            helper = ≡ᵉ.trans (proj₁ m≡m₁∪m₂) (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj-dom')
 
   syntax indexedSumᵐ  (λ a → x) m = Σᵐ[ a ← m ] x
   syntax indexedSumᵐᵛ (λ a → x) m = Σᵐᵛ[ a ← m ] x

src/Ledger/Deleg.lagda

@@ -123,18 +123,18 @@ data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Set whe
     c ∉ dom pools
     ────────────────────────────────
     pp ⊢  ⟦ pools , retiring ⟧ᵖ ⇀⦇ regpool c poolParams ,POOL⦈
-          ⟦ ❴ c , poolParams ❵ᵐ ∪ᵐˡ pools , retiring ⟧ᵖ
+          ⟦ ❴ c , poolParams ❵ᵐ ∪ˡ pools , retiring ⟧ᵖ
 
   POOL-retirepool :
     pp ⊢  ⟦ pools , retiring ⟧ᵖ ⇀⦇ retirepool c e ,POOL⦈
-          ⟦ pools , ❴ c , e ❵ᵐ ∪ᵐˡ retiring ⟧ᵖ
+          ⟦ pools , ❴ c , e ❵ᵐ ∪ˡ retiring ⟧ᵖ
 
 data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Set where
   GOVCERT-regdrep : let open PParams pp in
     (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
     ────────────────────────────────
     ⟦ e , pp , vs ⟧ᶜ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ regdrep c d an ,GOVCERT⦈
-                        ⟦ ❴ c , e + drepActivity ❵ᵐ ∪ᵐˡ dReps , ccKeys ⟧ᵛ
+                        ⟦ ❴ c , e + drepActivity ❵ᵐ ∪ˡ dReps , ccKeys ⟧ᵛ
 
   GOVCERT-deregdrep :
     c ∈ dom dReps
@@ -146,7 +146,7 @@ data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → S
     (c , nothing) ∉ ccKeys
     ────────────────────────────────
     Γ ⊢  ⟦ dReps , ccKeys ⟧ᵛ ⇀⦇ ccreghot c mc ,GOVCERT⦈
-         ⟦ dReps , singletonᵐ c mc ∪ᵐˡ ccKeys ⟧ᵛ
+         ⟦ dReps , singletonᵐ c mc ∪ˡ ccKeys ⟧ᵛ
 \end{code}
 \caption{Auxiliary DELEG and POOL rules}
 \end{figure*}

src/Ledger/GovernanceActions.lagda

@@ -322,7 +322,7 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
     ∀[ term ∈ range new ] term ≤ (s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e)
     ────────────────────────────────
     ⟦ gid , t , e ⟧ᵉ ⊢  s ⇀⦇ NewCommittee new rem q ,ENACT⦈
-                record  s { cc = just ((new ∪ᵐˡ old) ∣ rem ᶜ , q) , gid }
+                record  s { cc = just ((new ∪ˡ old) ∣ rem ᶜ , q) , gid }
 
   Enact-NewConst :
     ⟦ gid , t , e ⟧ᵉ ⊢  s ⇀⦇ NewConstitution dh sh ,ENACT⦈

src/Ledger/PPUp.lagda

@@ -95,7 +95,7 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update →
     → epoch slot ≡ e
     ────────────────────────────────
     Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈
-        record { pup = pup ∪ᵐˡ pupˢ ; fpup = fpupˢ }
+        record { pup = pup ∪ˡ pupˢ ; fpup = fpupˢ }
 
   PPUpdateFuture : let open PPUpdateEnv Γ in
     dom pup ⊆ dom genDelegs
@@ -104,7 +104,7 @@ data _⊢_⇀⦇_,PPUP⦈_ : PPUpdateEnv → PPUpdateState → Maybe Update →
     → sucᵉ (epoch slot) ≡ e
     ────────────────────────────────
     Γ ⊢ record { pup = pupˢ ; fpup = fpupˢ } ⇀⦇ just (pup , e) ,PPUP⦈
-        record { pup = pupˢ ; fpup = pup ∪ᵐˡ fpupˢ }
+        record { pup = pupˢ ; fpup = pup ∪ˡ fpupˢ }
 \end{code}
 \caption{PPUP inference rules}
 \end{figure*}

src/Ledger/Ratify.lagda

@@ -229,17 +229,17 @@ restrictedDists coins rank dists = dists
   where open StakeDistrs dists
         -- one always includes the other
         restrict : Credential ⇀ Coin → Credential ⇀ Coin
-        restrict dist = topNDRepDist rank dist ∪ᵐˡ mostStakeDRepDist dist coins
+        restrict dist = topNDRepDist rank dist ∪ˡ mostStakeDRepDist dist coins
 \end{code}
 \begin{figure*}[h!]
 {\small
 \begin{code}
 actualVotes : RatifyEnv → CCData → (GovRole × Credential) ⇀ Vote → GovAction → PParams
             → VDeleg ⇀ Vote
 actualVotes Γ cc votes ga pparams
-  =    mapKeys (credVoter CC) actualCCVotes
-  ∪ᵐˡ  actualPDRepVotes ∪ᵐˡ actualDRepVotes
-  ∪ᵐˡ  actualSPOVotes
+  =   mapKeys (credVoter CC) actualCCVotes
+  ∪ˡ  actualPDRepVotes ∪ˡ actualDRepVotes
+  ∪ˡ  actualSPOVotes
   where
     open RatifyEnv Γ
     open PParams pparams
@@ -267,17 +267,17 @@ actualVotes Γ cc votes ga pparams
       (nothing        , _)      → ∅ᵐ
 
     actualPDRepVotes
-      =    ❴ abstainRep       , Vote.abstain ❵ᵐ
-      ∪ᵐˡ  ❴ noConfidenceRep  , (case ga of λ where  NoConfidence  → Vote.yes
-                                                     _             → Vote.no) ❵ᵐ
+      =   ❴ abstainRep       , Vote.abstain ❵ᵐ
+      ∪ˡ  ❴ noConfidenceRep  , (case ga of λ where  NoConfidence  → Vote.yes
+                                                    _             → Vote.no) ❵ᵐ
 
     actualDRepVotes
-      =    roleVotes GovRole.DRep
-      ∪ᵐˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no
+      =   roleVotes GovRole.DRep
+      ∪ˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no
 
     actualSPOVotes
-      =    roleVotes GovRole.SPO
-      ∪ᵐˡ  constMap spos (if isHF then Vote.no else Vote.abstain)
+      =   roleVotes GovRole.SPO
+      ∪ˡ  constMap spos (if isHF then Vote.no else Vote.abstain)
       where
         spos : ℙ VDeleg
         spos = filterˢ isSPOProp $ dom (StakeDistrs.stakeDistr stakeDistrs)

src/Ledger/Utxo.lagda

@@ -319,7 +319,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where
     -- Add deposits
 
        ────────────────────────────────
-       Γ ⊢ s ⇀⦇ tx ,UTXO⦈  ⟦ (utxo ∣ txins ᶜ) ∪ᵐˡ (outs txb)
+       Γ ⊢ s ⇀⦇ tx ,UTXO⦈  ⟦ (utxo ∣ txins ᶜ) ∪ˡ outs txb
                            , fees + txfee
                            , updateDeposits pp txb deposits
                            , donations + txdonation

src/Ledger/Utxo/Properties.lagda

@@ -60,13 +60,13 @@ private
   ∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism)
 
 balance-∪ : disjoint (dom utxo) (dom utxo')
-                     → cbalance (utxo ∪ᵐˡ utxo') ≡ cbalance utxo + cbalance utxo'
+                     → cbalance (utxo ∪ˡ utxo') ≡ cbalance utxo + cbalance utxo'
 balance-∪ {utxo} {utxo'} h = begin
-  cbalance (utxo ∪ᵐˡ utxo')
+  cbalance (utxo ∪ˡ utxo')
     ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism
-    $ indexedSumᵐ-cong {x = (utxo ∪ᵐˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ)} (id , id)
+    $ indexedSumᵐ-cong {x = (utxo ∪ˡ utxo') ᶠᵐ} {(utxo ᶠᵐ) ∪ˡᶠ (utxo' ᶠᵐ)} (id , id)
     ⟩
-  coin (indexedSumᵐ _ ((utxo ᶠᵐ) ∪ᵐˡᶠ (utxo' ᶠᵐ)))
+  coin (indexedSumᵐ _ ((utxo ᶠᵐ) ∪ˡᶠ (utxo' ᶠᵐ)))
     ≡⟨ ⟦⟧-cong coinIsMonoidHomomorphism
     $ indexedSumᵐ-∪ {X = utxo ᶠᵐ} {utxo' ᶠᵐ} h
     ⟩
@@ -249,15 +249,15 @@ module DepositHelpers
 
   utxo-ref-prop :
     cbalance utxo + ref ≡
-    (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + txfee) + txdonation + tot
+    (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + txfee) + txdonation + tot
   utxo-ref-prop = begin
     cbalance utxo + ref
       ≡˘⟨ cong (_+ ref)
-        $ balance-cong-coin {utxo = (utxo ∣ txins ᶜ) ∪ᵐˡ (utxo ∣ txins)}{utxo}
-        $    disjoint-∪ᵐˡ-∪ (disjoint-sym res-ex-disjoint)
+        $ balance-cong-coin {utxo = (utxo ∣ txins ᶜ) ∪ˡ (utxo ∣ txins)}{utxo}
+        $    disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
         ≡ᵉ-∘ ∪-sym
         ≡ᵉ-∘ res-ex-∪ (_∈? txins) ⟩
-    cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ (utxo ∣ txins)) + ref
+    cbalance ((utxo ∣ txins ᶜ) ∪ˡ (utxo ∣ txins)) + ref
       ≡⟨ cong (_+ ref)
        $ balance-∪ {utxo ∣ txins ᶜ} {utxo ∣ txins}
           $ flip res-ex-disjoint ⟩
@@ -273,17 +273,17 @@ module DepositHelpers
       ℕ.+ tot ℕ.+ txdonation
       ≡˘⟨ cong (λ x → (x + txfee) + tot + txdonation)
         $ balance-∪ {utxo ∣ txins ᶜ} {outs txb} h ⟩
-    (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee)
+    (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee)
       ℕ.+ tot ℕ.+ txdonation
       ≡t⟨⟩
-    (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee)
+    (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee)
       ℕ.+ (tot ℕ.+ txdonation)
-      ≡⟨ cong ((cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) + txfee) +_)
+      ≡⟨ cong ((cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) + txfee) +_)
        $ +-comm tot txdonation ⟩
-    (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee)
+    (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee)
       ℕ.+ (txdonation ℕ.+ tot)
       ≡t⟨⟩
-    (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee)
+    (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee)
       ℕ.+ txdonation ℕ.+ tot
       ∎ where open IsEquivalence ≡ᵉ-isEquivalence renaming (trans to infixl 4 _≡ᵉ-∘_)
 
@@ -380,24 +380,24 @@ pov {tx}{utxo}{_}{fees}{deposits}{donations}
             ≡t⟨⟩
           cbalance utxo ℕ.+ ref ℕ.+ (remDepTot ℕ.+ fees)
             ≡⟨ cong (_+ (remDepTot + fees)) utxo-ref-prop ⟩
-          (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) ℕ.+ txfee)
+          (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) ℕ.+ txfee)
             ℕ.+ txdonation ℕ.+ tot ℕ.+ (remDepTot ℕ.+ fees)
             ≡t⟨⟩
-          cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb)
+          cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb)
             ℕ.+ (txfee ℕ.+ txdonation ℕ.+ (tot ℕ.+ remDepTot) ℕ.+ fees)
-            ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb) +_) rearrange0 ⟩
-          cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb)
+            ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb) +_) rearrange0 ⟩
+          cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb)
             + ((fees + txfee) + getCoin deposits' + txdonation)
             ∎ ⟩
-    cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb)
+    cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb)
       ℕ.+ ((fees + txfee) ℕ.+ getCoin deposits' ℕ.+ txdonation) ℕ.+ donations
       ≡t⟨⟩
-    cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb)
+    cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb)
       ℕ.+ (fees + txfee) ℕ.+ getCoin deposits' ℕ.+ (txdonation ℕ.+ donations)
-      ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb)
+      ≡⟨ cong (cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb)
                 + (fees + txfee) + getCoin deposits' ℕ.+_)
        $ +-comm txdonation donations ⟩
-    cbalance ((utxo ∣ txins ᶜ) ∪ᵐˡ outs txb)
+    cbalance ((utxo ∣ txins ᶜ) ∪ˡ outs txb)
       + (fees + txfee) + getCoin deposits' + (donations + txdonation)
       ∎
 \end{code}

src/latex/agda-latex-macros.sty

@@ -177,7 +177,7 @@
 \newcommand{\Credential}{\AgdaFunction{Credential}\xspace}
 \newcommand{\credVoter}{\AgdaInductiveConstructor{credVoter}\xspace}
 \newcommand{\Crypto}{\AgdaRecord{Crypto}\xspace}
-\newcommand{\cupsupermsuperl}{\AgdaFunction{∪ᵐˡ}\xspace}
+\newcommand{\cupsupermsuperl}{\AgdaFunction{∪ˡ}\xspace}
 \newcommand{\cupsuperplus}{\AgdaFunction{∪⁺}\xspace}
 \newcommand{\currentEpoch}{\AgdaField{currentEpoch}\xspace}