Chuangjie Xu, November 2016

-------------------------------------------
   Nonstandard Dialectica interpretation
-------------------------------------------

We implement the term extraction algorithm via a nonstandard
Dialectica interpretation for system H introduced in

   B. van den Berg, E. Briseid, and P. Safarik, A functional
   interpretation for nonstandard arithmetic, Annals of pure
   and applied logic 163 (2012), no. 12, 1962–1994.

In this module, we

(1) define the types d⁺(Φ) of actual realisers and d⁻(Φ) of
    counterexamples by induction on formula Φ;

(2) construct a realiser 𝔯(p):(d⁺Φ)* of formula Φ from its proof p by
    induction on p, following the soundness proof of the nonstandard
    Dialectica interpretation;

(3) embed the realiser 𝔯(p) into Agda to get an Agda term.

It is too complicated to implement the whole soundness proof in Agda.
The main difficulty is that, for arbitrary formula Φ, we have

    d⁺(Φ) = d⁺(Φ[x:=t])   and   d⁻(Φ) = d⁻(Φ[x:=t])              (†)

only up to identity type.  Then, given r:d⁺(Φ), we have to transport
it along the above equality/path to get an element of d⁺(Φ[x:=t]).
Since the above equality is (implicitly) used in many places of the
soundness proof, we have to apply the transport function many times
and also need a few lemmas about those transported terms.  This makes
proving the soundness theorem very difficult and the resulting proof
unreadable.  Notice that for a concrete formula Φ the above equations
hold judgementally and hence no transport is needed (this is similar
to the situation that one can only prove ∀n,m.n+m=m+n up to identity
type in intensional type theory, but if n,m are given concretely then
n+m=m+n holds judgementally).

There are at least two directions of addressing this problem:

1. Refine the definition of formulas such that the equations (†) hold
   judgementally.  (But simply adding substitution as a formula
   constructor does not work.)

2. Work instead with extensional type theory, e.g. the Nuprl system,
   so that a term of d⁺⁻(Φ) is also a term of d⁺⁻(Φ[x:=t]).

\begin{code}

{-# OPTIONS --no-termination-check #-}

module Dialectica where

open import Preliminaries
open import DataTypes

\end{code}

System H and its term language T are defined in module H.

\begin{code}

open import H

\end{code}

Types of realisers and counterexamples

\begin{code}

d⁺ d⁻ : {Γ : Cxt} → Fml Γ → Ty
d⁺ (st {σ} t)  = σ
d⁺ (a =ᴴ b)    = ①
d⁺ (a ≤ᴴ b)    = ①
d⁺ (a ∈ᴴ w)    = ①
d⁺ (A ∧ᴴ B)    = (d⁺ A) ⊠ (d⁺ B)
d⁺ (A ∨ᴴ B)    = (d⁺ A) ⊠ (d⁺ B)
d⁺ (A ⇒ᴴ B)    = ((d⁺ A)* ⇾ (d⁺ B)*) ⊠ ((d⁺ A)* ⇾ d⁻ B ⇾ (d⁻ A)*)
d⁺ (∀ᴴ A)      = d⁺ A
d⁺ (∃ᴴ A)      = d⁺ A
d⁺ (∀ˢᵗ {σ} A) = σ ⇾ (d⁺ A)*
d⁺ (∃ˢᵗ {σ} A) = σ ⊠ d⁺ A
d⁺ (Even n)    = ①

d⁻ (st {σ} t)  = ①
d⁻ (a =ᴴ b)    = ①
d⁻ (a ≤ᴴ b)    = ①
d⁻ (a ∈ᴴ w)    = ①
d⁻ (A ∧ᴴ B)    = d⁻ A ⊠ d⁻ B
d⁻ (A ∨ᴴ B)    = d⁻ A ⊠ d⁻ B
d⁻ (A ⇒ᴴ B)    = (d⁺ A)* ⊠ d⁻ B
d⁻ (∀ᴴ A)      = d⁻ A
d⁻ (∃ᴴ A)      = (d⁻ A)*
d⁻ (∀ˢᵗ {σ} A) = σ ⊠ d⁻ A
d⁻ (∃ˢᵗ {σ} A) = (d⁻ A)*
d⁻ (Even n)    = ①

d⁺* : {Γ : Cxt} → Fml Γ → Ty
d⁺* A = (d⁺ A)*

dd⁺* : {Γ : Cxt} → Asmpt Γ → Cxt
dd⁺*  ε      = ε
dd⁺* (Ξ ₊ A) = dd⁺* Ξ ₊ d⁺* A

d⁻* : {Γ : Cxt} → Fml Γ → Ty
d⁻* A = (d⁻ A)*

dd⁻* : {Γ : Cxt} → Asmpt Γ → List Ty
dd⁻*  ε      = ε
dd⁻* (Ξ ₊ A) = dd⁻* Ξ ₊ d⁻* A

Π : List Ty → Ty
Π  ε      = ①
Π (ρ ₊ σ) = Π ρ ⊠ σ

Tms : Cxt → List Ty → Set
Tms Γ ρ = Tm Γ (Π ρ)

wkn⁺⁺ʳ : {Γ : Cxt} (Ξ Ζ : Asmpt Γ) {σ : Ty}
      → Tm (Γ ₊₊ dd⁺* Ξ) σ → Tm (Γ ₊₊ dd⁺* (Ξ ₊₊ Ζ)) σ
wkn⁺⁺ʳ Ξ  ε      t = t
wkn⁺⁺ʳ Ξ (Ζ ₊ A) t = wkn (wkn⁺⁺ʳ Ξ Ζ t)

wkn⁺⁺ʳ⁺ : {Γ : Cxt} (Ξ Ζ : Asmpt Γ) {σ τ : Ty}
       → Tm (Γ ₊₊ dd⁺* Ξ ₊ σ) τ → Tm (Γ ₊₊ dd⁺* (Ξ ₊₊ Ζ) ₊ σ) τ
wkn⁺⁺ʳ⁺ Ξ Ζ t = wkn (wkn⁺⁺ʳ Ξ Ζ (Lam t)) · ν₀

wkn⁺⁺ˡ : {Γ : Cxt} (Ξ Ζ : Asmpt Γ) {σ : Ty}
      → Tm (Γ ₊₊ dd⁺* Ζ) σ → Tm (Γ ₊₊ dd⁺* (Ξ ₊₊ Ζ)) σ
wkn⁺⁺ˡ Ξ  ε      t = wk (⊆-₊₊r (dd⁺* Ξ)) t
wkn⁺⁺ˡ Ξ (Ζ ₊ A) t = wkn (wkn⁺⁺ˡ Ξ Ζ (Lam t)) · ν₀

wkn⁺⁺ˡ⁺ : {Γ : Cxt} (Ξ Ζ : Asmpt Γ) {σ τ : Ty}
       → Tm (Γ ₊₊ dd⁺* Ζ ₊ σ) τ → Tm (Γ ₊₊ dd⁺* (Ξ ₊₊ Ζ) ₊ σ) τ
wkn⁺⁺ˡ⁺ Ξ Ζ t = wkn (wkn⁺⁺ˡ Ξ Ζ (Lam t)) · ν₀


swap⁺ : {Γ : Cxt} {Ξ : Asmpt Γ} (Ζ : Asmpt Γ) {A B : Fml Γ} {σ : Ty}
      → Tm (Γ ₊₊ dd⁺* (Ξ ₊ A ₊ B ₊₊ Ζ)) σ → Tm (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ)) σ
