module Graded.Modality.Instances.Erasure.Modality where
open import Tools.Level
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum
open import Graded.Modality.Instances.Erasure
open import Graded.Modality.Variant lzero
open import Graded.Modality Erasure public
erasure-semiring-with-meet : Semiring-with-meet
erasure-semiring-with-meet = record
{ _+_ = _+_
; _·_ = _·_
; _∧_ = _∧_
; 𝟘 = 𝟘
; 𝟙 = ω
; +-·-Semiring = +-·-Semiring
; ∧-Semilattice = +-Semilattice
; ·-distrib-∧ = ·-distrib-+
; +-distrib-∧ = +-distrib-+
}
erasure-has-well-behaved-zero : Has-well-behaved-zero erasure-semiring-with-meet
erasure-has-well-behaved-zero = record
{ 𝟙≢𝟘 = λ ()
; is-𝟘? = λ where
𝟘 → yes refl
ω → no (λ ())
; zero-product = λ where
{p = 𝟘} {q = 𝟘} _ → inj₁ refl
{p = 𝟘} {q = ω} _ → inj₁ refl
{p = ω} {q = 𝟘} _ → inj₂ refl
{p = ω} {q = ω} ()
; +-positiveˡ = λ where
{p = 𝟘} _ → refl
{p = ω} {q = 𝟘} ()
{p = ω} {q = ω} ()
; ∧-positiveˡ = λ where
{p = 𝟘} _ → refl
{p = ω} ()
}
instance
erasure-has-star : Has-star erasure-semiring-with-meet
erasure-has-star = record
{ _⊛_▷_ = _⊛_▷_
; ⊛-ineq = ⊛-ineq₁ , ⊛-ineq₂
; +-sub-interchangeable-⊛ = +-sub-interchangeable-⊛
; ·-sub-distribʳ-⊛ = ·-sub-distribʳ-⊛
; ⊛-sub-distrib-∧ = λ r → ⊛-sub-distribˡ-∧ r , ⊛-sub-distribʳ-∧ r
}
ErasureModality : Modality-variant → Modality
ErasureModality variant = record
{ variant = variant
; semiring-with-meet = erasure-semiring-with-meet
; has-star = λ _ → erasure-has-star
; 𝟘-well-behaved = λ _ → erasure-has-well-behaved-zero
; +-decreasingˡ = λ _ _ → +-decreasingˡ
}