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/Hypergraph.agda | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

(limited to 'Data/Hypergraph.agda')

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