-- Intuitionistic propositional calculus.
-- Kripke-style semantics with exploding abstract worlds.

module A201607.IPC.Semantics.KripkeExploding where

open import A201607.IPC.Syntax.Common public


-- Intuitionistic Kripke-CPS models, with exploding worlds.

record Model : Set₁ where
  infix 3 _⊪ᵅ_
  field
    World : Set

    -- Intuitionistic accessibility; preorder.
    _≤_    : World  World  Set
    refl≤  :  {w}  w  w
    trans≤ :  {w w′ w″}  w  w′  w′  w″  w  w″

    -- Strong forcing for atomic propositions; monotonic.
    _⊪ᵅ_   : World  Atom  Set
    mono⊪ᵅ :  {P w w′}  w  w′  w ⊪ᵅ P  w′ ⊪ᵅ P

    -- Exploding.
    _‼_ : World  Ty  Set

open Model {{…}} public


-- Strong forcing and forcing, in a particular world of a particular model.

module _ {{_ : Model}} where
  mutual
    infix 3 _⊪_
    _⊪_ : World  Ty  Set
    w  α P   = w ⊪ᵅ P
    w  A  B =  {w′}  w  w′  w′  A  w′  B
    w  A  B = w  A × w  B
    w      = 𝟙
    w      = 𝟘
    w  A  B = w  A  w  B

    infix 3 _⊩_
    _⊩_ : World  Ty  Set
    w  A =  {C} {w′ : World}  w  w′  (∀ {w″ : World}  w′  w″  w″  A  w″  C)  w′  C

  infix 3 _⊩⋆_
  _⊩⋆_ : World  Cx Ty  Set
  w ⊩⋆      = 𝟙
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w  A


-- Monotonicity with respect to intuitionistic accessibility.

module _ {{_ : Model}} where
  mutual
    mono⊪ :  {A} {w w′ : World}  w  w′  w  A  w′  A
    mono⊪ {α P}   ξ s       = mono⊪ᵅ ξ s
    mono⊪ {A  B} ξ f       = λ ξ′ a  f (trans≤ ξ ξ′) a
    mono⊪ {A  B} ξ (a , b) = mono⊩ {A} ξ a , mono⊩ {B} ξ b
    mono⊪ {}    ξ        = 
    mono⊪ {}    ξ ()
    mono⊪ {A  B} ξ (ι₁ a)  = ι₁ (mono⊩ {A} ξ a)
    mono⊪ {A  B} ξ (ι₂ b)  = ι₂ (mono⊩ {B} ξ b)

    mono⊩ :  {A} {w w′ : World}  w  w′  w  A  w′  A
    mono⊩ ξ a = λ ξ′ k′  a (trans≤ ξ ξ′) k′

  mono⊩⋆ :  {Ξ} {w w′ : World}  w  w′  w ⊩⋆ Ξ  w′ ⊩⋆ Ξ
  mono⊩⋆ {}     ξ        = 
  mono⊩⋆ {Ξ , A} ξ (γ , a) = mono⊩⋆ {Ξ} ξ γ , mono⊩ {A} ξ a


-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ :  {A B} {w : World}  w  A  B  w  A  w  B
  s ⟪$⟫ a = s refl≤ a

  return :  {A} {w : World}  w  A  w  A
  return {A} a = λ ξ k  k refl≤ (mono⊪ {A} ξ a)

  bind :  {A B} {w : World}  w  A  (∀ {w′ : World}  w  w′  w′  A  w′  B)  w  B
  bind a k = λ ξ k′  a ξ  ξ′ a′  k (trans≤ ξ ξ′) a′ refl≤  ξ″ a″  k′ (trans≤ ξ′ ξ″) a″))


-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : World  Cx Ty  Ty  Set
  w  Γ  A = w ⊩⋆ Γ  w  A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : World  Cx Ty  Cx Ty  Set
  w  Γ ⇒⋆ Ξ = w ⊩⋆ Γ  w ⊩⋆ Ξ


-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty  Ty  Set₁
Γ  A =  {{_ : Model}} {w : World}  w  Γ  A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty  Cx Ty  Set₁
Γ ⊨⋆ Ξ =  {{_ : Model}} {w : World}  w  Γ ⇒⋆ Ξ


-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup :  {A Γ} {w : World}  A  Γ  w  Γ  A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