From 5f4d1cf740591476d3c7bc270fd11a2c578ab7e6 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 5 Nov 2025 08:11:48 -0600 Subject: Adjust universe levels --- Data/Hypergraph/Label.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'Data/Hypergraph/Label.agda') 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