===============================================
 =                                             =
 =  §3.2  Lifting to higher-order functionals  =
 =                                             =
 ===============================================

    Chuangjie Xu, July 2019

    Updated in February 2020

\begin{code}

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

open import Preliminaries
open import T
open import TAuxiliaries

\end{code}

■ A nucleus for lifting to higher types

\begin{code}

module Lifting (X : Ty) where

 : Ty
 = X  ι

η : {Γ : Cxt}  T Γ (ι  )
η = Lam (Lam ν₁)
 -- λ n  x . n

κ : {Γ : Cxt}  T Γ ((ι  )    )
κ = Lam (Lam (Lam (ν₂ · (ν₁ · ν₀) · ν₀)))
 -- λ g   f    x . g     (f  x)    x

--
-- Instantiate the translation by importing the following module
-- with the nucleus (Jι, η, κ)
--
open import GentzenTranslation  η κ

\end{code}

■ Relating terms and their lifting via a parametrized logical relation

\begin{code}

--
-- Base case of the logical relation
--
 :  X ⟧ʸ   ι ⟧ʸ    ⟧ʸ  Set
 x n f = n  f x

--
-- η preserves the logical relation
--
 : (x :  X ⟧ʸ)
    {Γ : Cxt} (γ :  Γ ⟧ˣ) (n :  ι ⟧ʸ)   x n ( η ⟧ᵐ γ n)
 x _ n = refl

--
-- κ preserves the logical relation
--
 : (x :  X ⟧ʸ)
    {Γ : Cxt} (γ :  Γ ⟧ˣ) {f :  ι  ι ⟧ʸ} {g :  ι   ⟧ʸ}
    (∀ i   x (f i) (g i))   {n h}   x n h   x (f n) ( κ ⟧ᵐ γ g h)
 x γ {f} {g} ζ {n} {h} θ = transport  z  f n  g z x) θ (ζ n)

--
-- Extend Rι to R for all types of T
--
R :  X ⟧ʸ  {ρ : Ty}   ρ ⟧ʸ    ρ ⟩ᴶ ⟧ʸ  Set
R x = LR._R_
 where
  import LogicalRelation  η κ ( x) ( x) ( x) as LR

\end{code}

■ If one can construct a generic element Ω : Xᴶ such that R x x Ω,
  then f = fᴶΩ up to pointwise equality.

\begin{code}

Cor : (Ω : T ε  X ⟩ᴶ)  (∀ x  R x x  Ω )
     (t : T ε (X  ι))
      x   t  x   t  · Ω  x
Cor Ω r t x = LR.FTLR t  (r x)
 where
  import LogicalRelation  η κ ( x) ( x) ( x) as LR

\end{code}