Rename ∅ → ⟦⟧ and ∅ᵐ → ∅

Addresses one item of #282

src/Axiom/Set.agda

@@ -167,13 +167,13 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
   ∈-unions : {a : A} {U : Set (Set A)} → (∃[ T ] T ∈ U × a ∈ T) ⇔ a ∈ proj₁ (unions U)
   ∈-unions = proj₂ $ unions _
 
-  ∅ : Set A
-  ∅ = fromList []
+  ⟦⟧ : Set A
+  ⟦⟧ = fromList []
 
-  ∅-strongly-finite : strongly-finite {A} ∅
+  ∅-strongly-finite : strongly-finite {A} ⟦⟧
   ∅-strongly-finite = [] , [] , R.SK-sym ∈-fromList
 
-  card-∅ : card (∅ {A} , ∅-strongly-finite) ≡ 0
+  card-∅ : card (⟦⟧ {A} , ∅-strongly-finite) ≡ 0
   card-∅ = refl
 
   singleton : A → Set A
@@ -189,12 +189,12 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
     where open R.EquationalReasoning
 
   partialToSet : (A → Maybe B) → A → Set B
-  partialToSet f a = maybe (fromList ∘ [_]) ∅ (f a)
+  partialToSet f a = maybe (fromList ∘ [_]) ⟦⟧ (f a)
 
   ∈-partialToSet : ∀ {a : A} {b : B} {f} → f a ≡ just b ⇔ b ∈ partialToSet f a
   ∈-partialToSet {a = a} {b} {f} = mk⇔
