open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Empty
open import Cubical.Data.Unit

module Semantics.Concrete where

ABS = ⊥
ABS-isProp = isProp⊥

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

◯-semantics : ∀ {X} → ◯ X ≃ Unit
◯-semantics {X} = isContr→≃Unit isContrΠ⊥

●-semantics : ∀ {X} → ● X ≃ X
●-semantics {X} = isoToEquiv (iso (λ { (η• x) → x }) η• (λ x → refl) (λ { (η• x) → refl }))