swap⁺  ε      t = wk ⊆-exch t
swap⁺ (Ζ ₊ X) t = wkn (swap⁺ Ζ (Lam t)) · ν₀

Pair⁻ : {Γ Δ : Cxt} (Ξ Ζ : Asmpt Γ)
      → Tms Δ (dd⁻* Ξ) → Tms Δ (dd⁻* Ζ) → Tms Δ (dd⁻* (Ξ ₊₊ Ζ))
Pair⁻ Ξ  ε      u _ = u
Pair⁻ Ξ (Ζ ₊ A) u v = Pair (Pair⁻ Ξ Ζ u (Pr1 v)) (Pr2 v)

pr₁⁻ : {Γ Δ : Cxt} (Ξ Ζ : Asmpt Γ)
     → Tms Δ (dd⁻* (Ξ ₊₊ Ζ)) → Tms Δ (dd⁻* Ξ) 
pr₁⁻ Ξ  ε      w = w
pr₁⁻ Ξ (Ζ ₊ A) w = pr₁⁻ Ξ Ζ (Pr1 w)

pr₂⁻ : {Γ Δ : Cxt} (Ξ Ζ : Asmpt Γ)
     → Tms Δ (dd⁻* (Ξ ₊₊ Ζ)) → Tms Δ (dd⁻* Ζ) 
pr₂⁻ Ξ  ε      w = ✹
pr₂⁻ Ξ (Ζ ₊ A) w = Pair (pr₂⁻ Ξ Ζ (Pr1 w)) (Pr2 w)


infixr  _++ᵐˢ⁻_

_++ᵐˢ⁻_ : {Γ Δ : Cxt} {Ξ : Asmpt Γ}
        → Tms Δ (dd⁻* Ξ) → Tms Δ (dd⁻* Ξ) → Tms Δ (dd⁻* Ξ)
_++ᵐˢ⁻_ {Ξ = ε}     _  _  = ✹
_++ᵐˢ⁻_ {Ξ = _ ₊ _} xs ys = Pair (Pr1 xs ++ᵐˢ⁻ Pr1 ys) (Pr2 xs ++ Pr2 ys)

Nilᵐˢ⁻ : {Γ Δ : Cxt} {Ξ : Asmpt Γ} → Tms Δ (dd⁻* Ξ)
Nilᵐˢ⁻ {Ξ = ε}     = ✹
Nilᵐˢ⁻ {Ξ = Ξ ₊ A} = Pair Nilᵐˢ⁻ Nil

Appᵐˢ⁻ : {Γ Δ : Cxt} {Ξ : Asmpt Γ} {σ : Ty}
       → Tm Δ (σ ⇾ Π (dd⁻* Ξ)) → Tm Δ (σ *) → Tms Δ (dd⁻* Ξ)
Appᵐˢ⁻ f xs = LRec · Nilᵐˢ⁻ · Lam (Lam ((wkn² f · ν₁) ++ᵐˢ⁻ ν₀)) · xs


\end{code}

Some lemmas and auxiliaries due to the fact that

  substitution and weakening of a formula do not change the types
  of its realisers and counterexamples.

\begin{code}


Lm[wk⁺] : {Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → d⁺ A ≡ d⁺ (wkᶠ ξ A)
Lm[wk⁻] : {Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → d⁻ A ≡ d⁻ (wkᶠ ξ A)
Lm[wk⁺] (st t)    = refl
Lm[wk⁺] (a =ᴴ b)  = refl
Lm[wk⁺] (a ≤ᴴ b)  = refl
Lm[wk⁺] (x ∈ᴴ xs) = refl
Lm[wk⁺] (A ∧ᴴ B)  = ⊠⁼ (Lm[wk⁺] A) (Lm[wk⁺] B)
Lm[wk⁺] (A ∨ᴴ B)  = ⊠⁼ (Lm[wk⁺] A) (Lm[wk⁺] B)
Lm[wk⁺] (A ⇒ᴴ B)  = ⊠⁼ (⇾⁼ (*⁼(Lm[wk⁺] A)) (*⁼(Lm[wk⁺] B))) (⇾⁼ (*⁼(Lm[wk⁺] A)) (⇾⁼ (Lm[wk⁻] B) (*⁼(Lm[wk⁻] A))))
Lm[wk⁺] (∀ᴴ A)    = Lm[wk⁺] A
Lm[wk⁺] (∃ᴴ A)    = Lm[wk⁺] A
Lm[wk⁺] (∀ˢᵗ A)   = ⇾⁼ refl (*⁼(Lm[wk⁺] A))
Lm[wk⁺] (∃ˢᵗ A)   = ⊠⁼ refl (Lm[wk⁺] A)
Lm[wk⁺] (Even n)  = refl

Lm[wk⁻] (st t)    = refl
Lm[wk⁻] (a =ᴴ b)  = refl
Lm[wk⁻] (a ≤ᴴ b)  = refl
Lm[wk⁻] (x ∈ᴴ xs) = refl
Lm[wk⁻] (A ∧ᴴ B)  = ⊠⁼ (Lm[wk⁻] A) (Lm[wk⁻] B)
Lm[wk⁻] (A ∨ᴴ B)  = ⊠⁼ (Lm[wk⁻] A) (Lm[wk⁻] B)
Lm[wk⁻] (A ⇒ᴴ B)  = ⊠⁼ (*⁼(Lm[wk⁺] A)) (Lm[wk⁻] B)
Lm[wk⁻] (∀ᴴ A)    = Lm[wk⁻] A
Lm[wk⁻] (∃ᴴ A)    = *⁼ (Lm[wk⁻] A)
Lm[wk⁻] (∀ˢᵗ A)   = ⊠⁼ refl (Lm[wk⁻] A)
Lm[wk⁻] (∃ˢᵗ A)   = *⁼ (Lm[wk⁻] A)
Lm[wk⁻] (Even n)  = refl

Lwk⁺  : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁺ A) → Tm Θ (d⁺ (wkᶠ ξ A))
Lwk⁺  {Θ} A = transport (Tm Θ) (Lm[wk⁺] A)

Rwk⁺  : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁺ (wkᶠ ξ A)) → Tm Θ (d⁺ A)
Rwk⁺  {Θ} A = transport (Tm Θ) (sym (Lm[wk⁺] A))

Lwk⁺* : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁺ A *) → Tm Θ (d⁺ (wkᶠ ξ A) *)
Lwk⁺* {Θ} A = transport (Tm Θ) (*⁼ (Lm[wk⁺] A))

Rwk⁺* : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁺ (wkᶠ ξ A) *) → Tm Θ (d⁺ A *)
Rwk⁺* {Θ} A = transport (Tm Θ) (sym (*⁼ (Lm[wk⁺] A)))

Lwk⁻  : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁻ A) → Tm Θ (d⁻ (wkᶠ ξ A))
Lwk⁻  {Θ} A = transport (Tm Θ) (Lm[wk⁻] A)

Rwk⁻  : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁻ (wkᶠ ξ A)) → Tm Θ (d⁻ A)
Rwk⁻  {Θ} A = transport (Tm Θ) (sym (Lm[wk⁻] A))

Lwk⁻* : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁻ A *) → Tm Θ (d⁻ (wkᶠ ξ A) *)
Lwk⁻* {Θ} A = transport (Tm Θ) (*⁼ (Lm[wk⁻] A))

