blob: c23d33aa7219a94b2d5f9ca36339e824c8dc051c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
{-# OPTIONS --without-K --safe #-}
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 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
field
Label : ℕ → Set ℓ
showLabel : (n : ℕ) → Label n → String
isCastable : IsCastable Label
_[_≤_] : (n : ℕ) → Rel (Label n) ℓ
isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
decTotalOrder n = record
{ Carrier = Label n
; _≈_ = _≡_
; _≤_ = n [_≤_]
; isDecTotalOrder = isDecTotalOrder n
}
_[_<_] : (n : ℕ) → Rel (Label n) ℓ
_[_<_] n = _<_ (decTotalOrder n)
strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
open IsCastable isCastable public
|
