Review

IntersectMBO · Mar 22, 2023 · c1b932c · c1b932c
1 parent f269d7a
commit c1b932c
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 5 deletions.
diff --git a/src/Axiom/Set.agda b/src/Axiom/Set.agda
@@ -198,7 +198,7 @@ record Theory {ℓ} : Type (sucˡ ℓ) where
       from' (x , x∈X , refl) | just x₁ | [ eq ] = to ∈-unions
         ( maybe ❴_❵ ∅ (f x)
         , to ∈-map (x , refl , x∈X)
-        , subst (λ z → x₁ ∈ maybe ❴_❵ ∅ z) (sym eq) (from ∈-singleton refl))
+        , subst (λ z → x₁ ∈ maybe ❴_❵ ∅ z) (sym eq) (to ∈-singleton refl))
 
   binary-unions : ∃[ Y ] ∀ {a} → (a ∈ X ⊎ a ∈ X') ⇔ a ∈ Y
   binary-unions {X = X} {X'} with unions (fromList (X ∷ [ X' ]))

diff --git a/src/Axiom/Set/Map/Dec.agda b/src/Axiom/Set/Map/Dec.agda
@@ -3,7 +3,7 @@ open import Axiom.Set
 
 module Axiom.Set.Map.Dec (thᵈ : Theoryᵈ) where
 
-open import Algebra.Bundles
+open import Algebra
 open import Agda.Primitive renaming (Set to Type)
 open import Data.These
 open import Interface.DecEq

diff --git a/src/Ledger/Deleg.lagda b/src/Ledger/Deleg.lagda
@@ -5,15 +5,17 @@
 
 open import Ledger.Prelude
 open import Ledger.Epoch
+open import Ledger.Crypto
 
 module Ledger.Deleg
-  (Network KeyHash ScriptHash : Set)
+  (crypto : Crypto)
+  (Network : Set)
   (epochStructure : EpochStructure)
   ⦃ _ : DecEq Network ⦄
-  ⦃ _ : DecEq KeyHash ⦄
-  ⦃ _ : DecEq ScriptHash ⦄
   where
 
+open Crypto crypto
+
 open import Agda.Primitive renaming (Set to Type)
 
 open import Ledger.Address Network KeyHash ScriptHash