Rwk⁻* : {Θ Γ Δ : Cxt} {ξ : Γ ⊆ Δ} (A : Fml Γ) → Tm Θ (d⁻ (wkᶠ ξ A) *) → Tm Θ (d⁻ A *)
Rwk⁻* {Θ} A = transport (Tm Θ) (sym (*⁼ (Lm[wk⁻] A)))

Lm[d⁺] : {Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ)) → d⁺ A ≡ d⁺ (A [ u ]ᶠ)
Lm[d⁻] : {Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ)) → d⁻ A ≡ d⁻ (A [ u ]ᶠ)
Lm[d⁺] (st t)    = refl
Lm[d⁺] (a =ᴴ b)  = refl
Lm[d⁺] (a ≤ᴴ b)  = refl
Lm[d⁺] (x ∈ᴴ xs) = refl
Lm[d⁺] (A ∧ᴴ B)  = ⊠⁼ (Lm[d⁺] A) (Lm[d⁺] B)
Lm[d⁺] (A ∨ᴴ B)  = ⊠⁼ (Lm[d⁺] A) (Lm[d⁺] B)
Lm[d⁺] (A ⇒ᴴ B)  = ⊠⁼ (⇾⁼ (*⁼(Lm[d⁺] A)) (*⁼(Lm[d⁺] B))) (⇾⁼ (*⁼(Lm[d⁺] A)) (⇾⁼ (Lm[d⁻] B) (*⁼ (Lm[d⁻] A))))
Lm[d⁺] (∀ᴴ A)    = trans (Lm[wk⁺] A) (Lm[d⁺] (exchᶠ A))
Lm[d⁺] (∃ᴴ A)    = trans (Lm[wk⁺] A) (Lm[d⁺] (exchᶠ A))
Lm[d⁺] (∀ˢᵗ A)   = ⇾⁼ refl (*⁼ (trans (Lm[wk⁺] A) (Lm[d⁺] (exchᶠ A))))
Lm[d⁺] (∃ˢᵗ A)   = ⊠⁼ refl (trans (Lm[wk⁺] A) (Lm[d⁺] (exchᶠ A)))
Lm[d⁺] (Even n)  = refl

Lm[d⁻] (st t)    = refl
Lm[d⁻] (a =ᴴ b)  = refl
Lm[d⁻] (a ≤ᴴ b)  = refl
Lm[d⁻] (x ∈ᴴ xs) = refl
Lm[d⁻] (A ∧ᴴ B)  = ⊠⁼ (Lm[d⁻] A) (Lm[d⁻] B)
Lm[d⁻] (A ∨ᴴ B)  = ⊠⁼ (Lm[d⁻] A) (Lm[d⁻] B)
Lm[d⁻] (A ⇒ᴴ B)  = ⊠⁼ (*⁼(Lm[d⁺] A)) (Lm[d⁻] B)
Lm[d⁻] (∀ᴴ A)    = trans (Lm[wk⁻] A) (Lm[d⁻] (exchᶠ A))
Lm[d⁻] (∃ᴴ A)    = *⁼ (trans (Lm[wk⁻] A) (Lm[d⁻] (exchᶠ A)))
Lm[d⁻] (∀ˢᵗ A)   = ⊠⁼ refl (trans (Lm[wk⁻] A) (Lm[d⁻] (exchᶠ A)))
Lm[d⁻] (∃ˢᵗ A)   = *⁼ (trans (Lm[wk⁻] A) (Lm[d⁻] (exchᶠ A)))
Lm[d⁻] (Even n)  = refl

Lm[d⁺*] : {Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ)) → (d⁺ A)* ≡ (d⁺ (A [ u ]ᶠ))*
Lm[d⁺*] A = *⁼ (Lm[d⁺] A)

Lm[d⁻*] : {Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ)) → (d⁻ A)* ≡ (d⁻ (A [ u ]ᶠ))*
Lm[d⁻*] A = *⁼ (Lm[d⁻] A)

L⁺* : {Δ Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ))
    → Tm Δ ((d⁺ A)*) → Tm Δ ((d⁺ (A [ u ]ᶠ))*)
L⁺* {Δ} A = transport (Tm Δ) (Lm[d⁺*] A)

R⁺* : {Δ Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ))
    → Tm Δ ((d⁺ (A [ u ]ᶠ))*) → Tm Δ ((d⁺ A)*)
R⁺* {Δ} A = transport (Tm Δ) (sym (Lm[d⁺*] A))

L⁻  : {Δ Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ))
    → Tm Δ (d⁻ A) → Tm Δ (d⁻ (A [ u ]ᶠ))
L⁻  {Δ} A = transport (Tm Δ) (Lm[d⁻] A)

L⁻* : {Δ Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ))
    → Tm Δ (d⁻ A *) → Tm Δ (d⁻ (A [ u ]ᶠ) *)
L⁻* {Δ} A = transport (Tm Δ) (*⁼(Lm[d⁻] A))

R⁻  : {Δ Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ))
    → Tm Δ (d⁻ (A [ u ]ᶠ)) → Tm Δ (d⁻ A)
R⁻  {Δ} A = transport (Tm Δ) (sym (Lm[d⁻] A))

R⁻* : {Δ Γ : Cxt} {σ : Ty} {u : Tm Γ σ} (A : Fml (Γ ₊ σ))
    → Tm Δ (d⁻ (A [ u ]ᶠ) *) → Tm Δ (d⁻ A *)
R⁻* {Δ} A = transport (Tm Δ) (*⁼(sym (Lm[d⁻] A)))

Lm[s]⁺ : {Γ : Cxt} (A : Fml (Γ ₊ Ⓝ)) → d⁺ A ≡ d⁺ (A [s]ᶠ)
Lm[s]⁻ : {Γ : Cxt} (A : Fml (Γ ₊ Ⓝ)) → d⁻ A ≡ d⁻ (A [s]ᶠ)
Lm[s]⁺ (st t)    = refl
Lm[s]⁺ (a =ᴴ b)  = refl
Lm[s]⁺ (a ≤ᴴ b)  = refl
Lm[s]⁺ (x ∈ᴴ xs) = refl
Lm[s]⁺ (A ∧ᴴ B)  = ⊠⁼ (Lm[s]⁺ A) (Lm[s]⁺ B)
Lm[s]⁺ (A ∨ᴴ B)  = ⊠⁼ (Lm[s]⁺ A) (Lm[s]⁺ B)
Lm[s]⁺ (A ⇒ᴴ B)  = ⊠⁼ (⇾⁼ (*⁼(Lm[s]⁺ A)) (*⁼(Lm[s]⁺ B))) (⇾⁼ (*⁼(Lm[s]⁺ A)) (⇾⁼ (Lm[s]⁻ B) (*⁼(Lm[s]⁻ A))))
Lm[s]⁺ (∀ᴴ A)    = trans (Lm[wk⁺] A) (trans (Lm[s]⁺ (exchᶠ A)) (Lm[wk⁺] (exchᶠ A [s]ᶠ)))
Lm[s]⁺ (∃ᴴ A)    = trans (Lm[wk⁺] A) (trans (Lm[s]⁺ (exchᶠ A)) (Lm[wk⁺] (exchᶠ A [s]ᶠ)))
Lm[s]⁺ (∀ˢᵗ A)   = ⇾⁼ refl (*⁼(trans (Lm[wk⁺] A) (trans (Lm[s]⁺ (exchᶠ A)) (Lm[wk⁺] (exchᶠ A [s]ᶠ)))))
Lm[s]⁺ (∃ˢᵗ A)   = ⊠⁼ refl (trans (Lm[wk⁺] A) (trans (Lm[s]⁺ (exchᶠ A)) (Lm[wk⁺] (exchᶠ A [s]ᶠ))))
Lm[s]⁺ (Even n)  = refl

