open import Tools.Bool
open import Tools.Unit
module Graded.Modality.Instances.Unit where
open import Tools.Function
open import Tools.Level
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Sum
open import Tools.Algebra ⊤
open import Graded.Modality ⊤ public
open import Graded.Modality.Variant lzero
open import Graded.FullReduction.Assumptions
open import Definition.Typed.Restrictions ⊤
private variable
variant : Modality-variant
rs : Type-restrictions
_+_ : Op₂ ⊤
_ + _ = tt
infixr 20 _+_
_⊛_▷_ : Op₃ ⊤
_ ⊛ _ ▷ _ = tt
+-Commutative : Commutative _+_
+-Commutative x y = refl
+-Associative : Associative _+_
+-Associative x y z = refl
+-Distributiveˡ : _+_ DistributesOverˡ _+_
+-Distributiveˡ x y z = refl
+-Distributiveʳ : _+_ DistributesOverʳ _+_
+-Distributiveʳ x y z = refl
+-LeftIdentity : LeftIdentity tt _+_
+-LeftIdentity tt = refl
+-RightIdentity : RightIdentity tt _+_
+-RightIdentity tt = refl
+-Identity : Identity tt _+_
+-Identity = +-LeftIdentity , +-RightIdentity
+-Idempotent : Idempotent _+_
+-Idempotent tt = refl
+-Magma : IsMagma _+_
+-Magma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _+_
}
+-Semigroup : IsSemigroup _+_
+-Semigroup = record
{ isMagma = +-Magma
; assoc = +-Associative
}
+-Monoid : IsMonoid _+_ tt
+-Monoid = record
{ isSemigroup = +-Semigroup
; identity = +-Identity
}
+-CommutativeMonoid : IsCommutativeMonoid _+_ tt
+-CommutativeMonoid = record
{ isMonoid = +-Monoid
; comm = +-Commutative
}
+-Band : IsBand _+_
+-Band = record
{ isSemigroup = +-Semigroup
; idem = +-Idempotent
}
+-Semilattice : IsSemilattice _+_
+-Semilattice = record
{ isBand = +-Band
; comm = +-Commutative
}
+-+-SemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _+_ tt tt
+-+-SemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-CommutativeMonoid
; *-isMonoid = +-Monoid
; distrib = +-Distributiveˡ , +-Distributiveʳ
}
+-+-Semiring : IsSemiring _+_ _+_ tt tt
+-+-Semiring = record
{ isSemiringWithoutAnnihilatingZero = +-+-SemiringWithoutAnnihilatingZero
; zero = (λ x → refl) , (λ x → refl)
}
unit-semiring-with-meet : Semiring-with-meet
unit-semiring-with-meet = record
{ _+_ = _+_
; _·_ = _+_
; _∧_ = _+_
; 𝟘 = tt
; 𝟙 = tt
; +-·-Semiring = +-+-Semiring
; ∧-Semilattice = +-Semilattice
; ·-distrib-∧ = +-Distributiveˡ , +-Distributiveʳ
; +-distrib-∧ = +-Distributiveˡ , +-Distributiveʳ
}
unit-has-star : Has-star unit-semiring-with-meet
unit-has-star = record
{ _⊛_▷_ = _⊛_▷_
; ⊛-ineq = (λ p q r → refl) , (λ p q r → refl)
; +-sub-interchangeable-⊛ = λ r p q p′ q′ → refl
; ·-sub-distribʳ-⊛ = λ r q p p′ → refl
; ⊛-sub-distrib-∧ = λ r → (λ p q q′ → refl) , (λ q p p′ → refl)
}
UnitModality :
(variant : Modality-variant) →
let open Modality-variant variant in
¬ T 𝟘ᵐ-allowed →
Modality
UnitModality variant not-ok = record
{ variant = variant
; semiring-with-meet = unit-semiring-with-meet
; 𝟘-well-behaved = ⊥-elim ∘→ not-ok
; has-star = λ _ → unit-has-star
; +-decreasingˡ = ⊥-elim ∘→ not-ok
}
full-reduction-assumptions :
let open Modality-variant variant in
(ok : ¬ T 𝟘ᵐ-allowed) →
Full-reduction-assumptions (UnitModality variant ok) rs
full-reduction-assumptions _ = record
{ 𝟙≤𝟘 = λ _ → refl
; ≡𝟙⊎𝟙≤𝟘 = λ _ → inj₁ refl
}