diff options
Diffstat (limited to 'Data/Hypergraph/Label.agda')
| -rw-r--r-- | Data/Hypergraph/Label.agda | 14 |
1 files changed, 7 insertions, 7 deletions
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 |