aboutsummaryrefslogtreecommitdiff
path: root/Data/Hypergraph/Label.agda
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