LP.agda

module LP where

open import Data.Empty using () renaming (⊥ to Empty)
open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
open import Data.Unit using () renaming (⊤ to Unit ; tt to unit)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)


data Cx (X : Set) : Set where
  ∅   : Cx X
  _,_ : Cx X → X → Cx X


data Var (X : Set) : Cx X → X → Set where
  top : ∀ {Γ A} → Var X (Γ , A) A
  pop : ∀ {Γ A B} → Var X Γ A → Var X (Γ , B) A


x₀ : ∀ {X Γ A} → Var X (Γ , A) A
x₀ = top

x₁ : ∀ {X Γ A B} → Var X ((Γ , A) , B) A
x₁ = pop x₀

x₂ : ∀ {X Γ A B C} → Var X (((Γ , A) , B) , C) A
x₂ = pop x₁


module S4 where
  data Ty : Set where
    ⊥  : Ty
    _⊃_ : Ty → Ty → Ty
    _∧_ : Ty → Ty → Ty
    □_  : Ty → Ty

  data Tm (Γ Δ : Cx Ty) : Ty → Set where
    var  : ∀ {A} → Var Ty Γ A → Tm Γ Δ A
    lam  : ∀ {A B} → Tm (Γ , A) Δ B → Tm Γ Δ (A ⊃ B)
    app  : ∀ {A B} → Tm Γ Δ (A ⊃ B) → Tm Γ Δ A → Tm Γ Δ B
    *var : ∀ {A} → Var Ty Δ A → Tm Γ Δ A
    up   : ∀ {A} → Tm ∅ Δ A → Tm Γ Δ (□ A)
    down : ∀ {A C} → Tm Γ Δ (□ A) → Tm Γ (Δ , A) C → Tm Γ Δ C
    pair : ∀ {A B} → Tm Γ Δ A → Tm Γ Δ B → Tm Γ Δ (A ∧ B)
    fst  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ A
    snd  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ B

  infixr 5 _⊃_
  infixl 10 _∧_

  v₀ : ∀ {Γ Δ A} → Tm (Γ , A) Δ A
  v₀ = var x₀

  v₁ : ∀ {Γ Δ A B} → Tm ((Γ , A) , B) Δ A
  v₁ = var x₁

  v₂ : ∀ {Γ Δ A B C} → Tm (((Γ , A) , B) , C) Δ A
  v₂ = var x₂

  *v₀ : ∀ {Γ Δ A} → Tm Γ (Δ , A) A
  *v₀ = *var x₀

  *v₁ : ∀ {Γ Δ A B} → Tm Γ ((Δ , A) , B) A
  *v₁ = *var x₁

  *v₂ : ∀ {Γ Δ A B C} → Tm Γ (((Δ , A) , B) , C) A
  *v₂ = *var x₂

  module Examples where
    I : ∀ {Γ Δ A} → Tm Γ Δ (A ⊃ A)
    I = lam v₀

    K : ∀ {Γ Δ A B} → Tm Γ Δ (A ⊃ B ⊃ A)
    K = lam (lam v₁)

    S : ∀ {Γ Δ A B C} → Tm Γ Δ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
    S = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

    D : ∀ {Γ Δ A B} → Tm Γ Δ (□ (A ⊃ B) ⊃ □ A ⊃ □ B)
    D = lam (lam (down v₁ (down v₀ (up (app *v₁ *v₀)))))

    T : ∀ {Γ Δ A} → Tm Γ Δ (□ A ⊃ A)
    T = lam (down v₀ *v₀)

    #4 : ∀ {Γ Δ A} → Tm Γ Δ (□ A ⊃ □ □ A)
    #4 = lam (down v₀ (up (up *v₀)))

    E1 : ∀ {Γ Δ A} → Tm Γ Δ (□ (□ A ⊃ A))
    E1 = up T

    E2 : ∀ {Γ Δ A} → Tm Γ Δ (□ (□ A ⊃ □ □ A))
    E2 = up #4

    E3 : ∀ {Γ Δ A B} → Tm Γ Δ (□ □ (A ⊃ B ⊃ A ∧ B))
    E3 = up (up (lam (lam (pair v₁ v₀))))

    E4 : ∀ {Γ Δ A B} → Tm Γ Δ (□ (□ A ⊃ □ B ⊃ □ □ (A ∧ B)))
    E4 = up (lam (lam (down v₁ (down v₀ (up (up (pair *v₁ *v₀)))))))


