From 5f4d1cf740591476d3c7bc270fd11a2c578ab7e6 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Wed, 5 Nov 2025 08:11:48 -0600
Subject: Adjust universe levels

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

(limited to 'Data/Circuit.agda')

diff --git a/Data/Circuit.agda b/Data/Circuit.agda
index 46c4e18..77d6b72 100644
--- a/Data/Circuit.agda
+++ b/Data/Circuit.agda
@@ -2,20 +2,22 @@
 
 open import Level using (Level)
 
-module Data.Circuit {c ℓ : Level} where
+module Data.Circuit {ℓ : Level} where
 
 open import Data.Circuit.Gate using (Gates)
 
 import Data.List as List
-import Data.Hypergraph {c} {ℓ} Gates as Hypergraph
+import Data.Hypergraph {ℓ} Gates as Hypergraph
 
 open import Data.Fin using (Fin)
 open import Data.Nat using (ℕ)
-open import Function using (Func; _⟶ₛ_)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺)
+open import Function using (Func; _⟶ₛ_; _∘_)
+open import Relation.Binary using (Setoid)
 
 open Func
-open Hypergraph using (List∘Edgeₛ)
+
+open Hypergraph using (Multiset∘Edgeₛ)
 open Hypergraph
   using (_≈_ ; mk≈ ; module Edge)
   renaming
@@ -33,6 +35,8 @@ map f (mkCircuit edges) = mkCircuit (List.map (Edge.map f) edges)
 discrete : (n : ℕ) → Circuit n
 discrete n = mkCircuit []
 
+open Edge using (Edgeₛ)
+
 mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m
 mapₛ f .to = map f
-mapₛ f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edge.map f) x≈y)
+mapₛ {n} {m} f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edgeₛ n) (Edgeₛ m) (cong (Edge.mapₛ f)) x≈y)
-- 
cgit v1.2.3