Lm[s]⁻ (st t)    = refl
Lm[s]⁻ (a =ᴴ b)  = refl
Lm[s]⁻ (a ≤ᴴ b)  = refl
Lm[s]⁻ (x ∈ᴴ xs) = refl
Lm[s]⁻ (A ∧ᴴ B)  = ⊠⁼ (Lm[s]⁻ A) (Lm[s]⁻ B)
Lm[s]⁻ (A ∨ᴴ B)  = ⊠⁼ (Lm[s]⁻ A) (Lm[s]⁻ B)
Lm[s]⁻ (A ⇒ᴴ B)  = ⊠⁼ (*⁼(Lm[s]⁺ A)) (Lm[s]⁻ B)
Lm[s]⁻ (∀ᴴ A)    = trans (Lm[wk⁻] A) (trans (Lm[s]⁻ (exchᶠ A)) (Lm[wk⁻] (exchᶠ A [s]ᶠ)))
Lm[s]⁻ (∃ᴴ A)    = *⁼(trans (Lm[wk⁻] A) (trans (Lm[s]⁻ (exchᶠ A)) (Lm[wk⁻] (exchᶠ A [s]ᶠ))))
Lm[s]⁻ (∀ˢᵗ A)   = ⊠⁼ refl (trans (Lm[wk⁻] A) (trans (Lm[s]⁻ (exchᶠ A)) (Lm[wk⁻] (exchᶠ A [s]ᶠ))))
Lm[s]⁻ (∃ˢᵗ A)   = *⁼(trans (Lm[wk⁻] A) (trans (Lm[s]⁻ (exchᶠ A)) (Lm[wk⁻] (exchᶠ A [s]ᶠ))))
Lm[s]⁻ (Even n)  = refl


Lm[dd⁺*-wkn] : {Γ : Cxt} (Ξ : Asmpt Γ) {σ : Ty} → dd⁺* Ξ ≡ dd⁺* (wknᵃ {Γ} {σ} Ξ)
Lm[dd⁺*-wkn]  ε      = refl
Lm[dd⁺*-wkn] (Ξ ₊ A) = ₊⁼ (Lm[dd⁺*-wkn] Ξ) (*⁼ (Lm[wk⁺] A))


Lm[dd⁻*-wkn] : {Γ : Cxt} (Ξ : Asmpt Γ) {σ : Ty} → dd⁻* Ξ ≡ dd⁻* (wknᵃ {Γ} {σ} Ξ)
Lm[dd⁻*-wkn]  ε      = refl
Lm[dd⁻*-wkn] (Ξ ₊ A) = ₊⁼ (Lm[dd⁻*-wkn] Ξ) (*⁼ (Lm[wk⁻] A))


\end{code}

Realisers constructed from proofs

\begin{code}

𝔯 : {Γ : Cxt} {Ξ : Asmpt Γ} {A : Fml Γ} → Prf Ξ A
  → Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ A *)
𝔠 : {Γ : Cxt} {Ξ : Asmpt Γ} {A : Fml Γ} → Prf Ξ A
  → Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
𝔯 Id         = ν₀
𝔯 (Wkn p)    = wkn (𝔯 p)
𝔯 (Swap Ζ p) = swap⁺ Ζ (𝔯 p)
𝔯 RecZer  = 𝒄
𝔯 RecSuc  = 𝒄
𝔯 LRecNil = 𝒄
𝔯 LRecCon = 𝒄
𝔯 β-eq    = 𝒄
𝔯 η-eq    = 𝒄
𝔯 βˣ-eq₁  = 𝒄
𝔯 βˣ-eq₂  = 𝒄
𝔯 ηˣ-eq   = 𝒄
𝔯 Refl        = 𝒄
𝔯 (Sym _)     = 𝒄
𝔯 (Trans _ _) = 𝒄
𝔯 (ApF _)     = 𝒄
--𝔯 (Transp P e p) = L⁺* P (R⁺* P (𝔯 p))
𝔯 (FunExt _)     = 𝒄
𝔯  ≤-Zero = 𝒄
𝔯 (≤-Succ _) = 𝒄
𝔯  ∈-zero     = 𝒄
𝔯 (∈-succ _) = 𝒄
𝔯 (⊥-elim _) = 𝒄
𝔯 (∧-intro p q) = Pairᴸ (𝔯 p) (𝔯 q)
𝔯 (∧-elim₁ p)   = Pr1ᴸ (𝔯 p)
𝔯 (∧-elim₂ p)   = Pr2ᴸ (𝔯 p)
𝔯 (∨-inl p) = Pairᴸ (𝔯 p) 𝒄
𝔯 (∨-inr p) = Pairᴸ 𝒄 (𝔯 p)
𝔯 {Γ} (∨-elim {Ξ} {A} {B} {C} cL cR p) = (𝔯cL₁ ⟪ Pr1ᴸ 𝔯p ⟫ᴸ) ++ (𝔯cR₁ ⟪ Pr2ᴸ 𝔯p ⟫ᴸ)
 where
  𝔯cL₁ : Tm (Γ ₊₊ dd⁺* Ξ) ((d⁺* A ⇾ d⁺* C) *)
  𝔯cL₁ = Pr1ᴸ (𝔯 cL)
  𝔯cR₁ : Tm (Γ ₊₊ dd⁺* Ξ) ((d⁺* B ⇾ d⁺* C) *)
  𝔯cR₁ = Pr1ᴸ (𝔯 cR)
  𝔯p   : Tm (Γ ₊₊ dd⁺* Ξ) ((d⁺ A ⊠ d⁺ B)*)
  𝔯p   = 𝔯 p
𝔯 {Γ} (⇒-intro {Ξ} {A} {B} p) = ⟪ Pair f g ⟫
 where
  f : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺* A ⇾ d⁺* B)
  f = Lam (𝔯 p)
  g : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺* A ⇾ d⁻ B ⇾ d⁻* A)
  g = Lam (Lam (wkn (Lam (Pr2 (𝔠 p))) · ν₀))
𝔯 (⇒-elim p q) = Pr1ᴸ (𝔯 p) ⟪ 𝔯 q ⟫ᴸ
𝔯 {Γ} (∀-intro {Ξ} {σ} {A} p) = 𝔯p'' [ 𝒄 ] -- Tm (Γ ₊₊ dd⁺* Ξ) (d⁺* A)
 where
  𝔯p : Tm (Γ ₊ σ ₊₊ dd⁺* (wknᵃ Ξ)) (d⁺* A)
  𝔯p = 𝔯 p
  𝔯p' : Tm (Γ ₊ σ ₊₊ dd⁺* Ξ) (d⁺* A)
  𝔯p' = transport (λ x → Tm (_ ₊ _ ₊₊ x) _) (sym (Lm[dd⁺*-wkn] Ξ)) 𝔯p
  𝔯p'' : Tm (Γ ₊₊ dd⁺* Ξ ₊ σ) (d⁺* A)
  𝔯p'' = wk (⊆-exch-end (dd⁺* Ξ)) 𝔯p'
