------------------------------------------------------------------------
-- A trivial mode structure
------------------------------------------------------------------------

open import Graded.Modality

module Graded.Mode.Instances.Trivial
  {a} {M : Set a}
  (๐•„ : Modality M)
  where

open import Graded.Mode
open import Graded.Mode.Instances.Zero-one.Variant ๐•„
open import Graded.Mode.Instances.Zero-one ๐Ÿ˜แต-Not-Allowed

-- A trivial mode structure.

trivial : IsMode Mode ๐•„
trivial = Zero-one-isMode