=========================================
 =                                       =
 =  A Gentzen-style monadic translation  =
 =                                       =
 =========================================

    Chuangjie Xu, July 2019

\begin{code}

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

open import Tplus

module GentzenTranslation
       (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 ⟩ᵛ

KE : (ρ : Ty) {σ : Ty} {Γ : Cxt}
   → T Γ ((σ ⇾ ⟨ ρ ⟩ᴶ) ⇾ J σ ⇾ ⟨ ρ ⟩ᴶ)
KE  ι      = κ
KE (τ ⊠ ρ) = Lam (Lam (Pair · (KE τ · Lam (Pr1 · (ν₂ · ν₀)) · ν₀)
                            · (KE ρ · Lam (Pr2 · (ν₂ · ν₀)) · ν₀)))
KE (τ ⊞ ρ) = κ
KE (τ ⇾ ρ) = Lam (Lam (Lam (KE ρ · 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 (KE ρ · (Rec · ν₁ · Lam (ν₁ · (η · ν₀)))))
Pair ᴶ    = Pair
Pr1 ᴶ     = Pr1
Pr2 ᴶ     = Pr2
Inj1 ᴶ    = Lam (η · (Inj1 · ν₀))
Inj2 ᴶ    = Lam (η · (Inj2 · ν₀))
Case{ρ} ᴶ = Lam (Lam (KE ρ · (Case · ν₁ · ν₀)))

\end{code}