------------------------------------------------------------------------ -- An instance related to Dedicated-star ------------------------------------------------------------------------ import Graded.Modality module Graded.Modality.Dedicated-star.Instance {a} {M : Set a} (open Graded.Modality M) {𝕄 : Modality} where open Modality 𝕄 open import Graded.Modality.Dedicated-star 𝕄 instance -- If the modality is supposed to come with a dedicated -- natrec-star operator, then such an operator is available. has-dedicated-star : ⦃ star : Dedicated-star ⦄ → Has-star semiring-with-meet has-dedicated-star ⦃ star = dedicated-star star ⦄ = has-star star