======================================
 =                                    =
 =  Example: lifting to higher types  =
 =                                    =
 ======================================

    Chuangjie Xu, July 2019

\begin{code}

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

open import Preliminaries
open import Tplus

\end{code}

■ A nucleus for lifting to higher types

\begin{code}

module Lifting (X : Ty) where

J : Ty → Ty
J σ = X ⇾ σ

η : {Γ : Cxt} {σ : Ty} → T Γ (σ ⇾ J σ)
η = Lam (Lam ν₁)

κ : {Γ : Cxt} {σ τ : Ty} → T Γ ((σ ⇾ J τ) ⇾ J σ ⇾ J τ)
κ = Lam (Lam (Lam (ν₂ · (ν₁ · ν₀) · ν₀)))

\end{code}

■ Relating terms and their lifting

\begin{code}

open import GentzenTranslation J η κ public

R : {ρ : Ty} → ⟦ X ⟧ʸ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ → ⟦ ρ ⟧ʸ → Set
R {ι    } x  φ       n      = n ≡ φ x
R {σ ⊠ τ} x (α , β) (a , b) = R x α a × R x β b
R {σ ⊞ τ} x  φ      (inl a) = case (λ α → R x α a) (λ _ → 𝟘) (φ x)
R {σ ⊞ τ} x  φ      (inr b) = case (λ _ → 𝟘) (λ β → R x β b) (φ x)
R {σ ⇾ τ} x  φ       f      = {α : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {a : ⟦ σ ⟧ʸ} → R x α a → R x (φ α) (f a)

--
-- The Kleisli extension for the base type preserves R.
--
R[KEᶥ] : (ρ : Ty) {Γ : Cxt} {γ : ⟦ Γ ⟧ˣ} (x : ⟦ X ⟧ʸ)
       → {f : ℕ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ} {g : ℕ → ⟦ ρ ⟧ʸ}
       → ((i : ℕ) → R x (f i) (g i))
       → R x (⟦ KE ρ ⟧ᵐ γ f) g

--
-- The Kleisli extension for coproducts preserves R.
--
R[KE⁺] : (ρ : Ty) (x : ⟦ X ⟧ʸ) {σ τ : Ty} {Γ : Cxt} {γ : ⟦ Γ ⟧ˣ}
       → (φ : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ + ⟦ ⟨ τ ⟩ᴶ ⟧ʸ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ) (f : ⟦ σ ⟧ʸ + ⟦ τ ⟧ʸ → ⟦ ρ ⟧ʸ)
       → ({α : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {a : ⟦ σ ⟧ʸ} → R x α a → R x (φ (inl α)) (f (inl a)))
       → ({β : ⟦ ⟨ τ ⟩ᴶ ⟧ʸ} {b : ⟦ τ ⟧ʸ} → R x β b → R x (φ (inr β)) (f (inr b)))
       → R x (⟦ KE ρ ⟧ᵐ γ φ) f

--
-- Extending R to contexts
--
Rˣ : {Γ : Cxt} → ⟦ X ⟧ʸ → ⟦ ⟪ Γ ⟫ᴶ ⟧ˣ → ⟦ Γ ⟧ˣ → Set
Rˣ {ε}     _  _       _      = 𝟙
Rˣ {Γ ₊ ρ} x (γ , a) (ξ , b) = Rˣ x γ ξ × R x a b

--
-- Variables in related contexts are related.
--
R[Var] : {Γ : Cxt} {ρ : Ty} {γ : ⟦ ⟪ Γ ⟫ᴶ ⟧ˣ} {ξ : ⟦ Γ ⟧ˣ} (x : ⟦ X ⟧ʸ)
       → Rˣ x γ ξ → (i : ∥ ρ ∈ Γ ∥) → R x (γ ₍ ⟨ i ⟩ᵛ ₎) (ξ ₍ i ₎)
R[Var] x (_ , θ)  zero    = θ
R[Var] x (ζ , _) (succ i) = R[Var] x ζ i

--
-- Any T term is related to its translation.
--
Lemma[R] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ) (x : ⟦ X ⟧ʸ)
         → {γ : ⟦ ⟪ Γ ⟫ᴶ ⟧ˣ} {ξ : ⟦ Γ ⟧ˣ} → Rˣ x γ ξ
         → R x (⟦ t ᴶ ⟧ᵐ γ) (⟦ t ⟧ᵐ ξ)
Lemma[R] (Var i) x ζ = R[Var] x ζ i
Lemma[R] (Lam t) x ζ = λ χ → Lemma[R] t x (ζ , χ)
Lemma[R] (f · a) x ζ = Lemma[R] f x ζ (Lemma[R] a x ζ)
Lemma[R] Zero    _ _ = refl
Lemma[R] Succ    _ _ = ap succ
Lemma[R](Rec{ρ}) x _ {α} {a} χ {φ} {f} ξ = R[KEᶥ] ρ x claim
 where
  claim : (i : ℕ) → R x (rec α (λ k → φ (λ _ → k)) i) (rec a f i)  
  claim         = χ
  claim (succ i) = ξ refl (claim i)
Lemma[R] Pair _ _ = λ χ₀ χ₁ → χ₀ , χ₁
Lemma[R] Pr1  _ _ = pr₁
Lemma[R] Pr2  _ _ = pr₂
Lemma[R] Inj1 _ _ = λ χ → χ
Lemma[R] Inj2 _ _ = λ χ → χ
Lemma[R](Case{ρ}) x _ χ η {ω} {w} = R[KE⁺] ρ x (case _ _) (case _ _) χ η {ω} {w}

\end{code}

■ Detailed proofs

\begin{code}

R⁺≡LL : {σ ρ : Ty} {x : ⟦ X ⟧ʸ}
      → {ω : ⟦ ⟨ σ ⊞ ρ ⟩ᴶ ⟧ʸ} {w : ⟦ σ ⊞ ρ ⟧ʸ}
      → {α : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {a : ⟦ σ ⟧ʸ}
      → ω x ≡ inl α → w ≡ inl a
      → R x α a ≡ R x ω w
R⁺≡LL e refl = sym (case⁼ˡ e)

R⁺≡RR : {σ ρ : Ty} {x : ⟦ X ⟧ʸ}
      → {ω : ⟦ ⟨ σ ⊞ ρ ⟩ᴶ ⟧ʸ} {w : ⟦ σ ⊞ ρ ⟧ʸ}
      → {β : ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ} {b : ⟦ ρ ⟧ʸ}
      → ω x ≡ inr β → w ≡ inr b
      → R x β b ≡ R x ω w
R⁺≡RR e refl = sym (case⁼ʳ e)

{- Proof of
R[KEᶥ] : (ρ : Ty) {Γ : Cxt} {γ : ⟦ Γ ⟧ˣ} (x : ⟦ X ⟧ʸ)
       → {f : ℕ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ} {g : ℕ → ⟦ ρ ⟧ʸ}
       → ((i : ℕ) → R x (f i) (g i))
       → R x (⟦ KE ρ ⟧ᵐ γ f) g
-}
R[KEᶥ]  ι      x ζ χ = trans (ζ _) (ap _ χ)
R[KEᶥ] (τ ⇾ ρ) x ζ χ = λ ξ → R[KEᶥ] ρ x (λ i → ζ i ξ) χ
R[KEᶥ] (τ ⊠ ρ) x ζ χ = R[KEᶥ] τ x (pr₁ ∘ ζ) χ , R[KEᶥ] ρ x (pr₂ ∘ ζ) χ
R[KEᶥ] (τ ⊞ ρ) x {f} {g} ζ {φ} {n} χ = claim₀ (g n) (ζ n) claim₁
 where
  claim₀ : {δ : ⟦ ⟨ τ ⊞ ρ ⟩ᴶ ⟧ʸ} (d : ⟦ τ ⊞ ρ ⟧ʸ)
         → R x (f n) d → f n x ≡ δ x → R x δ d
  claim₀ (inl a) ξ e = transport (case (λ α → R x α a) (λ _ → 𝟘)) e ξ
  claim₀ (inr b) ξ e = transport (case (λ _ → 𝟘) (λ β → R x β b)) e ξ
  claim₁ : f n x ≡ f (φ x) x
  claim₁ = ap (λ k → f k x) χ

{- Proof of
R[KE⁺] : (ρ : Ty) (x : ⟦ X ⟧ʸ) {σ τ : Ty} {Γ : Cxt} {γ : ⟦ Γ ⟧ˣ}
       → (φ : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ + ⟦ ⟨ τ ⟩ᴶ ⟧ʸ → ⟦ ⟨ ρ ⟩ᴶ ⟧ʸ) (f : ⟦ σ ⟧ʸ + ⟦ τ ⟧ʸ → ⟦ ρ ⟧ʸ)
       → ({α : ⟦ ⟨ σ ⟩ᴶ ⟧ʸ} {a : ⟦ σ ⟧ʸ} → R x α a → R x (φ (inl α)) (f (inl a)))
       → ({β : ⟦ ⟨ τ ⟩ᴶ ⟧ʸ} {b : ⟦ τ ⟧ʸ} → R x β b → R x (φ (inr β)) (f (inr b)))
       → R x (⟦ KE ρ ⟧ᵐ γ φ) f
-}
R[KE⁺] ι x φ f ζ ξ {ω} {inl a} χ with inspect (ω x)
... | inl α with≡ e = trans claim₀ claim₁
 where
  θ : R x α a
  θ = transport (case _ _) e χ
  claim₀ : f (inl a) ≡ φ (inl α) x
  claim₀ = ζ θ
  claim₁ : φ (inl α) x ≡ φ (ω x) x
  claim₁ = ap (λ z → φ z x) (sym e)
... | inr β with≡ e = 𝟘-elim (transport (case _ _) e χ)
R[KE⁺] ι x φ f ζ ξ {ω} {inr b} χ with inspect (ω x)
... | inl α with≡ e = 𝟘-elim (transport (case _ _) e χ)
... | inr β with≡ e = trans claim₀ claim₁
 where
  θ : R x β b
  θ = transport (case _ _) e χ
  claim₀ : f (inr b) ≡ φ (inr β) x
  claim₀ = ξ θ
  claim₁ : φ (inr β) x ≡ φ (ω x) x
  claim₁ = ap (λ z → φ z x) (sym e)
R[KE⁺] (ρ ⊠ ρ') x φ f ζ ξ χ = R[KE⁺] ρ x (pr₁ ∘ φ) (pr₁ ∘ f) (pr₁ ∘ ζ) (pr₁ ∘ ξ) χ ,
                              R[KE⁺] ρ' x (pr₂ ∘ φ) (pr₂ ∘ f) (pr₂ ∘ ζ) (pr₂ ∘ ξ) χ
R[KE⁺] (ρ ⊞ ρ') x φ f ζ ξ {ω} {inl a} χ with inspect (ω x)
... | inl α with≡ e = goal
 where
  θ : R x α a
  θ = transport (case _ _) e χ
  claim₀ : R x (φ (ω x)) (f (inl a))
  claim₀ = transport (λ z → R x (φ z) (f (inl a))) (sym e) (ζ θ)
  goal : R x (λ y → φ (ω y) y) (f (inl a))
  goal with inspect (f (inl a)) | inspect (φ (ω x) x)
  ... | inl u with≡ ef | inl v with≡ eφ = transport (λ X → X) (R⁺≡LL eφ ef) claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inl u) -- case (λ γ → R x γ u) (λ _ → 𝟘) (φ (ω x) x)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : R x v u -- case (λ γ → R x γ u) (λ _ → 𝟘) (inl v)
    claim₂ = transport (case _ _) eφ claim₁
  ... | inl u with≡ ef | inr t with≡ eφ = 𝟘-elim claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inl u)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : 𝟘
    claim₂ = transport (case _ _) eφ claim₁
  ... | inr s with≡ ef | inl v with≡ eφ = 𝟘-elim claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inr s) -- case (λ _ → 𝟘) (λ γ → R x γ s) (φ (ω x) x)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : 𝟘
    claim₂ = transport (case _ _) eφ claim₁
  ... | inr s with≡ ef | inr t with≡ eφ = transport (λ X → X) (R⁺≡RR eφ ef) claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inr s) -- case (λ _ → 𝟘) (λ γ → R x γ s) (φ (ω x) x)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : R x t s
    claim₂ = transport (case _ _) eφ claim₁
