From d2ce2675b5e0331b6bf5647a4fc195e458d9b5ee Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 30 Oct 2025 19:23:31 -0500
Subject: Add Circ functor

---
 Data/Circuit.agda | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'Data/Circuit.agda')

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)
 
-- 
cgit v1.2.3