𝔯 (∀-elim {A = A} p u) = L⁺* A (𝔯 p)
𝔯 (∃-intro {A = A} u p) = R⁺* A (𝔯 p) 
𝔯 {Γ} (∃-elim {Ξ} {σ} {A} {B} p) = goal -- Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ (∃ᴴ A ⇒ᴴ B) *)
 where
  Y : Ty → Set
  Y x = Tm (_ ₊ ((d⁺* A ⇾ d⁺* (wknᶠ B)) ⊠ (d⁺* A ⇾ d⁻ (wknᶠ B) ⇾ d⁻* A))
              ₊ (((d⁺* A ⇾ d⁺* B) ⊠ (d⁺* A ⇾ d⁻ B ⇾ (d⁻* A *))) *))
           (d⁺* A ⇾ (x *))
  𝔯p : Tm (Γ ₊₊ dd⁺* Ξ) (((d⁺* A ⇾ d⁺* (wknᶠ B)) ⊠ (d⁺* A ⇾ d⁻ (wknᶠ B) ⇾ d⁻* A)) *)
  𝔯p = 𝔯 p
  goal : Tm (Γ ₊₊ dd⁺* Ξ) (((d⁺* A ⇾ d⁺* B) ⊠ (d⁺* A ⇾ d⁻ B ⇾ (d⁻* A) *)) *)
  goal = LRec · Nil · Lam (Lam (Cons (Pair (transport Y (sym (Lm[wk⁺] B)) (Pr1 ν₁))
                                           (Lam (Lam ⟪ Pr2 ν₃ · ν₁ · Lwk⁻ B ν₀ ⟫))) ν₀)) · 𝔯p
𝔯 (st-eq p q) = 𝔯 p
𝔯 (st-cl {Ξ} t) = wkn₊₊ (dd⁺* Ξ) ⟪ wkε t ⟫
𝔯 (st-ap p q) = Appᴸ (𝔯 p) (𝔯 q)
𝔯 {Γ} (∀ˢᵗ-I {Ξ} {σ} {A} p) = ⟪ Lam (wkn 𝔯p₁ ⟪ ⟪ ν₀ ⟫ ⟫ᴸ) ⟫ -- : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ (∀ˢᵗ A) *)
 where
  𝔯p₁ : Tm (Γ ₊₊ dd⁺* Ξ) ((σ * ⇾ d⁺* A) *)
  𝔯p₁ = Pr1ᴸ (𝔯 p)
𝔯 {Γ} (∀ˢᵗ-E {Ξ} {σ} {A} p) = ⟪ Pair F 𝒄 ⟫ -- : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ (∀ᴴ (st ν₀ ⇒ᴴ A)) *)
 where
  𝔯p : Tm (Γ ₊₊ dd⁺* Ξ) ((σ ⇾ d⁺* A) *)
  𝔯p = 𝔯 p
  F : Tm (Γ ₊₊ dd⁺* Ξ) (σ * ⇾ d⁺* A)
  F = LRec · Nil · Lam (Lam (wkn² 𝔯p ⟪ ν₁ ⟫ᴸ ++ ν₀))
𝔯 {Γ} (∃ˢᵗ-I {Ξ} {σ} {A} p) = 𝔯 p -- : Tm (Γ ₊₊ dd⁺* Ξ) ((σ ⊠ d⁺ A) *)
𝔯 {Γ} (∃ˢᵗ-E {Ξ} {σ} {A} p) = 𝔯 p -- : Tm (Γ ₊₊ dd⁺* Ξ) ((σ ⊠ d⁺ A) *)
𝔯 (IR ι p q) = 𝒄
𝔯 {Γ} (IRˢᵗ {Ξ} {A} p q) = ⟪ Rec · a · f ⟫
 where
  𝔯p : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ (A [ Zero ]ᶠ) *)
  𝔯p = 𝔯 p
  a : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ A *)
  a = R⁺* A 𝔯p
  𝔯q₁ : Tm (Γ ₊₊ dd⁺* Ξ) (Ⓝ ⇾ d⁺ A * ⇾ d⁺ (A [s]ᶠ) *)
  𝔯q₁ = Lam (Lam (Pr1ᴸ (wkn² (𝔯 q) ⟪ ν₁ ⟫ᴸ) ⟪ ν₀ ⟫ᴸ))
  f : Tm (Γ ₊₊ dd⁺* Ξ) (Ⓝ ⇾ d⁺ A * ⇾ d⁺ A *)
  f = transport (λ x → Tm _ (Ⓝ ⇾ d⁺ A * ⇾ x *)) (sym(Lm[s]⁺ A)) 𝔯q₁
𝔯 {Γ} (I {σ} {τ} {φ} _) = ⟪ Pair U Y ⟫
 where
  U : Tm Γ ((((σ *) ⇾ ((((① *) ⇾ (d⁺ (wkn₂ᶠ φ) *)) ⊠ ((① *) ⇾ d⁻ (wkn₂ᶠ φ) ⇾ (① *)))*))*)
            ⇾ ((σ ⇾ (d⁺ φ *)) *))
  U = Lam Nil
  Y : Tm Γ ((((σ *) ⇾ ((((① *) ⇾ (d⁺ (wkn₂ᶠ φ) *)) ⊠ ((① *) ⇾ d⁻ (wkn₂ᶠ φ) ⇾ (① *)))*))*)
            ⇾ ((σ ⊠ d⁻ φ) *)
            ⇾ (((σ *) ⊠ (((① *) ⊠ d⁻ (wkn₂ᶠ φ)) *))*))
  Y = Lam (Lam ⟪ Pair (Pr1ᴸ ν₀)
                      (LRec · Nil · Lam (Lam (Cons (Pair ⟪ ✹ ⟫ (Lwk⁻ φ ν₁)) ν₀)) · (Pr2ᴸ ν₀)) ⟫)
𝔯 {Γ} (NCR {σ} {τ} {Ψ}) = ⟪ Pair U Y ⟫
 where
  U : Tm Γ (((σ ⊠ d⁺ Ψ) *) ⇾ (((σ *) ⊠ ① ⊠ d⁺ (wkn₂ᶠ Ψ))*))
  U = Lam (LRec · Nil · Lam (Lam (Cons (Pair (Pr1ᴸ ν₂) (Pair ✹ (Lwk⁺ Ψ (Pr2 ν₁)))) ν₀)) · ν₀)
  Y : Tm Γ (((σ ⊠ d⁺ Ψ) *) ⇾ (((① ⊠ d⁻ (wkn₂ᶠ Ψ))*)*) ⇾ ((d⁻ Ψ *)*))
  Y = Lam (LRec · Nil · Lam (Lam (Cons (Rwk⁻* Ψ (Pr2ᴸ ν₁)) ν₀)))
𝔯 {Γ} (HAC {σ} {τ} {Φ}) = ⟪ Pair U Y ⟫
 where
  U : Tm Γ (((σ ⇾ ((τ ⊠ d⁺ Φ) *)) *) ⇾ (((σ ⇾ (τ *)) ⊠ (σ ⇾ ((① ⊠ d⁺ (wkn₂ᶠ Φ)) *))) *))
  U = Lam ⟪ Pair (Lam (Pr1ᴸ (ν₁ ⟪ ν₀ ⟫ᴸ)))
                 (Lam (LRec · Nil · Lam (Lam (Cons (Pair ✹ (Lwk⁺ Φ (Pr2 ν₁))) ν₀)) · (ν₁ ⟪ ν₀ ⟫ᴸ))) ⟫
  Y : Tm Γ (((σ ⇾ ((τ ⊠ d⁺ Φ) *)) *) ⇾ ((σ ⊠ ((① ⊠ d⁻ (wkn₂ᶠ Φ)) *)) *) ⇾ ((σ ⊠ (d⁻ Φ *)) *))
  Y = Lam (LRec · Nil · Lam (Lam (Cons (Pair (Pr1 ν₁) (Rwk⁻* Φ (Pr2ᴸ (Pr2 ν₁)))) ν₀)))
