3 files changed, 36 insertions, 8 deletions
diff --git a/Data/Circuit.agda b/Data/Circuit.agda
index 0be86f9..09dfb2e 100644
--- a/Data/Circuit.agda
+++ b/Data/Circuit.agda
@@ -12,15 +12,16 @@ open import Data.Fin using (Fin)
 open import Data.Hypergraph {c} {ℓ} Gates
   using
     ( Hypergraph
-    ; mkHypergraph
     ; Hypergraphₛ
+    ; mkHypergraphₛ
+    ; List∘Edgeₛ
     ; module Edge
-    ; normalize
+    ; mkHypergraph
     ; _≈_
     ; mk≈
     )
 open import Data.Nat using (ℕ)
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary using (Setoid)
 open import Function.Bundles using (Func; _⟶ₛ_)
 
 open List using (List)
@@ -35,6 +36,9 @@ map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges)
 Circuitₛ : ℕ → Setoid c (c ⊔ ℓ)
 Circuitₛ = Hypergraphₛ
 
+mkCircuitₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Circuitₛ n
+mkCircuitₛ = mkHypergraphₛ
+
 open Func
 open Edge.Sort using (sort)
 
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index 2e8498c..18a259b 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -6,9 +6,32 @@ open import Data.Hypergraph.Label using (HypergraphLabel)
 
 module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
 
+import Data.List.Relation.Binary.Pointwise as PW
+import Data.Hypergraph.Edge HL as HypergraphEdge
+import Function.Reasoning as →-Reasoning
+import Relation.Binary.PropositionalEquality as ≡
+
 open import Data.Hypergraph.Base {c} HL public
 open import Data.Hypergraph.Setoid {c} {ℓ} HL public
-
-import Data.Hypergraph.Edge HL as HypergraphEdge
+open import Data.Nat using (ℕ)
+open import Function using (_∘_; _⟶ₛ_; Func)
+open import Level using (0ℓ)
+open import Relation.Binary using (Setoid)
 
 module Edge = HypergraphEdge
+
+open Edge using (Edgeₛ; ≈-Edge⇒≡)
+open Func
+
+List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ
+List∘Edgeₛ = PW.setoid ∘ Edgeₛ
+
+mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n
+mkHypergraphₛ .to = mkHypergraph
+mkHypergraphₛ {n} .cong ≋-edges = ≋-edges
+    |> PW.map ≈-Edge⇒≡
+    |> PW.Pointwise-≡⇒≡
+    |> ≡.cong mkHypergraph
+    |> Setoid.reflexive (Hypergraphₛ n)
+  where
+    open →-Reasoning
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} }