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 ++++++++++------
 Data/Hypergraph.agda       | 30 ++++++++++++++----------------
 Data/Hypergraph/Edge.agda  | 15 +++++++++++----
 Data/Hypergraph/Label.agda | 14 +++++++-------
 Data/System.agda           | 13 ++++++-------
 5 files changed, 48 insertions(+), 40 deletions(-)

(limited to 'Data')

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)
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index ff92d0e..770c500 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -1,18 +1,18 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; 0ℓ)
 open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Level using (Level; 0ℓ)
 
-module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
+module Data.Hypergraph {ℓ : Level} (HL : HypergraphLabel) where
 
 import Data.List.Relation.Binary.Pointwise as PW
 import Function.Reasoning as →-Reasoning
 import Relation.Binary.PropositionalEquality as ≡
-import Data.Hypergraph.Edge HL as Hyperedge
+import Data.Hypergraph.Edge {ℓ} HL as Hyperedge
 import Data.List.Relation.Binary.Permutation.Propositional as List-↭
+import Data.List.Relation.Binary.Permutation.Setoid as ↭
 
 open import Data.List using (List; map)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-refl; ↭-sym; ↭-trans)
 open import Data.Nat using (ℕ)
 open import Data.String using (String; unlines)
 open import Function using (_∘_; _⟶ₛ_; Func)
@@ -22,13 +22,15 @@ module Edge = Hyperedge
 open Edge using (Edge; Edgeₛ)
 
 -- A hypergraph is a list of edges
-record Hypergraph (v : ℕ) : Set c where
+record Hypergraph (v : ℕ) : Set ℓ where
   constructor mkHypergraph
   field
     edges : List (Edge v)
 
 module _ {v : ℕ} where
 
+  open ↭ (Edgeₛ v) using (_↭_; ↭-refl; ↭-sym; ↭-trans)
+
   show : Hypergraph v → String
   show (mkHypergraph e) = unlines (map Edge.show e)
 
@@ -55,7 +57,7 @@ module _ {v : ℕ} where
   ≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (↭-trans ≡n₁ ≡n₂)
 
 -- The setoid of labeled hypergraphs with v nodes
-Hypergraphₛ : ℕ → Setoid c ℓ
+Hypergraphₛ : ℕ → Setoid ℓ ℓ
 Hypergraphₛ v = record
     { Carrier = Hypergraph v
     ; _≈_ = _≈_
@@ -68,15 +70,11 @@ Hypergraphₛ v = record
 
 open Func
 
-List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ
-List∘Edgeₛ = PW.setoid ∘ Edgeₛ
+open ↭ using (↭-setoid)
+
+Multiset∘Edgeₛ : (n : ℕ) → Setoid ℓ ℓ
+Multiset∘Edgeₛ = ↭-setoid ∘ Edgeₛ
 
-mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n
+mkHypergraphₛ : {n : ℕ} → Multiset∘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
+mkHypergraphₛ {n} .cong = mk≈
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 1e24559..5c22a04 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -2,7 +2,8 @@
 
 open import Data.Hypergraph.Label using (HypergraphLabel)
 
-module Data.Hypergraph.Edge (HL : HypergraphLabel) where
+open import Level using (Level; 0ℓ)
+module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where
 
 import Data.Vec as Vec
 import Data.Vec.Relation.Binary.Equality.Cast as VecCast
@@ -15,13 +16,15 @@ open import Data.String using (String; _<+>_)
 open import Data.Vec.Show using () renaming (show to showVec)
 open import Level using (0ℓ)
 open import Relation.Binary using (Setoid; IsEquivalence)
+open import Function using (_⟶ₛ_; Func)
 
 module HL = HypergraphLabel HL
 
 open HL using (Label; cast; cast-is-id)
 open Vec using (Vec)
+open Func
 
-record Edge (v : ℕ) : Set where
+record Edge (v : ℕ) : Set ℓ where
   constructor mkEdge
   field
     {arity} : ℕ
@@ -42,7 +45,7 @@ open VecCast using (_≈[_]_)
 module _ {v : ℕ} where
 
   -- an equivalence relation on edges with v nodes
-  record _≈_ (E E′ : Edge v) : Set where
+  record _≈_ (E E′ : Edge v) : Set ℓ where
     constructor mk≈
     module E = Edge E
     module E′ = Edge E′
@@ -92,5 +95,9 @@ module _ {v : ℕ} where
     rewrite cast-is-id ≡.refl l
     rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
 
-Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
+Edgeₛ : (v : ℕ) → Setoid ℓ ℓ
 Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} }