𝔯 {Γ} (HGMPˢᵗ {σ} {φ} {ψ} _ _) = ⟪ Pair U Y ⟫
 where
  U : Tm Γ ((((((σ ⇾ (d⁺ φ *))*) ⇾ (d⁺ ψ *)) ⊠ (((σ ⇾ (d⁺ φ *)) *) ⇾ d⁻ ψ ⇾ ((σ ⊠ d⁻ φ) *)))*)
            ⇾ ((σ * ⊠ ((((① * ⇾ (d⁺ (wkn₁ᶠ φ) *)) ⊠ (① * ⇾ d⁻ (wkn₁ᶠ φ) ⇾ ① *))*) ⇾ (d⁺ (wknᶠ ψ) *))
                    ⊠ ((((① * ⇾ (d⁺ (wkn₁ᶠ φ) *)) ⊠ (① * ⇾ d⁻ (wkn₁ᶠ φ) ⇾ ① *))*)
                       ⇾ d⁻ (wknᶠ ψ) ⇾ ((① * ⊠ d⁻ (wkn₁ᶠ φ))*)))*))
  U = Lam ⟪ Pair (Pr1ᴸ (Pr2ᴸ ν₀ ⟪ 𝒄 ₓ 𝒄 ⟫ᴸ)) 𝒄 ⟫
  Y : Tm Γ ((((((σ ⇾ (d⁺ φ *))*) ⇾ (d⁺ ψ *)) ⊠ (((σ ⇾ (d⁺ φ *))*) ⇾ d⁻ ψ ⇾ ((σ ⊠ d⁻ φ) *)))*)
            ⇾ (((((① * ⇾ (d⁺ (wkn₁ᶠ φ) *)) ⊠ (① * ⇾ d⁻ (wkn₁ᶠ φ) ⇾ ① *))*) ⊠ d⁻ (wknᶠ ψ))*)
            ⇾ ((((σ ⇾ (d⁺ φ *)) *) ⊠ d⁻ ψ) *))
  Y = Lam (Lam ⟪ 𝒄 ⟫)
𝔯 {Γ} (HIP-∀ˢᵗ {σ} {τ} {φ} {Ψ} _) = ⟪ Pair U Y ⟫
 where
  X : Cxt
  X = _ -- to please the type checker (actually it can infer the value X)
  U : Tm Γ ((((((σ ⇾ (d⁺ φ *))*) ⇾ ((τ ⊠ d⁺ Ψ)*)) ⊠ (((σ ⇾ (d⁺ φ *))*) ⇾ (d⁻ Ψ *) ⇾ ((σ ⊠ d⁻ φ)*)))*)
            ⇾ ((τ * ⊠ (((σ ⇾ (d⁺ (wkn₁ᶠ φ) *))*) ⇾ ((① ⊠ d⁺ (wkn₁ᶠ Ψ))*))
                    ⊠ (((σ ⇾ (d⁺ (wkn₁ᶠ φ) *))*) ⇾ ((① ⊠ d⁻ (wkn₁ᶠ Ψ))*) ⇾ ((σ ⊠ d⁻ (wkn₁ᶠ φ)) *)))*))
  U = Lam ⟪ Pair (Pr1ᴸ (Pr1ᴸ ν₀ ⟪ 𝒄 ⟫ᴸ))
                 (Pair (Lam (LRec · Nil · Lam (Lam (Cons (Pair ✹ (Lwk⁺ Ψ ν₁)) ν₀)) · Pr2ᴸ (Pr1ᴸ ν₁ ⟪ 𝒄 ⟫ᴸ)))
                       (Lam (Lam (transport (λ x → Tm X ((σ ⊠ x)*)) (Lm[wk⁻] φ) (Pr2ᴸ ν₂ ⟪ 𝒄 ₓ 𝒄 ⟫ᴸ))))) ⟫
  Y : Tm Γ ((((((σ ⇾ (d⁺ φ *))*) ⇾ ((τ ⊠ d⁺ Ψ)*)) ⊠ (((σ ⇾ (d⁺ φ *))*) ⇾ (d⁻ Ψ *) ⇾ ((σ ⊠ d⁻ φ) *)))*)
            ⇾ ((((σ ⇾ (d⁺ (wkn₁ᶠ φ) *))*) ⊠ ((① ⊠ d⁻ (wkn₁ᶠ Ψ)) *))*)
            ⇾ ((((σ ⇾ (d⁺ φ *))*) ⊠ (d⁻ Ψ *)) *))
  Y = Lam (LRec · Nil · Lam (Lam (Cons (Pair 𝒄 (Rwk⁻* Ψ (Pr2ᴸ (Pr2 ν₁)))) ν₀)))
𝔯 (st-succ p) = Mapᴸ (Lam (Succ ν₀)) (𝔯 p)
𝔯 _ = 𝒄 -- All the additional internal axioms has no computational contents

