open import Tools.Bool
open import Tools.Level
open import Tools.Nullary
open import Tools.Sum
open import Graded.Modality.Instances.Zero-one-many false as ππΟ
open import Graded.Modality.Variant lzero
module Graded.Modality.Instances.Linearity
(variant : Modality-variant)
(open Modality-variant variant)
(variant-ok : Β¬ β-available β Β¬ T πα΅-allowed)
where
open ππΟ renaming (Zero-one-many to Linearity) public
open import Graded.Modality Linearity
open import Graded.FullReduction.Assumptions
import Graded.Modality.Properties
open import Definition.Typed.Restrictions Linearity
open import Tools.Empty
open import Tools.Function
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Unit
private variable
rs : Type-restrictions
linearityModality : Modality
linearityModality = zero-one-many-greatest variant (flip variant-ok)
linearity-has-well-behaved-zero : Has-well-behaved-zero (Modality.semiring-with-meet linearityModality)
linearity-has-well-behaved-zero = zero-one-many-has-well-behaved-zero
open Graded.Modality.Properties linearityModality
Suitable-for-full-reduction :
Type-restrictions β Set
Suitable-for-full-reduction rs =
Β¬ Unit-allowed Γ
(β p β Β¬ Ξ£β-allowed π p) Γ
(β p β Β¬ Ξ£β-allowed Ο p)
where
open Type-restrictions rs
suitable-for-full-reduction :
Type-restrictions β β Suitable-for-full-reduction
suitable-for-full-reduction rs =
record rs
{ Unit-allowed = β₯
; Ξ Ξ£-allowed = Ξ» b p q β
Ξ Ξ£-allowed b p q Γ p β’ π Γ p β’ Ο
}
, idαΆ
, (Ξ» _ β (_$ refl) ββ projβ ββ projβ)
, (Ξ» _ β (_$ refl) ββ projβ ββ projβ)
where
open Type-restrictions rs
full-reduction-assumptions :
Suitable-for-full-reduction rs β
Full-reduction-assumptions linearityModality rs
full-reduction-assumptions (Β¬Unit , Β¬π , Β¬Ο) = record
{ πβ€π = β₯-elim ββ Β¬Unit
; β‘πβπβ€π = Ξ» where
{p = π} ok β β₯-elim (Β¬π _ ok)
{p = Ο} ok β β₯-elim (Β¬Ο _ ok)
{p = π} _ β injβ refl
}