=========================================
 =                                       =
 =  A Kolmogorov-style translation of T  =
 =                                       =
 =========================================

    Chuangjie Xu, July 2019


References.

□ Tarmo Uustalu.  Monad translating inductive and coinductive types.
  In: H. Geuvers, F. Wiedijk (Eds.), Types for Proofs and Programs
  (TYPES 2002). Lecture Notes in Computer Science, vol 2646, Springer,
  2002, pp. 299–315.


\begin{code}

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

open import Tplus

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

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

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

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

infixl  _◇_

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

Rec◇ : {Γ : Cxt} {ρ : Ty} → T Γ (ρ ⇾ (J ι ⇾ J (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 ᴷᵒ     = η · (κ · Pr1)
Pr2 ᴷᵒ     = η · (κ · Pr2)
Inj1 ᴷᵒ    = η · Lam (η · (Inj1 · ν₀))
Inj2 ᴷᵒ    = η · Lam (η · (Inj2 · ν₀))
Case ᴷᵒ    = η · (κ · Lam (η · (κ · Lam (η · (κ · (Case · ν₁ · ν₀))))))

\end{code}