𝔠 Id      = Pair ✹ ⟪ ν₀ ⟫
𝔠 (Wkn p) = Pair (wk (⊆-ext (ε ₊ _)) (𝔠 p)) 𝒄
𝔠 {Γ} (Swap {Ξ} Ζ {A} {B} {C} p) = Pair⁻ _ Ζ (Pair (Pair u b) a) v
            -- Tms (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (dd⁻* (Ξ ₊ B ₊ A ₊₊ Ζ))
 where
  𝔠p  : Tms (Γ ₊₊ dd⁺* (Ξ ₊ A ₊ B ₊₊ Ζ) ₊ d⁻ C) (dd⁻* (Ξ ₊ A ₊ B ₊₊ Ζ))
  𝔠p  = 𝔠 p
  𝔠p' : Tms (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (dd⁻* (Ξ ₊ A ₊ B ₊₊ Ζ))
  𝔠p' = wkn (swap⁺ Ζ (Lam 𝔠p)) · ν₀
  𝔠p'₁ : Tms (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (dd⁻* (Ξ ₊ A ₊ B))
  𝔠p'₁ = pr₁⁻ _ Ζ 𝔠p'
  u : Tms (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (dd⁻* Ξ)
  u = Pr1 (Pr1 𝔠p'₁)
  a : Tm  (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (d⁻* A)
  a = Pr2 (Pr1 𝔠p'₁)
  b : Tm  (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (d⁻* B)
  b = Pr2 𝔠p'₁
  v : Tms (Γ ₊₊ dd⁺* (Ξ ₊ B ₊ A ₊₊ Ζ) ₊ d⁻ C) (dd⁻* Ζ)
  v = pr₂⁻ _ Ζ 𝔠p'
𝔠 RecZer  = ✹
𝔠 RecSuc  = ✹
𝔠 LRecNil = ✹
𝔠 LRecCon = ✹
𝔠 β-eq    = ✹
𝔠 η-eq    = ✹
𝔠 βˣ-eq₁  = ✹
𝔠 βˣ-eq₂  = ✹
𝔠 ηˣ-eq   = ✹
𝔠  Refl       = ✹
𝔠 (Sym p)     = 𝔠 p
𝔠 (Trans p q) = 𝔠 p ++ᵐˢ⁻ 𝔠 q
𝔠 (ApF p)     = 𝔠 p
𝔠 (FunExt p) = 𝔠 p
𝔠  ≤-Zero    = 𝒄
𝔠 (≤-Succ p) = 𝔠 p
𝔠  ∈-zero    = ✹
𝔠 (∈-succ p) = 𝔠 p
𝔠 (⊥-elim p) = wkn (𝔠 p [ 𝒄 ])
𝔠 {Γ} (∧-intro {Ξ} {A} {B} p q) = w𝔠p ++ᵐˢ⁻ w𝔠q
 where
  w𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (A ∧ᴴ B)) (dd⁻* Ξ)
  w𝔠p = wkn (Lam (𝔠 p)) · Pr1 ν₀
  w𝔠q : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (A ∧ᴴ B)) (dd⁻* Ξ)
  w𝔠q = wkn (Lam (𝔠 q)) · Pr2 ν₀
𝔠 (∧-elim₁ p) = wkn (Lam (𝔠 p)) · Pair ν₀ 𝒄
           -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
      --  𝔠 p : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (A ∧ᴴ B)) (dd⁻* Ξ)
𝔠 (∧-elim₂ p) = wkn (Lam (𝔠 p)) · Pair 𝒄 ν₀
           -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ B) (dd⁻* Ξ)
𝔠 (∨-inl p) = wkn (Lam (𝔠 p)) · Pr1 ν₀
𝔠 (∨-inr p) = wkn (Lam (𝔠 p)) · Pr2 ν₀
𝔠 {Γ} (∨-elim {Ξ} {A} {B} {C} cL cR p) = u ++ᵐˢ⁻ v ++ᵐˢ⁻ w
 where
  𝔯p : Tm (Γ ₊₊ dd⁺* Ξ) ((d⁺ A ⊠ d⁺ B) *)
  𝔯p = 𝔯 p
  𝔯cL₂ : Tm (Γ ₊₊ dd⁺* Ξ) (((d⁺ A *) ⇾ d⁻ C ⇾ (d⁻ A *)) *)
  𝔯cL₂ = Pr2ᴸ (𝔯 cL)
  a : Tm (Γ ₊₊ dd⁺* Ξ ₊ d⁻ C) (d⁻* A)
  a = wkn 𝔯cL₂ ⟪ wkn (Pr1ᴸ 𝔯p) ₓ ν₀ ⟫ᴸ
  𝔯cR₂ : Tm (Γ ₊₊ dd⁺* Ξ) (((d⁺ B *) ⇾ d⁻ C ⇾ (d⁻ B *)) *)
  𝔯cR₂ = Pr2ᴸ (𝔯 cR)
  b : Tm (Γ ₊₊ dd⁺* Ξ ₊ d⁻ C) (d⁻* B)
  b = wkn 𝔯cR₂ ⟪ wkn (Pr2ᴸ 𝔯p) ₓ ν₀ ⟫ᴸ
  ab : Tm (Γ ₊₊ dd⁺* Ξ ₊ d⁻ C) ((d⁻ A ⊠ d⁻ B)*)
  ab = Pairᴸ a b
  𝔠L : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ d⁻ C)) (dd⁻* Ξ)
  𝔠L = 𝔠 cL
  𝔠R : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* B ⊠ d⁻ C)) (dd⁻* Ξ)
  𝔠R = 𝔠 cR
  𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁻ A ⊠ d⁻ B)) (dd⁻* Ξ)
  𝔠p = 𝔠 p
  u v w : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ C) (dd⁻* Ξ)
  u = wkn (Lam 𝔠L) · Pair (wkn (Pr1ᴸ 𝔯p)) ν₀
  v = wkn (Lam 𝔠R) · Pair (wkn (Pr2ᴸ 𝔯p)) ν₀
  w = Appᵐˢ⁻ (wkn (Lam 𝔠p)) ab
𝔠 {Γ} (⇒-intro {Ξ} {A} {B} p) = wkn (Lam (Lam (Pr1 (𝔠 p)))) · Pr1 ν₀ · Pr2 ν₀
           -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ d⁻ B)) (dd⁻* Ξ)
        -- 𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁺* A ₊ d⁻ B) (dd⁻* Ξ ₊ d⁻* A)
𝔠 {Γ} (⇒-elim {Ξ} {A} {B} p q) = u ++ᵐˢ⁻ v -- CHECK!
                            -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ B) (dd⁻* Ξ)
 where
  𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ d⁻ B)) (dd⁻* Ξ)
  𝔠p = 𝔠 p
  𝔯q : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺* A)
  𝔯q = 𝔯 q
  u : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ B) (dd⁻* Ξ)
  u = wkn (Lam 𝔠p) · (Pair (wkn 𝔯q) ν₀)
  𝔠q : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
  𝔠q = 𝔠 q
  𝔯p₂ : Tm (Γ ₊₊ dd⁺* Ξ) ((d⁺* A ⇾ d⁻ B ⇾ d⁻* A)*)
  𝔯p₂ = Pr2ᴸ (𝔯 p)
  a : Tm (Γ ₊₊ dd⁺* Ξ ₊ d⁻ B) (d⁻* A)
  a = wkn 𝔯p₂ ⟪ wkn 𝔯q ₓ ν₀ ⟫ᴸ
  v : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ B) (dd⁻* Ξ)
  v = Appᵐˢ⁻ (wkn (Lam 𝔠q)) a
𝔠 {Γ} (∀-intro {Ξ} {σ} {A} p) = 𝔠p'' -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ) -- CHECK!
 where
  𝔠p : Tms (Γ ₊ σ ₊₊ dd⁺* (wknᵃ Ξ) ₊ d⁻ A) (dd⁻* (wknᵃ Ξ))
  𝔠p = 𝔠 p
  𝔠p' : Tms (Γ ₊₊ dd⁺* (wknᵃ Ξ) ₊ d⁻ A) (dd⁻* (wknᵃ Ξ))
  𝔠p' = (wk (⊆-exch-end (dd⁺* (wknᵃ Ξ) ₊ d⁻ A)) 𝔠p) [ 𝒄 ]
  𝔠p'' : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
  𝔠p'' = transport² (λ x y → Tms (Γ ₊₊ x ₊ d⁻ A) y) (sym (Lm[dd⁺*-wkn] Ξ)) (sym (Lm[dd⁻*-wkn] Ξ)) 𝔠p'
𝔠 {Γ} (∀-elim {Ξ} {σ} {A} p u) = transport (λ x → Tms (Γ ₊₊ dd⁺* Ξ ₊ x) (dd⁻* Ξ)) (Lm[d⁻] A) (𝔠 p)
                            -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (A [ u ]ᶠ)) (dd⁻* Ξ)
                        --  𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
