------------------------------------------------------------------------
-- Instances related to the Has-omega property
------------------------------------------------------------------------

module Graded.Modality.Omega-instances {a} {M : Set a} where

open import Graded.Modality M

open Has-omega ⦃ … ⦄ public