mutual
  data Ty : Set where
    ⊥  : Ty
    _⊃_ : Ty → Ty → Ty
    _∧_ : Ty → Ty → Ty
    _∴_ : ∀ {Ξ A} → Tm ∅ Ξ A → Ty → Ty

  data Tm (Γ Δ : Cx Ty) : Ty → Set where
    var  : ∀ {A} → Var Ty Γ A → Tm Γ Δ A
    lam  : ∀ {A B} → Tm (Γ , A) Δ B → Tm Γ Δ (A ⊃ B)
    app  : ∀ {A B} → Tm Γ Δ (A ⊃ B) → Tm Γ Δ A → Tm Γ Δ B
    *var : ∀ {A} → Var Ty Δ A → Tm Γ Δ A
    up   : ∀ {A} → (t : Tm ∅ Δ A) → Tm Γ Δ (t ∴ A)
    down : ∀ {Ξ A C} {t : Tm ∅ Ξ A} → Tm Γ Δ (t ∴ A) → Tm Γ (Δ , A) C → Tm Γ Δ C
    pair : ∀ {A B} → Tm Γ Δ A → Tm Γ Δ B → Tm Γ Δ (A ∧ B)
    fst  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ A
    snd  : ∀ {A B} → Tm Γ Δ (A ∧ B) → Tm Γ Δ B


syntax lam t      = ƛ t
syntax app t₁ t₂  = t₁ ∙ t₂
syntax up t       = ⇑ t
syntax down t₁ t₂ = ⇓⟨ t₁ ∣ t₂ ⟩
syntax pair t₁ t₂ = p⟨ t₁ , t₂ ⟩
syntax fst t      = π₀ t
syntax snd t      = π₁ t

infixr 5 _⊃_
infixl 10 _∧_
infixl 10 app
infixr 15 _∴_


v₀ : ∀ {Γ Δ A} → Tm (Γ , A) Δ A
v₀ = var x₀

v₁ : ∀ {Γ Δ A B} → Tm ((Γ , A) , B) Δ A
v₁ = var x₁

v₂ : ∀ {Γ Δ A B C} → Tm (((Γ , A) , B) , C) Δ A
v₂ = var x₂

*v₀ : ∀ {Γ Δ A} → Tm Γ (Δ , A) A
*v₀ = *var x₀

*v₁ : ∀ {Γ Δ A B} → Tm Γ ((Δ , A) , B) A
*v₁ = *var x₁

*v₂ : ∀ {Γ Δ A B C} → Tm Γ (((Δ , A) , B) , C) A
*v₂ = *var x₂

[vᵢ]_ : Ty → Ty
[vᵢ] A = _∴_ {Ξ = (∅ , A)} *v₀ A