𝔠 {Γ} (∃-intro {Ξ} {σ} {A} u p) = goal -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (∃ᴴ A)) (dd⁻* Ξ) -- CHECK!
 where
  𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (A [ u ]ᶠ)) (dd⁻* Ξ)
  𝔠p = 𝔠 p
  𝔠p' : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
  𝔠p' = transport (λ x → Tms (Γ ₊₊ dd⁺* Ξ ₊ x) (dd⁻* Ξ)) (sym (Lm[d⁻] A)) 𝔠p
  goal : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻* A) (dd⁻* Ξ)
  goal = Appᵐˢ⁻ (wkn (Lam 𝔠p')) ν₀
𝔠 {Γ} (∃-elim {Ξ} {σ} {A} {B} p) = goal -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ d⁻ B)) (dd⁻* Ξ)
 where
  𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ d⁻ (wknᶠ B))) (dd⁻* Ξ)
  𝔠p = 𝔠 p
  goal : Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ d⁻ B)) (dd⁻* Ξ)
  goal = transport (λ x → Tms (Γ ₊₊ dd⁺* Ξ ₊ (d⁺* A ⊠ x)) (dd⁻* Ξ)) (sym (Lm[wk⁻] B)) 𝔠p
𝔠 (st-eq p q) = 𝔠 p ++ᵐˢ⁻ 𝔠 q
𝔠 (st-cl t)   = 𝒄
𝔠 (st-ap p q) = 𝔠 p ++ᵐˢ⁻ 𝔠 q
𝔠 (∀ˢᵗ-I p) = (wkn (Lam (𝔠 p))) · (Pair ⟪ Pr1 ν₀ ⟫ (Pr2 ν₀))
         -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ (σ ⊠ d⁻ A)) (dd⁻* Ξ)
     -- 𝔠 p : Tms (Γ ₊₊ dd⁺* Ξ ₊ (σ * ⊠ d⁻ A)) (dd⁻* Ξ)
𝔠 {Γ} (∀ˢᵗ-E {Ξ} {σ} {A} p) = goal
         -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ (σ * ⊠ d⁻ A)) (dd⁻* Ξ)
 where
  𝔠p : Tms (Γ ₊₊ dd⁺* Ξ ₊ (σ ⊠ d⁻ A)) (dd⁻* Ξ)
  𝔠p = 𝔠 p
  goal : Tms (Γ ₊₊ dd⁺* Ξ ₊ (σ * ⊠ d⁻ A)) (dd⁻* Ξ)
  goal = LRec · Nilᵐˢ⁻ · Lam (Lam ((wkn³ (Lam 𝔠p) · Pair ν₁ (Pr2 ν₂)) ++ᵐˢ⁻ ν₀)) · (Pr1 ν₀)
𝔠 (∃ˢᵗ-I p) = wkn (Lam (𝔠 p)) · Pairʳ ✹ ν₀
         -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻* A) (dd⁻* Ξ)
     -- 𝔠 p : Tms (Γ ₊₊ dd⁺* Ξ ₊ ((① ⊠ d⁻ A)*)) (dd⁻* Ξ)
𝔠 (∃ˢᵗ-E p) = wkn (Lam (𝔠 p)) · Pr2ᴸ ν₀
         -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (∃ᴴ (st ν₀ ∧ᴴ A))) (dd⁻* Ξ)
     -- 𝔠 p : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻* A) (dd⁻* Ξ)
𝔠 (IR _ p q) = 𝒄
𝔠 {Γ} (IRˢᵗ {Ξ} {A} p q) = Rec · u · h · Pr1 ν₀
                      -- : Tms (Γ ₊₊ dd⁺* Ξ ₊ (Ⓝ ⊠ d⁻ A)) (dd⁻* Ξ)
 where
  𝔠p  : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ (A [ Zero ]ᶠ)) (dd⁻* Ξ)
  𝔠p  = 𝔠 p
  𝔠p' : Tms (Γ ₊₊ dd⁺* Ξ ₊ d⁻ A) (dd⁻* Ξ)
  𝔠p' = transport (λ x → Tms (Γ ₊₊ dd⁺* Ξ ₊ x) (dd⁻* Ξ)) (sym (Lm[d⁻] A)) 𝔠p
  𝔠q  : Tms (Γ ₊₊ dd⁺* Ξ ₊ (Ⓝ ⊠ d⁺* A ⊠ d⁻ (A [s]ᶠ))) (dd⁻* Ξ)
  𝔠q  = 𝔠 q
  𝔠q' : Tms (Γ ₊₊ dd⁺* Ξ ₊ (Ⓝ ⊠ d⁺* A ⊠ d⁻ A)) (dd⁻* Ξ)
  𝔠q' = transport (λ x → Tms (Γ ₊₊ dd⁺* Ξ ₊ (Ⓝ ⊠ d⁺* A ⊠ x)) (dd⁻* Ξ)) (sym (Lm[s]⁻ A)) 𝔠q
  𝔯q : Tm (Γ ₊₊ dd⁺* Ξ) ((Ⓝ ⇾ ((((d⁺ A *) ⇾ (d⁺ (A [s]ᶠ) *)) ⊠ ((d⁺ A *) ⇾ d⁻ (A [s]ᶠ) ⇾ (d⁻ A *))) *)) *)
  𝔯q = 𝔯 q
  𝔯p : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ (A [ Zero ]ᶠ) *)
  𝔯p = 𝔯 p
  a : Tm (Γ ₊₊ dd⁺* Ξ) (d⁺ A *)
  a = R⁺* A 𝔯p
  𝔯q₁ : Tm (Γ ₊₊ dd⁺* Ξ) (Ⓝ ⇾ d⁺* A ⇾ d⁺* (A [s]ᶠ))
  𝔯q₁ = Lam (Lam (Pr1ᴸ (wkn² 𝔯q ⟪ ν₁ ⟫ᴸ) ⟪ ν₀ ⟫ᴸ))
  f : Tm (Γ ₊₊ dd⁺* Ξ) (Ⓝ ⇾ d⁺* A ⇾ d⁺* A)
  f = transport (λ x → Tm _ (Ⓝ ⇾ d⁺* A ⇾ x *)) (sym(Lm[s]⁺ A)) 𝔯q₁
  g : Tm (Γ ₊₊ dd⁺* Ξ) (Ⓝ ⇾ d⁺* A)
  g = Rec · a · f
  u : Tm (Γ ₊₊ dd⁺* Ξ ₊ (Ⓝ ⊠ d⁻ A)) (Π (dd⁻* Ξ))
  u = wkn (Lam 𝔠p') · Pr2 ν₀
  h : Tm (Γ ₊₊ dd⁺* Ξ ₊ (Ⓝ ⊠ d⁻ A)) (Ⓝ ⇾ Π (dd⁻* Ξ) ⇾ Π (dd⁻* Ξ))
  h = Lam (Lam (wkn³ (Lam 𝔠q') · Pair ν₁ (Pair (wkn³ g · ν₁) (Pr2 ν₂))))
𝔠 (I _)        = ✹
𝔠  NCR         = ✹
𝔠  HAC         = ✹
𝔠 (HGMPˢᵗ _ _) = ✹
𝔠 (HIP-∀ˢᵗ _)  = ✹
𝔠 (st-succ p)  = 𝔠 p
𝔠 _ = 𝒄

\end{code}

By embedding system T into Agda, we use the following to extract an
Agda term from a given proof in system H.

\begin{code}

extract : {Φ : Fml ε} → Prf ε Φ → ⟦ d⁺* Φ ⟧ʸ
extract p = ⟦ 𝔯 p ⟧ᵐ ⋆

open import Simp

simpExtract : {Φ : Fml ε} → Prf ε Φ → ⟦ simpᵀ (d⁺* Φ) ⟧ʸ 
simpExtract {Φ} p = simpᴹ (d⁺* Φ) (extract p)

\end{code}