+
+mapₛ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
+mapₛ f .to = map f
+mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (VecCast.≈-cong′ (Vec.map f) ≡p)
diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda
index c23d33a..ca95002 100644
--- a/Data/Hypergraph/Label.agda
+++ b/Data/Hypergraph/Label.agda
@@ -4,22 +4,22 @@ module Data.Hypergraph.Label where
 open import Data.Castable using (IsCastable)
 open import Data.Nat.Base using (ℕ)
 open import Data.String using (String)
-open import Level using (Level; suc)
+open import Level using (Level; 0ℓ)
 open import Relation.Binary using (Rel; IsDecTotalOrder)
 open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
 open import Relation.Binary.Properties.DecTotalOrder using (<-strictTotalOrder; _<_)
 open import Relation.Binary.PropositionalEquality using (_≡_)
 
-record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+record HypergraphLabel : Set₁ where
 
   field
-    Label : ℕ → Set ℓ
+    Label : ℕ → Set
     showLabel : (n : ℕ) → Label n → String
     isCastable : IsCastable Label
-    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+    _[_≤_] : (n : ℕ) → Rel (Label n) 0ℓ
     isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
 
-  decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+  decTotalOrder : (n : ℕ) → DecTotalOrder 0ℓ 0ℓ 0ℓ
   decTotalOrder n = record
       { Carrier = Label n
       ; _≈_ = _≡_
@@ -27,10 +27,10 @@ record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
       ; isDecTotalOrder = isDecTotalOrder n
       }
 
-  _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+  _[_<_] : (n : ℕ) → Rel (Label n) 0ℓ
   _[_<_] n =  _<_ (decTotalOrder n)
 
-  strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+  strictTotalOrder : (n : ℕ) → StrictTotalOrder 0ℓ 0ℓ 0ℓ
   strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
 
   open IsCastable isCastable public
diff --git a/Data/System.agda b/Data/System.agda
index 0361369..cecdfcd 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -1,7 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level)
-
+open import Level using (Level; 0ℓ; suc)
 module Data.System {ℓ : Level} where
 
 import Function.Construct.Identity as Id
@@ -11,7 +10,7 @@ open import Data.Circuit.Value using (Value)
 open import Data.Nat.Base using (ℕ)
 open import Data.Setoid using (_⇒ₛ_; ∣_∣)
 open import Data.System.Values Value using (Values; _≋_; module ≋)
-open import Level using (Level; _⊔_; 0ℓ; suc)
+open import Level using (Level; 0ℓ; suc)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid)
 open import Function.Base using (_∘_)
@@ -20,10 +19,10 @@ open import Function.Construct.Setoid using (_∙_)
 
 open Func
 
-record System (n : ℕ) : Set (suc ℓ) where
+record System (n : ℕ) : Set₁ where
 
   field
-    S : Setoid ℓ ℓ
+    S : Setoid 0ℓ 0ℓ
     fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
     fₒ : ∣ S ⇒ₛ Values n ∣
 
@@ -66,7 +65,7 @@ module _ {n : ℕ} where
   ≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s))
   ≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s))
 
-  System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
+  System-Preorder : Preorder (suc 0ℓ) (suc 0ℓ) ℓ
   System-Preorder = record
       { Carrier = System n
       ; _≈_ = _≡_
@@ -82,5 +81,5 @@ module _ (n : ℕ) where
 
   open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
 
-  Systemₛ : Setoid (suc ℓ) ℓ
+  Systemₛ : Setoid (suc 0ℓ) ℓ
   Systemₛ = InducedEquivalence
-- 
cgit v1.2.3