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/Hypergraph/Edge.agda  | 15 +++++++++++----
 Data/Hypergraph/Label.agda | 14 +++++++-------
 2 files changed, 18 insertions(+), 11 deletions(-)

(limited to 'Data/Hypergraph')

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