-    (λ h → subst (λ x → b ∈ maybe (fromList ∘ [_]) ∅ x) (sym h) (to ∈-singleton refl))
-    (case f a returning (λ y → b ∈ maybe (λ x → fromList [ x ]) ∅ y → y ≡ just b) of
+    (λ h → subst (λ x → b ∈ maybe (fromList ∘ [_]) ⟦⟧ x) (sym h) (to ∈-singleton refl))
+    (case f a returning (λ y → b ∈ maybe (λ x → fromList [ x ]) ⟦⟧ y → y ≡ just b) of
       λ where (just x) → λ h → cong just (sym $ from ∈-singleton h)
               nothing  → λ h → case from ∈-fromList h of λ ())
 
@@ -269,7 +269,7 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
       where open R.EquationalReasoning
 
     disjoint' : Set A → Set A → Type ℓ
-    disjoint' X Y = X ∩ Y ≡ᵉ ∅
+    disjoint' X Y = X ∩ Y ≡ᵉ ⟦⟧
 
   All : (A → Type) → Set A → Type ℓ
   All P X = ∀ {a} → a ∈ X → P a

src/Axiom/Set/Map.agda

@@ -58,7 +58,7 @@ record IsLeftUnique (R : Rel A B) : Type where
   field isLeftUnique : left-unique R
 
 instance
-  ∅-left-unique : IsLeftUnique {A = A} {B = B} ∅
+  ∅-left-unique : IsLeftUnique {A = A} {B = B} ⟦⟧
   ∅-left-unique .IsLeftUnique.isLeftUnique h h' = ⊥-elim $ ∉-∅ h
 
 ⊆-left-unique : R ⊆ R' → left-unique R' → left-unique R
@@ -96,8 +96,8 @@ _≡ᵉᵐ_ = _≡ᵉ_ on _ˢ
 instance
   _ = ˢ-left-unique
 
-∅ᵐ : Map A B
-∅ᵐ = _ᵐ ∅ ⦃ ∅-left-unique ⦄
+∅ : Map A B
+∅ = _ᵐ ⟦⟧ ⦃ ∅-left-unique ⦄
 
 fromListᵐ : ⦃ _ : DecEq A ⦄ → List (A × B) → Map A B
 fromListᵐ l = fromList (deduplicate (λ x y → proj₁ x ≟ proj₁ y) l) ,

src/Axiom/Set/Map/Dec.agda

@@ -57,4 +57,4 @@ module Lookupᵐᵈ (sp-∈ : spec-∈ A) where
     _∪⁺_ = unionWith (fold id id _∙_)
 
     aggregate₊ : FinSet (A × V) → Map A V
-    aggregate₊ (_ , l , _) = foldl (λ m x → m ∪⁺ ❴ x ❵ᵐ) ∅ᵐ l
+    aggregate₊ (_ , l , _) = foldl (λ m x → m ∪⁺ ❴ x ❵ᵐ) ∅ l

src/Axiom/Set/Properties.agda

@@ -153,25 +153,25 @@ map-⊆ x⊆y a∈map with from ∈-map a∈map
 map-≡ᵉ : {X Y : Set A} {f : A → B} → X ≡ᵉ Y → map f X ≡ᵉ map f Y
 map-≡ᵉ (x⊆y , y⊆x) = map-⊆ x⊆y , map-⊆ y⊆x
 
-∉-∅ : {a : A} → a ∉ ∅
+∉-∅ : {a : A} → a ∉ ⟦⟧
 ∉-∅ h = case ∈⇔P h of λ ()
 
-∅-minimum : Minimum (_⊆_ {A}) ∅
+∅-minimum : Minimum (_⊆_ {A}) ⟦⟧
 ∅-minimum = λ _ → ⊥-elim ∘ ∉-∅
 
-∅-least : X ⊆ ∅ → X ≡ᵉ ∅
+∅-least : X ⊆ ⟦⟧ → X ≡ᵉ ⟦⟧
 ∅-least X⊆∅ = (X⊆∅ , ∅-minimum _)
 
-∅-weakly-finite : weakly-finite {A = A} ∅
+∅-weakly-finite : weakly-finite {A = A} ⟦⟧
 ∅-weakly-finite = [] , ⊥-elim ∘ ∉-∅
 
-∅-finite : finite {A = A} ∅
+∅-finite : finite {A = A} ⟦⟧
 ∅-finite = [] , mk⇔ (⊥-elim ∘ ∉-∅) λ ()
 
-map-∅ : {X : Set A} {f : A → B} → map f ∅ ≡ᵉ ∅
+map-∅ : {X : Set A} {f : A → B} → map f ⟦⟧ ≡ᵉ ⟦⟧
 map-∅ = ∅-least λ x∈map → case ∈-map⁻' x∈map of λ where (_ , _ , h) → ⊥-elim (∉-∅ h)
 
-mapPartial-∅ : {f : A → Maybe B} → mapPartial f ∅ ≡ᵉ ∅
+mapPartial-∅ : {f : A → Maybe B} → mapPartial f ⟦⟧ ≡ᵉ ⟦⟧
 mapPartial-∅ {f = f} = ∅-least λ x∈map → case from (∈-mapPartial {f = f}) x∈map of λ where
   (_ , h , _) → ⊥-elim (∉-∅ h)
 
@@ -242,7 +242,7 @@ Set-JoinSemilattice : IsJoinSemilattice (_≡ᵉ_ {A}) _⊆_ _∪_
 Set-JoinSemilattice = record
   { isPartialOrder = ⊆-PartialOrder ; supremum = ∪-Supremum }
 
-Set-BoundedJoinSemilattice : IsBoundedJoinSemilattice (_≡ᵉ_ {A}) _⊆_ _∪_ ∅
+Set-BoundedJoinSemilattice : IsBoundedJoinSemilattice (_≡ᵉ_ {A}) _⊆_ _∪_ ⟦⟧
 Set-BoundedJoinSemilattice = record
   { isJoinSemilattice = Set-JoinSemilattice ; minimum = ∅-minimum }
 

src/Axiom/Set/Rel.agda

@@ -49,7 +49,7 @@ relatedˡ : Rel A B → Set A
 relatedˡ = map proj₁
 
 ∅ʳ : Rel A B
-∅ʳ = ∅
+∅ʳ = ⟦⟧
 
 dom : Rel A B → Set A
 dom = map proj₁
@@ -100,7 +100,7 @@ dom-mapʳ⊆ a∈dmR with to dom∈ a∈dmR
 mapʳ-dom : {f : B → B'} → dom R ≡ᵉ dom (mapʳ f R)
 mapʳ-dom = dom-⊆mapʳ , dom-mapʳ⊆
 
-dom-∅ : dom R ⊆ ∅ → R ≡ᵉ ∅
+dom-∅ : dom R ⊆ ⟦⟧ → R ≡ᵉ ⟦⟧
 dom-∅ dom⊆∅ = ∅-least (λ {x} x∈R → ⊥-elim $ ∉-∅ $ dom⊆∅ $ from dom∈ (-, x∈R))
 
 mapPartialLiftKey : (A → B → Maybe B') → A × B → Maybe (A × B')
@@ -168,7 +168,7 @@ module Restriction (sp-∈ : spec-∈ A) where
   ex-⊆ : (R ∣ X ᶜ) ⊆ R
   ex-⊆ = proj₂ ∘′ ∈⇔P
 
-  res-∅ : R ∣ ∅ ≡ᵉ ∅
+  res-∅ : R ∣ ⟦⟧ ≡ᵉ ⟦⟧
   res-∅ = dom-∅ res-dom
 
   res-ex-∪ : Decidable (_∈ X) → (R ∣ X) ∪ (R ∣ X ᶜ) ≡ᵉ R

src/Axiom/Set/Sum.agda

@@ -89,7 +89,7 @@ module _ ⦃ _ : DecEq A ⦄ {f : A → Carrier} where
   indexedSum-cong : indexedSum f Preserves (_≡ᵉ_ on proj₁) ⟶ _≈_
   indexedSum-cong {x} {y} = factor-cong {x = x} {y}
 
-  indexedSum-∅ : indexedSum f (∅ , ∅-finite) ≈ ε
+  indexedSum-∅ : indexedSum f (⟦⟧ , ∅-finite) ≈ ε
   indexedSum-∅ = begin _ ∎
 
   indexedSum-∪ : ⦃ Xᶠ : finite X ⦄ ⦃ Yᶠ : finite Y ⦄ → disjoint X Y

src/Ledger/Chain.lagda

@@ -84,7 +84,7 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
              ((deposits ∣ ❴ GovActionDeposit gaid ❵) ˢ)
       govActionReturns = aggregate₊ $ mapˢ (λ (a , _ , d) → a , d) removedGovActions ᶠˢ
 
-      es        = record esW { withdrawals = ∅ᵐ }
+      es        = record esW { withdrawals = ∅ }
       retired   = retiring ⁻¹ e
       refunds   = govActionReturns ∪⁺ trWithdrawals ∣ dom rewards
       unclaimed = govActionReturns ∪⁺ trWithdrawals ∣ dom rewards ᶜ
@@ -113,7 +113,7 @@ data _⊢_⇀⦇_,NEWEPOCH⦈_ : NewEpochEnv → NewEpochState → Epoch → New
     in
     e ≡ sucᵉ lastEpoch
     → record { currentEpoch = e ; treasury = treasury ; GState gState ; NewEpochEnv Γ }
-        ⊢ ⟦ es , ∅ , false ⟧ʳ ⇀⦇ govSt' ,RATIFY⦈ fut'
+        ⊢ ⟦ es , ⟦⟧ , false ⟧ʳ ⇀⦇ govSt' ,RATIFY⦈ fut'
     ────────────────────────────────
     Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ ⟦ e , acnt' , ls' , es , fut' ⟧ⁿᵉ
 
@@ -150,7 +150,7 @@ govActionDeposits : LState → VDeleg ⇀ Coin
 govActionDeposits ls =
   let open LState ls; open CertState certState; open PState pState
       open UTxOState utxoSt; open DState dState
-   in foldl _∪⁺_ ∅ᵐ $ setToList $
+   in foldl _∪⁺_ ∅ $ setToList $
     mapPartial
       (λ where (gaid , record { returnAddr = record {stake = c} }) → do
         vd ← lookupᵐ? voteDelegs c ⦃ _ ∈? _ ⦄
@@ -162,8 +162,8 @@ calculateStakeDistrs : LState → StakeDistrs
 calculateStakeDistrs ls =
   let open LState ls; open CertState certState; open PState pState
       open UTxOState utxoSt; open DState dState
-      spoDelegs = ∅ᵐ -- TODO
-      drepDelegs = ∅ᵐ -- TODO
+      spoDelegs = ∅ -- TODO
+      drepDelegs = ∅ -- TODO
   in
   record
     { stakeDistr = govActionDeposits ls

src/Ledger/Chain/Properties.agda

@@ -25,7 +25,7 @@ module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where
   open NewEpochState nes hiding (es)
   open RatifyState fut using (removed) renaming (es to esW)
   open LState ls; open CertState certState; open Acnt acnt
-  es         = record esW { withdrawals = ∅ᵐ }
+  es         = record esW { withdrawals = ∅ }
   govSt'     = filter (λ x → ¿ ¬ proj₁ x ∈ mapˢ proj₁ removed ¿) govSt
 
   NEWEPOCH-total : ∃[ nes' ] Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes'
@@ -35,7 +35,7 @@ module _ {Γ : NewEpochEnv} {nes : NewEpochState} {e : Epoch} where
       (yes p) → -, NEWEPOCH-New p (pFut .proj₂)
     where pFut = RATIFY-total {record { currentEpoch = e ; treasury = treasury
                                       ; GState gState ; NewEpochEnv Γ }}
-                              {⟦ es , ∅ , false ⟧ʳ} {govSt'}
+                              {⟦ es , ⟦⟧ , false ⟧ʳ} {govSt'}
 
   NEWEPOCH-complete : ∀ nes' → Γ ⊢ nes ⇀⦇ e ,NEWEPOCH⦈ nes' → NEWEPOCH-total .proj₁ ≡ nes'
   NEWEPOCH-complete nes' h with h | e ≟ sucᵉ lastEpoch

src/Ledger/Foreign/HSLedger.agda

@@ -74,7 +74,7 @@ module Implementation where
     .Value-CommutativeMonoid   → +-0-commutativeMonoid
     .coin                      → id
     .inject                    → id
-    .policies                  → λ _ → ∅
+    .policies                  → λ _ → ⟦⟧
     .size                      → λ x → 1 -- there is only ada in this token algebra
     ._≤ᵗ_                      → _≤_
     .AssetName                 → String
@@ -157,7 +157,7 @@ HsGovParams = record
   { Implementation
   ; ppUpd = let open PParamsDiff in λ where
       .UpdateT                → ⊤
-      .updateGroups           → λ _ → ∅
+      .updateGroups           → λ _ → ⟦⟧
       .applyUpdate            → λ p _ → p
       .ppdWellFormed          → λ _ → false
       .ppdWellFormed⇒hasGroup → λ ()
@@ -247,7 +247,7 @@ instance
       ; mint       = ε -- tokenAlgebra only contains ada atm, so mint is surely empty
       ; txfee      = txfee
       ; txvldt     = from txvldt
-      ; txwdrls    = ∅ᵐ
+      ; txwdrls    = ∅
       ; txup       = nothing
       ; txADhash   = nothing
       ; netwrk     = nothing
@@ -277,7 +277,7 @@ instance
       }
     .from txw → let open F.TxWitnesses txw in record
       { vkSigs  = from vkSigs
-      ; scripts = ∅
+      ; scripts = ⟦⟧
       ; txdats  = from txdats
       ; txrdmrs = from txrdmrs
       }
@@ -372,7 +372,7 @@ instance
     .from s → let open F.UTxOState s in record
       { utxo      = from utxo
       ; fees      = fees
-      ; deposits  = ∅ᵐ
+      ; deposits  = ∅
       ; donations = ε
       }
 

src/Ledger/Gov.lagda

@@ -71,7 +71,7 @@ addAction : GovState
           → Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash a
           → GovState
 addAction s e aid addr a prev = s ∷ʳ (aid , record
-  { votes = ∅ᵐ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev })
+  { votes = ∅ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev })
 
 \end{code}
 \caption{Types and functions used in the GOV transition system}
@@ -103,7 +103,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
        actionWellFormed a ≡ true
     →  d ≡ govActionDeposit
     →  (∀ {new rem q} → a ≡ NewCommittee new rem q
-        → ∀[ e ∈ range new ]  epoch < e  ×  dom new ∩ rem ≡ᵉ ∅)
+        → ∀[ e ∈ range new ]  epoch < e  ×  dom new ∩ rem ≡ᵉ ⟦⟧)
     ───────────────────────────────────────
     (Γ , k) ⊢ s ⇀⦇ sig ,GOV'⦈ s'
 

src/Ledger/Gov/Properties.agda

@@ -42,7 +42,7 @@ instance
     case ¿ actionWellFormed a ≡ true × d ≡ pparams .PParams.govActionDeposit ¿
          ,′ isNewCommittee a of λ where
       (yes (wf , dep) , yes (new , rem , q , refl)) →
-        case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where
+        case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ⟦⟧ ¿ of λ where
           (yes newOk) → just (_ , GOV-Propose wf dep λ where refl → newOk)
           (no _)      → nothing
       (yes (wf , dep) , no notNewComm) → just (_ , GOV-Propose wf dep λ isNewComm → ⊥-elim (notNewComm (_ , _ , _ , isNewComm)))
@@ -57,7 +57,7 @@ instance
   ... | no ¬p | _ = ⊥-elim (¬p (wf , dep))
   ... | yes _ | no notNewComm = refl
   ... | yes _ | yes (new , rem , q , refl)
-    rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl
+    rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ⟦⟧ ¿ (newOk refl) .proj₂ = refl
 
 Computational-GOV : Computational _⊢_⇀⦇_,GOV⦈_
 Computational-GOV = it

src/Ledger/GovernanceActions.lagda

@@ -262,7 +262,7 @@ record EnactState : Set where
 
 ccCreds : HashProtected (Maybe ((Credential ⇀ Epoch) × ℚ)) → ℙ Credential
 ccCreds (just x  , _)  = dom (x .proj₁)
-ccCreds (nothing , _)  = ∅
+ccCreds (nothing , _)  = ⟦⟧
 \end{code}
 \caption{Enactment types}
 \label{fig:enactment-types}
@@ -305,7 +305,7 @@ data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactSta
     ⟦ gid , t , e ⟧ᵉ ⊢   s ⇀⦇ NoConfidence ,ENACT⦈
                  record  s { cc = nothing , gid }
 
-  Enact-NewComm : let old      = maybe proj₁ ∅ᵐ (s .EnactState.cc .proj₁)
+  Enact-NewComm : let old      = maybe proj₁ ∅ (s .EnactState.cc .proj₁)
                       maxTerm  = s .pparams .proj₁ .PParams.ccMaxTermLength +ᵉ e
                   in
     ∀[ term ∈ range new ] term ≤ maxTerm

src/Ledger/NewPP.lagda

@@ -25,8 +25,8 @@ record NewPParamState : Set where
 updatePPUp : PParams → PPUpdateState → PPUpdateState
 updatePPUp pparams record { fpup = fpup }
   with allᵇ (isViableUpdate? pparams) (range fpup)
-... | false  = record { pup = ∅ᵐ    ; fpup = ∅ᵐ }
-... | true   = record { pup = fpup  ; fpup = ∅ᵐ }
+... | false  = record { pup = ∅    ; fpup = ∅ }
+... | true   = record { pup = fpup  ; fpup = ∅ }
 
 votedValue : ProposedPPUpdates → PParams → ℕ → Maybe PParamsUpdate
 votedValue pup pparams quorum =

src/Ledger/PParams.lagda

@@ -135,7 +135,7 @@ record PParamsDiff : Set₁ where
         updateGroups : UpdateT → ℙ PParamGroup
         applyUpdate : PParams → UpdateT → PParams
         ppdWellFormed : UpdateT → Bool
-        ppdWellFormed⇒hasGroup : ∀ {u} → ppdWellFormed u ≡ true → updateGroups u ≢ ∅
+        ppdWellFormed⇒hasGroup : ∀ {u} → ppdWellFormed u ≡ true → updateGroups u ≢ ⟦⟧
         ppdWellFormed⇒WF       : ∀ {u} → ppdWellFormed u ≡ true → ∀ pp
                                → paramsWellFormed pp
                                → paramsWellFormed (applyUpdate pp u)

src/Ledger/Ratify.lagda

@@ -178,7 +178,7 @@ mostStakeDRepDist-0 = (proj₂ ∘ Equivalence.from ∈-filter)
                     , λ x → Equivalence.to ∈-filter (z≤n , x)
 
 -- TODO: maybe this can be proven easier with the maximum?
-mostStakeDRepDist-∅ : ∀ {dist} → ∃[ N ] mostStakeDRepDist dist N ˢ ≡ᵉ ∅
+mostStakeDRepDist-∅ : ∀ {dist} → ∃[ N ] mostStakeDRepDist dist N ˢ ≡ᵉ ⟦⟧
 mostStakeDRepDist-∅ {dist} = suc (∑ᵐᵛ[ x ← dist ᶠᵐ ] x) , Properties.∅-least
   (⊥-elim ∘ uncurry helper ∘ Equivalence.from ∈-filter)
   where
@@ -216,7 +216,7 @@ mostStakeDRepDist-∅ {dist} = suc (∑ᵐᵛ[ x ← dist ᶠᵐ ] x) , Properti
 
 topNDRepDist : ℕ → Credential ⇀ Coin → Credential ⇀ Coin
 topNDRepDist n dist = case (lengthˢ (dist ˢ) ≥? n) ,′ (n >? 0) of λ where
-  (_     , no  _)  → ∅ᵐ
+  (_     , no  _)  → ∅
   (no _  , yes _)  → dist
   (yes p , yes p₁) → mostStakeDRepDist dist (proj₁ (∃topNDRepDist {dist = dist} p p₁))
 
@@ -254,7 +254,7 @@ actualVotes Γ pparams cc ga votes  =   mapKeys (credVoter CC) (actualCCVotes cc
 
   activeCC : CCData → ℙ Credential
   activeCC (just (cc , _))  = dom $ filterᵐᵇ (is-just ∘ proj₂) (ccHotKeys ∣ dom cc)
-  activeCC nothing          = ∅
+  activeCC nothing          = ⟦⟧
 
   spos : ℙ VDeleg
   spos = filterˢ isSPOProp $ dom (StakeDistrs.stakeDistr stakeDistrs)
@@ -265,7 +265,7 @@ actualVotes Γ pparams cc ga votes  =   mapKeys (credVoter CC) (actualCCVotes cc
              _                        → Vote.abstain -- expired, no hot key or resigned
 
   actualCCVotes : CCData → Credential ⇀ Vote
-  actualCCVotes nothing          =  ∅ᵐ
+  actualCCVotes nothing          =  ∅
   actualCCVotes (just (cc , q))  =  ifᵈ (ccMinSize ≤ lengthˢ (activeCC $ just (cc , q)))
                                     then mapWithKey actualCCVote cc
                                     else constMap (dom cc) Vote.no

src/Ledger/Set/Theory.agda

@@ -42,7 +42,7 @@ abstract
     card-≡ᵉ (-, Theoryᶠ.DecEq⇒strongly-finite List-Modelᶠ (toSet X))
             (-, Theoryᶠ.DecEq⇒strongly-finite List-Modelᶠ (toSet Y)) X≡Y
 
-  lengthˢ-∅ : ∀ {A} ⦃ _ : DecEq A ⦄ → lengthˢ {A} ∅ ≡ 0
+  lengthˢ-∅ : ∀ {A} ⦃ _ : DecEq A ⦄ → lengthˢ {A} ⟦⟧ ≡ 0
   lengthˢ-∅ = refl
 
   setToList : {A : Set} → ℙ A → List A

src/Ledger/Utxo.lagda

@@ -109,7 +109,7 @@ module _ (let open Tx; open TxBody) where
   certDepositᵐ : PParams → DCert → DepositPurpose ⇀ Coin
   certDepositᵐ pp cert = case certDeposit pp cert of λ where
     (just (p , v))  → ❴ p , v ❵ᵐ
-    nothing         → ∅ᵐ
+    nothing         → ∅
 
   propDepositᵐ : PParams → GovActionID → GovProposal → DepositPurpose ⇀ Coin
   propDepositᵐ pp gaid record { returnAddr = record { stake = c } }
@@ -147,7 +147,7 @@ m ≤ᵇ n = ¿ m ≤ n ¿ᵇ
 _≥ᵇ_ = flip _≤ᵇ_
 
 ≟-∅ᵇ : {A : Set} ⦃ _ : DecEq A ⦄ → (X : ℙ A) → Bool
-≟-∅ᵇ X = ¿ X ≡ ∅ ¿ᵇ
+≟-∅ᵇ X = ¿ X ≡ ⟦⟧ ¿ᵇ
 \end{code}
 \begin{code}
 -- TODO: this could be a regular property
@@ -306,7 +306,7 @@ data _⊢_⇀⦇_,UTXO⦈_ where
         open UTxOEnv Γ renaming (pparams to pp)
         open UTxOState s
     in
-    ∙  txins ≢ ∅                              ∙ txins ⊆ dom utxo
+    ∙  txins ≢ ⟦⟧                              ∙ txins ⊆ dom utxo
     ∙  inInterval slot txvldt                 ∙ minfee pp tx ≤ txfee
     ∙  consumed pp s txb ≡ produced pp s txb  ∙ coin mint ≡ 0
     ∙  txsize ≤ maxTxSize pp