open import Agda.Primitive using (lzero)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma


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

◯ : Type → Type
◯ X = (abs : ABS) → X

◯∙ : (ABS → Type) → Type
◯∙ X = (abs : ABS) → X abs

η∘ : {X : Type} → X → ◯ X
η∘ x abs = x

◯-map : {X Y : Type} → (X → Y) → ◯ X → ◯ Y
◯-map f x∘ abs = f (x∘ abs)

η∘-isNatural : {X Y : Type} (f : X → Y) → η∘ ∘ f ≡ ◯-map f ∘ η∘
η∘-isNatural f = funExt λ x → refl

◯-preserve-× : {X Y : Type} → ◯ (X × Y) ≃ ◯ X × ◯ Y
◯-preserve-× {X} {Y} = isoToEquiv lemma
  where
    lemma : Iso (◯ (X × Y)) (◯ X × ◯ Y)
    lemma .Iso.fun [x,y]∘ = (λ abs → [x,y]∘ abs .fst) , (λ abs → [x,y]∘ abs .snd)
    lemma .Iso.inv (x∘ , y∘) = λ abs → x∘ abs , y∘ abs
    lemma .Iso.rightInv (x∘ , y∘) = refl
    lemma .Iso.leftInv [x,y]∘ = funExt λ abs → refl

○Σ≃○Σ○ : ∀ {X Y} → ◯ (Σ X Y) ≃ ◯ (Σ X (◯ ∘ Y))
○Σ≃○Σ○ {X} {Y} = isoToEquiv isoΣ◯
  where
    isoΣ◯ : Iso (◯ (Σ X Y)) (◯ (Σ X (◯ ∘ Y)))
    isoΣ◯ .Iso.fun x,y abs = map-snd η∘ (x,y abs)
    isoΣ◯ .Iso.inv x,y∘ abs = map-snd (_$ abs) (x,y∘ abs)
    isoΣ◯ .Iso.rightInv x,y∘ = funExt λ abs i → x,y∘ abs .fst , λ abs' → x,y∘ abs .snd (ABS-isProp abs abs' i)
    isoΣ◯ .Iso.leftInv x,y = refl

◯-X≃◯X : ∀ {X} → ABS → ◯ X ≃ X
◯-X≃◯X {X} abs = isoToEquiv iso◯
  where
    iso◯ : Iso (◯ X) X
    iso◯ .Iso.fun y = y abs
    iso◯ .Iso.inv = η∘
    iso◯ .Iso.rightInv a = refl
    iso◯ .Iso.leftInv y i abs' = y (ABS-isProp abs abs' i)

isConcrete : Type → Type
isConcrete X = isContr (◯ X)

concrete→◯contr : ∀ {X} → isConcrete X → ◯ (isContr X)
concrete→◯contr is-concrete abs = subst isContr (ua (◯-X≃◯X abs)) is-concrete

◯contr→concrete : ∀ {X} → ◯ (isContr X) → isConcrete X
◯contr→concrete ◯is-contr .fst abs = ◯is-contr abs .fst
◯contr→concrete ◯is-contr .snd x∘ = funExt λ abs → ◯is-contr abs .snd (x∘ abs)

isConcrete× : ∀ {X₁ X₂} → isConcrete X₁ → isConcrete X₂ → isConcrete (X₁ × X₂)
isConcrete× {X₁} {X₂} is-concrete₁ is-concrete₂ =
  subst isContr (sym (ua ◯-preserve-×)) (isContrΣ is-concrete₁ (const is-concrete₂))

spec : {X : Type} (x₀ : X) → Type
spec {X} x₀ = Σ[ x ∈ X ] ◯ (x ≡ x₀)

isConcreteSpec : {X : Type} (x₀ : X) → isConcrete (spec x₀)
isConcreteSpec x₀ =
  subst isContr (ua ○Σ≃○Σ○) $
  isContrΠ λ _ →
  subst isContr (Σ-cong-snd λ _ → ua (isoToEquiv symIso)) $
  (isContrSingl x₀)

noninterference : ∀ {X Y} → isConcrete X → ◯ (((x : X) → Y x) ≃ Σ X Y)
noninterference {X} {Y} is-concrete abs =
  let is-contr = concrete→◯contr is-concrete abs in
    ((x : X) → Y x)
  ≃⟨ Π-contractDom is-contr ⟩
    Y (is-contr .fst)
  ≃⟨ invEquiv (Σ-contractFst is-contr) ⟩
    (Σ X Y)
  ■

modularity : ∀ {X Y} → isConcrete X → (f : X → Y) → (x x' : X) → ◯ (f x ≡ f x')
modularity {X} {Y} is-concrete f x x' abs =
  transport
    (sym $ ua $
      noninterference
        {Y = λ (x , x') → f x ≡ f x'}
        (isConcrete× is-concrete is-concrete)
        abs
    )
    ((x , x) , refl)
    (x , x')