open import Agda.Primitive using (lzero)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Unit


module Modality.Concrete (ABS : Type) (ABS-isProp : isProp ABS) where

data ● (X : Type) : Type where
  η• : (x : X) → ● X
  ∗ : (abs : ABS) → ● X
  law : (x : X) (abs : ABS) → η• x ≡ ∗ abs

◯●-isContr : ∀ {X} (abs : ABS) → isContr (● X)
◯●-isContr abs .fst = ∗ abs
◯●-isContr abs .snd (η• x) = sym (law x abs)
◯●-isContr abs .snd (∗ abs') = cong ∗ (ABS-isProp abs abs')
◯●-isContr abs .snd (law x abs' i) j =
  hcomp (λ k → λ
    { (j = i0) → law x abs (i ∨ k)
    ; (j = i1) → law x abs' i
    ; (i = i0) → law x abs (k ∧ ~ j)
    ; (i = i1) → ∗ (ABS-isProp abs abs' j)
    })
  (law x (ABS-isProp abs abs' j) i)
-- https://q.uiver.app/#q=WzAsMTQsWzAsMF0sWzksM10sWzgsMiwiXFxldGEoeCkiXSxbMTEsMiwiXFxhc3QgYWJzJyJdLFs4LDUsIlxcZXRhKHgpIl0sWzExLDUsIlxcYXN0IGFicyJdLFsxMCwxLCJcXGV0YSh4KSJdLFsxMywxLCJcXGFzdCBhYnMnIl0sWzEwLDQsIlxcYXN0IGFicyJdLFsxMyw0LCJcXGFzdCBhYnMiXSxbNCwzLCJcXGJ1bGxldCJdLFs1LDMsIlxcYnVsbGV0Il0sWzQsMiwiXFxidWxsZXQiXSxbNSwyLCJcXGJ1bGxldCJdLFsyLDMsImxhdyh4KShhYnMnKSIsMV0sWzQsMl0sWzUsM10sWzQsNSwibGF3KHgpKGFicykiLDFdLFsyLDZdLFszLDddLFs0LDhdLFs1LDldLFs2LDcsImxhdyh4KShhYnMnKSIsMSx7ImNvbG91ciI6WzAsNjAsNjBdfSxbMCw2MCw2MCwxXV0sWzgsOSwiIiwxLHsiY29sb3VyIjpbMCw2MCw2MF19XSxbOCw2LCIiLDEseyJjb2xvdXIiOlswLDYwLDYwXX1dLFs5LDcsIiIsMSx7ImNvbG91ciI6WzAsNjAsNjBdfV0sWzEwLDExLCJpIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZG90dGVkIn19fV0sWzEwLDEyLCJqIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZG90dGVkIn19fV0sWzEwLDEzLCJrIiwxLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZG90dGVkIn19fV1d

●-ind : {X : Type} (R : ● X → Type)
  → (η•-case : (x : X) → R (η• x))
  → (∗-case : (abs : ABS) → R (∗ abs))
  → (law-case : (x : X) (abs : ABS) → PathP (λ i → R (law x abs i)) (η•-case x) (∗-case abs))
  → (x• : ● X) → R x•
●-ind R η•-case ∗-case law-case (η• x) = η•-case x
●-ind R η•-case ∗-case law-case (∗ abs) = ∗-case abs
●-ind R η•-case ∗-case law-case (law x abs i) = law-case x abs i

◯●-indP : ∀ {X} {R : ● X → Type}
  → (η•-case : (x : X) → R (η• x))
  → (∗-case : (abs : ABS) → R (∗ abs))
  → (law-case : (x : X) (abs : ABS) → PathP (λ i → R (law x abs i)) (η•-case x) (∗-case abs))
  → (x• : ● X) (abs : ABS) →
      PathP (λ i → R (◯●-isContr abs .snd x• (~ i)))
        (●-ind R η•-case ∗-case law-case x•) (∗-case abs)
◯●-indP {R = R} η•-case ∗-case law-case x• abs =
  cong (●-ind R η•-case ∗-case law-case) (sym (◯●-isContr abs .snd x•))

●-map : {X Y : Type} → (X → Y) → ● X → ● Y
●-map f (η• x) = η• (f x)
●-map f (∗ abs) = ∗ abs
●-map f (law x abs i) = law (f x) abs i

●-map-∘ : {X Y Z : Type} {f : X → Y} {g : Y → Z} → ●-map g ∘ ●-map f ≡ ●-map (g ∘ f)
●-map-∘ {f = f} {g} _ (η• x) = η• (g (f x))
●-map-∘ {f = f} {g} _ (∗ abs) = ∗ abs
●-map-∘ {f = f} {g} _ (law x abs j) = law (g (f x)) abs j

●-lex : ∀ {X} {x x' : X} → η• x ≡ η• x' → ● (x ≡ x')
●-lex {X} {x} h = subst encode h (η• refl)
  where
    encode : ● X → Type
    encode (η• x') = ● (x ≡ x')
    encode (∗ abs) = Unit
    encode (law x' abs i) = isContr→≡Unit (◯●-isContr {x ≡ x'} abs) i