module Examples where
  I : ∀ {Γ Δ A} → Tm Γ Δ (A ⊃ A)
  I = lam v₀

  K : ∀ {Γ Δ A B} → Tm Γ Δ (A ⊃ B ⊃ A)
  K = lam (lam v₁)

  S : ∀ {Γ Δ A B C} → Tm Γ Δ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
  S = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

  D : ∀ {Γ Δ A B} → Tm Γ Δ ([vᵢ] (A ⊃ B) ⊃ [vᵢ] A ⊃ app *v₁ *v₀ ∴ B)
  D = lam (lam (down v₁ (down v₀ (up (app *v₁ *v₀)))))

  T : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ A)
  T = lam (down v₀ *v₀)

  #4 : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ up *v₀ ∴ *v₀ ∴ A)
  #4 = lam (down v₀ (up (up *v₀)))

  E1 : ∀ {Γ Δ A} → Tm Γ Δ (T ∴ ([vᵢ] A ⊃ A))
  E1 = up T

  E2 : ∀ {Γ Δ A} → Tm Γ Δ (#4 ∴ ([vᵢ] A ⊃ up *v₀ ∴ *v₀ ∴ A))
  E2 = up #4

  E3 : ∀ {Γ Δ A B} →
       Tm Γ Δ (up (lam (lam (pair v₁ v₀))) ∴ lam (lam (pair v₁ v₀)) ∴ (A ⊃ B ⊃ A ∧ B))
  E3 = up (up (lam (lam (pair v₁ v₀))))

  E4 : ∀ {Γ Δ A B} →
       Tm Γ Δ (lam (lam (down v₁ (down v₀ (up (up (pair *v₁ *v₀)))))) ∴
              ([vᵢ] A ⊃ [vᵢ] B ⊃ up (pair *v₁ *v₀) ∴ pair *v₁ *v₀ ∴ (A ∧ B)))
  E4 = up (lam (lam (down v₁ (down v₀ (up (up (pair *v₁ *v₀)))))))


module AltArtemovNotation where
  I : ∀ {Γ Δ A} → Tm Γ Δ (A ⊃ A)
  I = ƛ v₀

  K : ∀ {Γ Δ A B} → Tm Γ Δ (A ⊃ B ⊃ A)
  K = ƛ ƛ v₁

  S : ∀ {Γ Δ A B C} → Tm Γ Δ ((A ⊃ B ⊃ C) ⊃ (A ⊃ B) ⊃ A ⊃ C)
  S = ƛ ƛ ƛ ((v₂ ∙ v₀) ∙ (v₁ ∙ v₀))

  D : ∀ {Γ Δ A B} → Tm Γ Δ ([vᵢ] (A ⊃ B) ⊃ [vᵢ] A ⊃ (*v₁ ∙ *v₀) ∴ B)
  D = ƛ ƛ ⇓⟨ v₁ ∣ ⇓⟨ v₀ ∣ ⇑ (*v₁ ∙ *v₀) ⟩ ⟩

  T : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ A)
  T = ƛ ⇓⟨ v₀ ∣ *v₀ ⟩

  #4 : ∀ {Γ Δ A} → Tm Γ Δ ([vᵢ] A ⊃ ⇑ *v₀ ∴ *v₀ ∴ A)
  #4 = ƛ ⇓⟨ v₀ ∣ ⇑ ⇑ *v₀ ⟩

  E1 : ∀ {Γ Δ A} → Tm Γ Δ (T ∴ ([vᵢ] A ⊃ A))
  E1 = ⇑ T

  E2 : ∀ {Γ Δ A} → Tm Γ Δ (#4 ∴ ([vᵢ] A ⊃ ⇑ *v₀ ∴ *v₀ ∴ A))
  E2 = ⇑ #4

  E3 : ∀ {Γ Δ A B} →
       Tm Γ Δ (⇑ ƛ ƛ p⟨ v₁ , v₀ ⟩ ∴ ƛ ƛ p⟨ v₁ , v₀ ⟩ ∴ (A ⊃ B ⊃ A ∧ B))
  E3 = ⇑ ⇑ ƛ ƛ p⟨ v₁ , v₀ ⟩

  E4 : ∀ {Γ Δ A B} →
       Tm Γ Δ (ƛ ƛ ⇓⟨ v₁ ∣ ⇓⟨ v₀ ∣ ⇑ ⇑ p⟨ *v₁ , *v₀ ⟩ ⟩ ⟩ ∴
              ([vᵢ] A ⊃ [vᵢ] B ⊃ ⇑ p⟨ *v₁ , *v₀ ⟩ ∴ p⟨ *v₁ , *v₀ ⟩ ∴ (A ∧ B)))
  E4 = ⇑ ƛ ƛ ⇓⟨ v₁ ∣ ⇓⟨ v₀ ∣ ⇑ ⇑ p⟨ *v₁ , *v₀ ⟩ ⟩ ⟩


module ForgetfulProjection where
  ⌊_⌋ᴬ : Ty → S4.Ty
  ⌊ ⊥ ⌋ᴬ    = S4.⊥
  ⌊ A ⊃ B ⌋ᴬ = ⌊ A ⌋ᴬ S4.⊃ ⌊ B ⌋ᴬ
  ⌊ A ∧ B ⌋ᴬ = ⌊ A ⌋ᴬ S4.∧ ⌊ B ⌋ᴬ
  ⌊ t ∴ A ⌋ᴬ = S4.□ ⌊ A ⌋ᴬ

  ⌊_⌋ᴳ : Cx Ty → Cx S4.Ty
  ⌊ ∅ ⌋ᴳ       = ∅
  ⌊ (Γ , A) ⌋ᴳ = (⌊ Γ ⌋ᴳ , ⌊ A ⌋ᴬ)

  ⌊_⌋ˣ : ∀ {Γ A} → Var Ty Γ A → Var S4.Ty ⌊ Γ ⌋ᴳ ⌊ A ⌋ᴬ
  ⌊ top ⌋ˣ   = top
  ⌊ pop x ⌋ˣ = pop ⌊ x ⌋ˣ

  ⌊_⌋ : ∀ {Γ Δ A} → Tm Γ Δ A → S4.Tm ⌊ Γ ⌋ᴳ ⌊ Δ ⌋ᴳ ⌊ A ⌋ᴬ
  ⌊ var x ⌋      = S4.var ⌊ x ⌋ˣ
  ⌊ lam t ⌋      = S4.lam ⌊ t ⌋
  ⌊ app t₁ t₂ ⌋  = S4.app ⌊ t₁ ⌋ ⌊ t₂ ⌋
  ⌊ *var x ⌋     = S4.*var ⌊ x ⌋ˣ
  ⌊ up t ⌋       = S4.up ⌊ t ⌋
  ⌊ down t₁ t₂ ⌋ = S4.down ⌊ t₁ ⌋ ⌊ t₂ ⌋
  ⌊ pair t₁ t₂ ⌋ = S4.pair ⌊ t₁ ⌋ ⌊ t₂ ⌋
  ⌊ fst t ⌋      = S4.fst ⌊ t ⌋
  ⌊ snd t ⌋      = S4.snd ⌊ t ⌋


mutual
  ⟦_⟧ᴬ : Ty → Set
  ⟦ ⊥ ⟧ᴬ    = Empty
  ⟦ A ⊃ B ⟧ᴬ = ⟦ A ⟧ᴬ → ⟦ B ⟧ᴬ
  ⟦ A ∧ B ⟧ᴬ = ⟦ A ⟧ᴬ × ⟦ B ⟧ᴬ
  ⟦ t ∴ A ⟧ᴬ = ∃ (λ t′ → t ≡ t′) × ⟦ A ⟧ᴬ

  ⟦_⟧ᴳ : Cx Ty → Set
  ⟦ ∅ ⟧ᴳ       = Unit
  ⟦ (Γ , A) ⟧ᴳ = ⟦ Γ ⟧ᴳ × ⟦ A ⟧ᴬ

  ⟦_⟧ˣ : ∀ {Γ A} → Var Ty Γ A → ⟦ Γ ⟧ᴳ → ⟦ A ⟧ᴬ
  ⟦ top ⟧ˣ   (γ , a) = a
  ⟦ pop x ⟧ˣ (γ , b) = ⟦ x ⟧ˣ γ

  ⟦_⟧ : ∀ {Γ Δ A} → Tm Γ Δ A → ⟦ Γ ⟧ᴳ → ⟦ Δ ⟧ᴳ → ⟦ A ⟧ᴬ
  ⟦ var x ⟧      γ δ = ⟦ x ⟧ˣ γ
  ⟦ lam t ⟧      γ δ = λ a → ⟦ t ⟧ (γ , a) δ
  ⟦ app t₁ t₂ ⟧  γ δ = (⟦ t₁ ⟧ γ δ) (⟦ t₂ ⟧ γ δ)
  ⟦ *var x ⟧     γ δ = ⟦ x ⟧ˣ δ
  ⟦ up t ⟧       γ δ = ((t , refl) , ⟦ t ⟧ unit δ)
  ⟦ down t₁ t₂ ⟧ γ δ with ⟦ t₁ ⟧ γ δ
  …                 | ((t , refl) , *a) = ⟦ t₂ ⟧ γ (δ , *a)
  ⟦ pair t₁ t₂ ⟧ γ δ = (⟦ t₁ ⟧ γ δ , ⟦ t₂ ⟧ γ δ)
  ⟦ fst t ⟧      γ δ = proj₁ (⟦ t ⟧ γ δ)
  ⟦ snd t ⟧      γ δ = proj₂ (⟦ t ⟧ γ δ)