R[KE⁺] (ρ ⊞ ρ') x φ f ζ ξ {ω} {inl a} χ | inr β with≡ e = 𝟘-elim (transport (case _ _) e χ)
R[KE⁺] (ρ ⊞ ρ') x φ f ζ ξ {ω} {inr b} χ with inspect (ω x)
... | inl α with≡ e = 𝟘-elim (transport (case _ _) e χ)
... | inr β with≡ e = goal
 where
  θ : R x β b
  θ = transport (case _ _) e χ
  claim₀ : R x (φ (ω x)) (f (inr b))
  claim₀ = transport (λ z → R x (φ z) (f (inr b))) (sym e) (ξ θ)
  goal : R x (λ y → φ (ω y) y) (f (inr b))
  goal with inspect (f (inr b)) | inspect (φ (ω x) x)
  ... | inl u with≡ ef | inl v with≡ eφ = transport (λ X → X) (R⁺≡LL eφ ef) claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inl u) -- case (λ γ → R x γ u) (λ _ → 𝟘) (φ (ω x) x)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : R x v u -- case (λ γ → R x γ u) (λ _ → 𝟘) (inl v)
    claim₂ = transport (case _ _) eφ claim₁
  ... | inl u with≡ ef | inr t with≡ eφ = 𝟘-elim claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inl u)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : 𝟘
    claim₂ = transport (case _ _) eφ claim₁
  ... | inr s with≡ ef | inl v with≡ eφ = 𝟘-elim claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inr s) -- case (λ _ → 𝟘) (λ γ → R x γ s) (φ (ω x) x)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : 𝟘
    claim₂ = transport (case _ _) eφ claim₁
  ... | inr s with≡ ef | inr t with≡ eφ = transport (λ X → X) (R⁺≡RR eφ ef) claim₂
   where
    claim₁ : R {ρ ⊞ ρ'} x (φ (ω x)) (inr s) -- case (λ _ → 𝟘) (λ γ → R x γ s) (φ (ω x) x)
    claim₁ = transport (R x _) ef claim₀
    claim₂ : R x t s
    claim₂ = transport (case _ _) eφ claim₁
R[KE⁺] (ρ ⇾ ρ') x φ f ζ ξ χ η = R[KE⁺] ρ' x (λ z → φ z _) (λ z → f z _) (λ θ → ζ θ η) (λ θ → ξ θ η) χ

\end{code}