=====================================
 =                                   =
 =  A Kuroda-style translation of T  =
 =                                   =
 =====================================

    Chuangjie Xu, July 2019


References.

□ Thomas Powell.  A functional interpretation with state.  In:
  Proceedings of the Thirty third Annual IEEE Symposium on Logic in
  Computer Science (LICS 2018), IEEE Computer Society Press, 2018,
  pp. 839–848.


\begin{code}

{-# OPTIONS --without-K --safe #-}

open import Tplus

module KurodaTranslation
       (J : Ty → Ty)
       (η : {Γ : Cxt} {σ : Ty} → T Γ (σ ⇾ J σ))
       (κ : {Γ : Cxt} {σ τ : Ty} → T Γ ((σ ⇾ J τ) ⇾ J σ ⇾ J τ))
 where

⟨_⟩ᴷ ⟨_⟩ : Ty → Ty
⟨ ρ ⟩ᴷ    = J ⟨ ρ ⟩
⟨ ι ⟩     = ι
⟨ σ ⊠ τ ⟩ = ⟨ σ ⟩ ⊠ ⟨ τ ⟩
⟨ σ ⊞ τ ⟩ = ⟨ σ ⟩ ⊞ ⟨ τ ⟩
⟨ σ ⇾ τ ⟩ = ⟨ σ ⟩ ⇾ J ⟨ τ ⟩

⟪_⟫ : Cxt → Cxt
⟪ ε ⟫     = ε
⟪ Γ ₊ ρ ⟫ = ⟪ Γ ⟫ ₊ ⟨ ρ ⟩

⟨_⟩ᵛ : {Γ : Cxt} {ρ : Ty} → ∥ ρ ∈ Γ ∥ → ∥ ⟨ ρ ⟩ ∈ ⟪ Γ ⟫ ∥
⟨ zero ⟩ᵛ   = zero
⟨ succ i ⟩ᵛ = succ ⟨ i ⟩ᵛ

infixl  _✶_

_✶_ : {Γ : Cxt} {σ τ : Ty} → T Γ (J (σ ⇾ J τ)) → T Γ (J σ) → T Γ (J τ)
f ✶ a = κ · Lam (κ · ν₀ · wkn a) · f
     -- κ (λ h → κ h a) f

Rec✶ : {Γ : Cxt} {ρ : Ty} → T Γ (ρ ⇾ (ι ⇾ J (ρ ⇾ J ρ)) ⇾ ι ⇾ J ρ)
Rec✶ = Lam (Lam (Rec · (η · ν₁) · Lam (Lam (ν₂ · ν₁ ✶ ν₀))))

infix  _ᴷ

_ᴷ : {Γ : Cxt} {ρ : Ty} → T Γ ρ → T ⟪ Γ ⟫ ⟨ ρ ⟩ᴷ
Var i ᴷ   = η · Var ⟨ i ⟩ᵛ
Lam t ᴷ   = η · Lam (t ᴷ)
(f · a) ᴷ = f ᴷ ✶ a ᴷ
Zero ᴷ    = η · Zero
Succ ᴷ    = η · Lam (η · (Succ · ν₀))
Rec ᴷ     = η · Lam (η · Lam (η · (Rec✶ · ν₁ · ν₀)))
Pair ᴷ    = η · Lam (η · Lam (η · (Pair · ν₁ · ν₀)))
Pr1 ᴷ     = η · Lam (η · (Pr1 · ν₀))
Pr2 ᴷ     = η · Lam (η · (Pr2 · ν₀))
Inj1 ᴷ    = η · Lam (η · (Inj1 · ν₀))
Inj2 ᴷ    = η · Lam (η · (Inj2 · ν₀))
Case ᴷ    = η · Lam (η · Lam (η · (Case · ν₁ · ν₀)))

\end{code}