=====================================
 =                                   =
 =  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 20 _✶_

_✶_ : {Γ : 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 60 _ᴷ

_ᴷ : {Γ : 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}