Add Circ functormain

1 files changed, 4 insertions, 3 deletions

diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 7d0fa7c..ee32393 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -25,8 +25,7 @@ open import Data.String using (String; _<+>_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
 open import Data.Vec.Show using () renaming (show to showVec)
 open import Level using (0ℓ)
-open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
-open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary using (Setoid; DecTotalOrder; StrictTotalOrder; IsEquivalence)
 open import Relation.Nullary using (¬_)
 
 
@@ -89,7 +88,6 @@ record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
     module i≈j = ≈-Edge i≈j
     module j≈k = ≈-Edge j≈k
 
-open import Relation.Binary using (IsEquivalence)
 ≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v})
 ≈-Edge-IsEquivalence = record
     { refl = ≈-Edge-refl
@@ -345,3 +343,6 @@ open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) publ
 
 module Sort {v} = ListSort (decTotalOrder {v})
 open Sort using (sort) public
+
+Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
+Edgeₛ v = record { isEquivalence = ≈-Edge-IsEquivalence {v} }