open import Cubical.Foundations.Equiv
open import Cubical.Data.Unit

module Semantics.Abstract where

ABS = Unit
ABS-isProp = isPropUnit

open import Modality.Abstract ABS ABS-isProp
open import Modality.Concrete ABS ABS-isProp

◯-semantics : ∀ {X} → ◯ X ≃ X
◯-semantics {X} = ΠUnit λ _ → X

●-semantics : ∀ {X} → ● X ≃ Unit
●-semantics = isContr→≃Unit (◯●-isContr tt)