open import Tools.Level
module Graded.Modality.Variant (a : Level) where
open import Tools.Bool
open import Tools.Empty
open import Tools.Level
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Unit
record Modality-variant : Set (lsuc a) where
field
๐แต-allowed : Bool
โ-available : Set a
โ-available-propositional : (p q : โ-available) โ p โก q
โ-available-decided : Dec โ-available
โ-available-and-๐แต-available-if : Bool โ Modality-variant
โ-available-and-๐แต-available-if ok = record
{ ๐แต-allowed = ok
; โ-available = Lift _ โค
; โ-available-propositional = ฮป _ _ โ refl
; โ-available-decided = yes _
}
โ-not-available-and-๐แต-available-if : Bool โ Modality-variant
โ-not-available-and-๐แต-available-if ok = record
{ ๐แต-allowed = ok
; โ-available = Lift _ โฅ
; โ-available-propositional = ฮป ()
; โ-available-decided = no (ฮป ())
}