H

Chuangjie Xu, July 2016

------------------------------------
   Nonstandard Heyting arithmetic
------------------------------------

We define 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.

using some inductive datatypes.  Instead of writing a compiler for its
term language T, we embed it into Agda by defining an interpretation
function ⟦_⟧.  Then, after extracting a T-term from a proof in H, we
use ⟦_⟧ to get a runnable Agda function/program.

We disable the termination checker because it doesn't believe that the
substitution functions terminate.  We keep the current definition of
substitution, because it's easier to work with, though we have at least
two ways of defining substitution to please the termination checker.

\begin{code}

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

module H where

open import Preliminaries
open import DataTypes

\end{code}

------------------------------------
          Gödel's system T
------------------------------------

with natural numbers and finite lists

We inductively define a datatype Tm for well-typed lambda terms.  In
particular, we use de Bruijn indices to ensure that any variable
occurrence always points to a variable in a given context.

\begin{code}

infixr 15 _⊠_
infixr 10 _⇾_

data Ty : Set where
 ① ② Ⓝ : Ty
 _* : Ty → Ty
 _⊠_ _⇾_ : Ty → Ty → Ty

Cxt : Set
Cxt = List Ty

infixl 20 _·_

data Tm (Γ : Cxt) : Ty → Set where
 Var  : {A : Ty} → ∥ A ∈ Γ ∥ → Tm Γ A
 ✹    : Tm Γ ①
 TT   : Tm Γ ②
 FF   : Tm Γ ②
 IF   : {A : Ty} → Tm Γ (A ⇾ A ⇾ ② ⇾ A)
 Zero : Tm Γ Ⓝ
 Succ : Tm Γ Ⓝ → Tm Γ Ⓝ
 Rec  : {A : Ty}   → Tm Γ (A ⇾ (Ⓝ ⇾ A ⇾ A) ⇾ Ⓝ ⇾ A)
 Nil  : {A : Ty}   → Tm Γ (A *)
 Cons : {A : Ty}   → Tm Γ A → Tm Γ (A *) → Tm Γ (A *)
 LRec : {A B : Ty} → Tm Γ (A ⇾ (B ⇾ A ⇾ A) ⇾ B * ⇾ A)
 Pair : {A B : Ty} → Tm Γ A → Tm Γ B → Tm Γ (A ⊠ B)
 Pr1  : {A B : Ty} → Tm Γ (A ⊠ B) → Tm Γ A
 Pr2  : {A B : Ty} → Tm Γ (A ⊠ B) → Tm Γ B
 Lam  : {A B : Ty} → Tm (Γ ₊ A) B → Tm Γ (A ⇾ B)
 _·_  : {A B : Ty} → Tm Γ (A ⇾ B) → Tm Γ A → Tm Γ B

ν₀ : {Γ : Cxt} {σ : Ty} → Tm (Γ ₊ σ) σ
ν₀ = Var zero

ν₁ : {Γ : Cxt} {σ σ₁ : Ty} → Tm (Γ ₊ σ ₊ σ₁) σ
ν₁ = Var (succ zero)

ν₂ : {Γ : Cxt} {σ σ₁ σ₂ : Ty} → Tm (Γ ₊ σ ₊ σ₁ ₊ σ₂) σ
ν₂ = Var (succ (succ zero))

*⁼ : {σ σ' : Ty} → σ ≡ σ' → σ * ≡ σ' *
*⁼ refl = refl

⊠⁼ : {σ σ' τ τ' : Ty} → σ ≡ σ' → τ ≡ τ' → σ ⊠ τ ≡ σ' ⊠ τ'
⊠⁼ refl refl = refl

⇾⁼ : {σ σ' τ τ' : Ty} → σ ≡ σ' → τ ≡ τ' → σ ⇾ τ ≡ σ' ⇾ τ'
⇾⁼ refl refl = refl

\end{code}

Embed T into Agda

\begin{code}

⟦_⟧ʸ : Ty → Set
⟦ ① ⟧ʸ    = 𝟙
⟦ ② ⟧ʸ    = 𝟚
⟦ Ⓝ ⟧ʸ    = ℕ
⟦ σ * ⟧ʸ   = List ⟦ σ ⟧ʸ
⟦ σ ⊠ τ ⟧ʸ = ⟦ σ ⟧ʸ × ⟦ τ ⟧ʸ
⟦ σ ⇾ τ ⟧ʸ = ⟦ σ ⟧ʸ → ⟦ τ ⟧ʸ

⟦_⟧ˣ : Cxt → Set
⟦ ε ⟧ˣ     = 𝟙
⟦ Γ ₊ σ ⟧ˣ = ⟦ Γ ⟧ˣ × ⟦ σ ⟧ʸ

⟦_⟧ᵐ : {Γ : Cxt} {σ : Ty} → Tm Γ σ → ⟦ Γ ⟧ˣ → ⟦ σ ⟧ʸ
⟦ Var zero ⟧ᵐ     (ρ , a) = a
⟦ Var (succ i) ⟧ᵐ (ρ , a) = ⟦ Var i ⟧ᵐ ρ
⟦ ✹ ⟧ᵐ ρ = ⋆
⟦ TT ⟧ᵐ ρ = ⊤
⟦ FF ⟧ᵐ ρ = ⊥
⟦ IF ⟧ᵐ ρ = if
⟦ Zero ⟧ᵐ   ρ = zero
⟦ Succ t ⟧ᵐ ρ = succ (⟦ t ⟧ᵐ ρ)
⟦ Rec ⟧ᵐ    ρ = rec
⟦ Nil ⟧ᵐ       ρ = ε
⟦ Cons x xs ⟧ᵐ ρ = ⟦ xs ⟧ᵐ ρ ₊ ⟦ x ⟧ᵐ ρ
⟦ LRec ⟧ᵐ      ρ = recᴸ
⟦ Pair a b ⟧ᵐ  ρ = ⟦ a ⟧ᵐ ρ , ⟦ b ⟧ᵐ ρ
⟦ Pr1 t ⟧ᵐ     ρ = pr₁ (⟦ t ⟧ᵐ ρ)
⟦ Pr2 t ⟧ᵐ     ρ = pr₂ (⟦ t ⟧ᵐ ρ)
⟦ Lam t ⟧ᵐ ρ = λ x → ⟦ t ⟧ᵐ (ρ , x)
⟦ f · a ⟧ᵐ ρ = ⟦ f ⟧ᵐ ρ (⟦ a ⟧ᵐ ρ)

\end{code}

----------------------------
          System H
----------------------------

Formulas

\begin{code}

infix  10 _=ᴴ_
infix  10 _≤ᴴ_
infix  10 _∈ᴴ_
infixr 9  _∧ᴴ_
infixr 9  _∨ᴴ_
infixr 8  _⇒ᴴ_

data Fml (Γ : Cxt) : Set where
 st             : {σ : Ty} → Tm Γ σ → Fml Γ
 _=ᴴ_           : {σ : Ty} → Tm Γ σ → Tm Γ σ → Fml Γ
 _≤ᴴ_           :            Tm Γ Ⓝ → Tm Γ Ⓝ → Fml Γ
 _∈ᴴ_           : {σ : Ty} → Tm Γ σ → Tm Γ (σ *) → Fml Γ
 _∧ᴴ_ _∨ᴴ_ _⇒ᴴ_ : Fml Γ → Fml Γ → Fml Γ
 ∀ᴴ ∃ᴴ ∀ˢᵗ ∃ˢᵗ  : {σ : Ty} → Fml (Γ ₊ σ) → Fml Γ
 Even           : Tm Γ Ⓝ → Fml Γ

⊥ᴴ : {Γ : Cxt} → Fml Γ
⊥ᴴ = Zero =ᴴ Succ Zero

data internal {Γ : Cxt} : Fml Γ → Set where
 int-= : {σ : Ty} {a b : Tm Γ σ}                 → internal (a =ᴴ b)
 int-≤ : {n m : Tm Γ Ⓝ}                         → internal (n ≤ᴴ m)
 int-∈ : {σ : Ty} {a : Tm Γ σ} {w : Tm Γ (σ *)}  → internal (a ∈ᴴ w)
 int-∧ : {A B : Fml Γ} → internal A → internal B → internal (A ∧ᴴ B)
 int-∨ : {A B : Fml Γ} → internal A → internal B → internal (A ∨ᴴ B)
 int-⇒ : {A B : Fml Γ} → internal A → internal B → internal (A ⇒ᴴ B)
 int-∀ : {σ : Ty} {A : Fml (Γ ₊ σ)} → internal A → internal (∀ᴴ A)
 int-∃ : {σ : Ty} {A : Fml (Γ ₊ σ)} → internal A → internal (∃ᴴ A)
 int-E : {n : Tm Γ Ⓝ} → internal (Even n)

\end{code}

Some auxiliaries for defining proofs which are defined later

\begin{code}

_[_]  : {Γ : Cxt} {A C : Ty} → Tm (Γ ₊ A) C → Tm Γ A → Tm Γ C

_[_]ᶠ : {Γ : Cxt} {σ : Ty}   → Fml (Γ ₊ σ)  → Tm Γ σ → Fml Γ

wkn   : {Γ : Cxt} {A X : Ty}   → Tm Γ A          → Tm (Γ ₊ X) A

wkε   : {Γ : Cxt} {A : Ty}     → Tm ε A          → Tm Γ A

wknᶠ  : {Γ : Cxt} {σ : Ty}     → Fml Γ           → Fml (Γ ₊ σ)

wkn₁ᶠ : {Γ : Cxt} {σ τ : Ty}   → Fml (Γ ₊ σ)     → Fml (Γ ₊ τ ₊ σ)

wkn₂ᶠ : {Γ : Cxt} {σ τ ρ : Ty} → Fml (Γ ₊ σ ₊ τ) → Fml (Γ ₊ ρ ₊ σ ₊ τ)

wkn²ᶠ : {Γ : Cxt} {σ τ : Ty}   → Fml Γ           → Fml (Γ ₊ σ ₊ τ)

_[s]ᶠ : {Γ : Cxt}              → Fml (Γ ₊ Ⓝ)    → Fml (Γ ₊ Ⓝ)

\end{code}

Proofs, via natural deduction

An element of type Prf Ξ A can be understood as a proof of A under the
assumption Ξ.

\begin{code}

Asmpt : Cxt → Set
Asmpt Γ = List (Fml Γ)

wknᵃ : {Γ : Cxt} {σ : Ty} → Asmpt Γ → Asmpt (Γ ₊ σ)
wknᵃ  ε      = ε
wknᵃ (Ξ ₊ A) = wknᵃ Ξ ₊ wknᶠ A


data Prf {Γ : Cxt} : Asmpt Γ → Fml Γ → Set where
--------- Rules of sequent calculi ---------
 Id      : {A : Fml Γ}
         → Prf (ε ₊ A) A
 Wkn     : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ B → Prf (Ξ ₊ A) B
 Swap    : {Ξ : Asmpt Γ} (Ζ : Asmpt Γ) {A B C : Fml Γ}
         → Prf (Ξ ₊ A ₊ B ₊₊ Ζ) C → Prf (Ξ ₊ B ₊ A ₊₊ Ζ) C
--------------------------------------------
--------- Computational rule of Ⓝ ---------
 RecZer  : {σ : Ty} {a : Tm Γ σ} {f : Tm Γ (Ⓝ ⇾ σ ⇾ σ)}
         → Prf ε (Rec · a · f · Zero =ᴴ a)
 RecSuc  : {σ : Ty} {a : Tm Γ σ} {f : Tm Γ (Ⓝ ⇾ σ ⇾ σ)} {n : Tm Γ Ⓝ}
         → Prf ε (Rec · a · f · Succ n =ᴴ f · n · (Rec · a · f · n))
--------------------------------------------
--------- Computational rule of * ----------
 LRecNil : {σ τ : Ty} {a : Tm Γ σ} {f : Tm Γ (τ ⇾ σ ⇾ σ)}
         → Prf ε (LRec · a · f · Nil =ᴴ a)
 LRecCon : {σ τ : Ty} {a : Tm Γ σ} {f : Tm Γ (τ ⇾ σ ⇾ σ)} {x : Tm Γ τ} {xs : Tm Γ (τ *)}
         → Prf ε (LRec · a · f · (Cons x xs) =ᴴ f · x · (LRec · a · f · xs))
--------------------------------------------
--------- Computational rule of ⇾ ----------
 β-eq    : {σ τ : Ty} {t : Tm (Γ ₊ σ) τ} {u : Tm Γ σ}
         → Prf ε (Lam t · u =ᴴ t [ u ])
 η-eq    : {σ τ : Ty} {f : Tm Γ (σ ⇾ τ)}
         → Prf ε (Lam (wkn f · Var zero) =ᴴ f)
--------------------------------------------
--------- Computational rule of ⊠ ----------
 βˣ-eq₁  : {σ τ : Ty} {a : Tm Γ σ} {b : Tm Γ τ}
         → Prf ε (Pr1 (Pair a b) =ᴴ a)
 βˣ-eq₂  : {σ τ : Ty} {a : Tm Γ σ} {b : Tm Γ τ}
         → Prf ε (Pr2 (Pair a b) =ᴴ b)
 ηˣ-eq   : {σ τ : Ty} {w : Tm Γ (σ ⊠ τ)}
         → Prf ε (Pair (Pr1 w) (Pr2 w) =ᴴ w)
--------------------------------------------
------------ Rules of equality -------------
 Refl    : {σ : Ty} {a : Tm Γ σ}
         → Prf ε (a =ᴴ a)
 Sym     : {Ξ : Asmpt Γ} {σ : Ty} {a b : Tm Γ σ}
         → Prf Ξ (a =ᴴ b) → Prf Ξ (b =ᴴ a)
 Trans   : {Ξ : Asmpt Γ} {σ : Ty} {a b c : Tm Γ σ}
         → Prf Ξ (a =ᴴ b) → Prf Ξ (b =ᴴ c) → Prf Ξ (a =ᴴ c)
 ApF     : {Ξ : Asmpt Γ} {σ τ : Ty} {a b : Tm Γ σ} {f : Tm Γ (σ ⇾ τ)}
         → Prf Ξ (a =ᴴ b) → Prf Ξ (f · a =ᴴ f · b)
 FunExt  : {Ξ : Asmpt Γ} {σ τ : Ty} {f g : Tm Γ (σ ⇾ τ)}
         → Prf Ξ (∀ᴴ (wkn f · ν₀ =ᴴ wkn g · ν₀)) → Prf Ξ (f =ᴴ g)
--------------------------------------------
---------------- Rules of ≤ ----------------
 ≤-Zero  : {Ξ : Asmpt Γ} {n : Tm Γ Ⓝ}
         → Prf Ξ (Zero ≤ᴴ n)
 ≤-Succ  : {Ξ : Asmpt Γ} {n m : Tm Γ Ⓝ}
         → Prf Ξ (n ≤ᴴ m) → Prf Ξ (Succ n ≤ᴴ Succ m)
--------------------------------------------
--------- Rules of less-than-equal ---------
 ∈-zero  : {σ : Ty} {a : Tm Γ σ} {w : Tm Γ (σ *)}
         → Prf ε (a ∈ᴴ (Cons a w))
 ∈-succ  : {Ξ : Asmpt Γ} {σ : Ty} {a b : Tm Γ σ} {w : Tm Γ (σ *)}
         → Prf Ξ (a ∈ᴴ w) → Prf Ξ (a ∈ᴴ (Cons b w))
--------------------------------------------
-------------- Logical rules ---------------
 ⊥-elim  : {Ξ : Asmpt Γ} {A : Fml Γ}
         → Prf Ξ ⊥ᴴ → Prf Ξ A
 ∧-intro : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ A → Prf Ξ B → Prf Ξ (A ∧ᴴ B)
 ∧-elim₁ : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ (A ∧ᴴ B) → Prf Ξ A
 ∧-elim₂ : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ (A ∧ᴴ B) → Prf Ξ B
 ∨-inl   : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ A → Prf Ξ (A ∨ᴴ B)
 ∨-inr   : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ B → Prf Ξ (A ∨ᴴ B)
 ∨-elim  : {Ξ : Asmpt Γ} {A B C : Fml Γ}
         → Prf Ξ (A ⇒ᴴ C) → Prf Ξ (B ⇒ᴴ C) → Prf Ξ (A ∨ᴴ B) → Prf Ξ C
 ⇒-intro : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf (Ξ ₊ A) B → Prf Ξ (A ⇒ᴴ B)
 ⇒-elim  : {Ξ : Asmpt Γ} {A B : Fml Γ}
         → Prf Ξ (A ⇒ᴴ B) → Prf Ξ A → Prf Ξ B
 ∀-intro : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → Prf (wknᵃ Ξ) A → Prf Ξ (∀ᴴ A)
 ∀-elim  : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → Prf Ξ (∀ᴴ A) → (u : Tm Γ σ) → Prf Ξ (A [ u ]ᶠ)
 ∃-intro : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → (u : Tm Γ σ) → Prf Ξ (A [ u ]ᶠ) → Prf Ξ (∃ᴴ A)
 ∃-elim  : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)} {B : Fml Γ}
         → Prf Ξ (∀ᴴ (A ⇒ᴴ wknᶠ B)) → Prf Ξ (∃ᴴ A ⇒ᴴ B)
--------------------------------------------
--------------- Axioms of st ---------------
 st-eq   : {Ξ : Asmpt Γ} {σ : Ty} {a b : Tm Γ σ}
         → Prf Ξ (st a) → Prf Ξ (a =ᴴ b) → Prf Ξ (st b)
 st-cl   : {Ξ : Asmpt Γ} {σ : Ty} (t : Tm ε σ)
         → Prf Ξ (st (wkε t))
 st-ap   : {Ξ : Asmpt Γ} {σ τ : Ty} {f : Tm Γ (σ ⇾ τ)} {a : Tm Γ σ}
         → Prf Ξ (st f) → Prf Ξ (st a) → Prf Ξ (st (f · a))
 ∀ˢᵗ-I   : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → Prf Ξ (∀ᴴ (st ν₀ ⇒ᴴ A)) → Prf Ξ (∀ˢᵗ A)
 ∀ˢᵗ-E   : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → Prf Ξ (∀ˢᵗ A) → Prf Ξ (∀ᴴ (st ν₀ ⇒ᴴ A))
 ∃ˢᵗ-I   : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → Prf Ξ (∃ᴴ (st ν₀ ∧ᴴ A)) → Prf Ξ (∃ˢᵗ A)
 ∃ˢᵗ-E   : {Ξ : Asmpt Γ} {σ : Ty} {A : Fml (Γ ₊ σ)}
         → Prf Ξ (∃ˢᵗ A) → Prf Ξ (∃ᴴ (st ν₀ ∧ᴴ A))
--------------------------------------------
-------- Induction principle of Ⓝ ---------
 IR      : {Ξ : Asmpt Γ} {A : Fml (Γ ₊ Ⓝ)} → internal A
         → Prf Ξ (A [ Zero ]ᶠ) → Prf Ξ (∀ᴴ (A ⇒ᴴ A [s]ᶠ)) → Prf Ξ (∀ᴴ A)
 IRˢᵗ    : {Ξ : Asmpt Γ} {A : Fml (Γ ₊ Ⓝ)}
         → Prf Ξ (A [ Zero ]ᶠ) → Prf Ξ (∀ˢᵗ (A ⇒ᴴ A [s]ᶠ)) → Prf Ξ (∀ˢᵗ A)
--------------------------------------------
------------ Nonstandard axioms ------------
 I       : {σ τ : Ty} {φ : Fml (Γ ₊ τ ₊ σ)} → internal φ
         → Prf ε (∀ˢᵗ (∃ᴴ (∀ᴴ (ν₀ ∈ᴴ ν₂ ⇒ᴴ wkn₂ᶠ φ))) ⇒ᴴ ∃ᴴ (∀ˢᵗ φ))
 NCR     : {σ τ : Ty} {Φ : Fml (Γ ₊ τ ₊ σ)}
         → Prf ε (∀ᴴ (∃ˢᵗ Φ) ⇒ᴴ ∃ˢᵗ (∀ᴴ (∃ᴴ (ν₀ ∈ᴴ ν₂ ∧ᴴ wkn₂ᶠ Φ))))
 HAC     : {σ τ : Ty} {Φ : Fml (Γ ₊ σ ₊ τ)}
         → Prf ε (∀ˢᵗ (∃ˢᵗ Φ) ⇒ᴴ ∃ˢᵗ (∀ˢᵗ (∃ᴴ (ν₀ ∈ᴴ (ν₂ · ν₁) ∧ᴴ wkn₂ᶠ Φ))))
 HGMPˢᵗ  : {σ : Ty} {φ : Fml (Γ ₊ σ)} {ψ : Fml Γ} → internal φ → internal ψ
         → Prf ε ((∀ˢᵗ φ ⇒ᴴ ψ) ⇒ᴴ ∃ˢᵗ (∀ᴴ (ν₀ ∈ᴴ ν₁ ⇒ᴴ wkn₁ᶠ φ) ⇒ᴴ wknᶠ ψ))
 HIP-∀ˢᵗ : {σ τ : Ty} {φ : Fml (Γ ₊ σ)} {Ψ : Fml (Γ ₊ τ)} → internal φ
         → Prf ε ((∀ˢᵗ φ ⇒ᴴ ∃ˢᵗ Ψ) ⇒ᴴ ∃ˢᵗ (∀ˢᵗ (wkn₁ᶠ φ) ⇒ᴴ ∃ᴴ (ν₀ ∈ᴴ ν₁ ∧ᴴ wkn₁ᶠ Ψ)))
--------------------------------------------
 st-succ : {Ξ : Asmpt Γ} {n : Tm Γ Ⓝ}
         → Prf Ξ (st n) → Prf Ξ (st (Succ n))
 Lmᴴ[n≤0→n=0]  : {Ξ : Asmpt Γ} {n : Tm Γ Ⓝ}
               → Prf Ξ (n ≤ᴴ Zero) → Prf Ξ (n =ᴴ Zero)
 Lmᴴ[≤-Succ-∨] : {Ξ : Asmpt Γ} {n m : Tm Γ Ⓝ}
               → Prf Ξ (n ≤ᴴ Succ m) → Prf Ξ (n =ᴴ Succ m ∨ᴴ n ≤ᴴ m)
 EvenZ : {Ξ : Asmpt Γ}
       → Prf Ξ (Even Zero)
 EvenS : {Ξ : Asmpt Γ} {n : Tm Γ Ⓝ}
       → Prf Ξ (Even n) → Prf Ξ (Even (Succ (Succ n)))


\end{code}

We define some operators on terms and formulas.

Weakening and substitution on terms

\begin{code}

wk : {Γ Δ : Cxt} {A : Ty} → Γ ⊆ Δ → Tm Γ A → Tm Δ A
wk ξ (Var i)    = Var (ξ i)
wk ξ  ✹         = ✹
wk ξ  TT        = TT
wk ξ  FF        = FF
wk ξ  IF        = IF
wk ξ  Zero      = Zero
wk ξ (Succ n)   = Succ (wk ξ n)
wk ξ  Rec       = Rec
wk ξ  Nil       = Nil
wk ξ (Cons h t) = Cons (wk ξ h) (wk ξ t)
wk ξ  LRec      = LRec
wk ξ (Pair a b) = Pair (wk ξ a) (wk ξ b)
wk ξ (Pr1 w)    = Pr1 (wk ξ w)
wk ξ (Pr2 w)    = Pr2 (wk ξ w)
wk ξ (Lam t)    = Lam (wk (⊆-cons ξ) t)
wk ξ (f · a)    = wk ξ f · wk ξ a

--wkn : {Γ : Cxt} {A X : Ty} → Tm Γ A → Tm (Γ ₊ X) A
wkn = wk succ

--wkε  : {Γ : Cxt} {A : Ty} → Tm ε A → Tm Γ A
wkε = wk ε-⊆

wkn² : {Γ : Cxt} {A X Y : Ty} → Tm Γ A → Tm (Γ ₊ X ₊ Y) A
wkn² = wk (succ ∘ succ)

wkn³ : {Γ : Cxt} {A X Y Z : Ty} → Tm Γ A → Tm (Γ ₊ X ₊ Y ₊ Z) A
wkn³ = wk (succ ∘ succ ∘ succ)

wkn⁴ : {Γ : Cxt} {A X Y Z W : Ty} → Tm Γ A → Tm (Γ ₊ X ₊ Y ₊ Z ₊ W) A
wkn⁴ = wk (succ ∘ succ ∘ succ ∘ succ)

wkn₊₊ : {Γ : Cxt} (Δ : Cxt) {A : Ty} → Tm Γ A → Tm (Γ ₊₊ Δ) A
wkn₊₊ Δ = wk (⊆-₊₊r Δ)

exch : {Γ : Cxt} {A B C : Ty} → Tm (Γ ₊ A ₊ B) C → Tm (Γ ₊ B ₊ A) C
exch = wk ⊆-exch

subst : {Γ : Cxt} {A C : Ty} → Tm (Γ ₊ A) C → Tm Γ A → Tm Γ C
subst (Var zero)     u = u
subst (Var (succ i)) u = Var i
subst  ✹             u = ✹
subst  TT            u = TT
subst  FF            u = FF
subst  IF            u = IF
subst  Zero          u = Zero
subst (Succ n)       u = Succ (subst n u)
subst  Rec           u = Rec
subst  Nil           u = Nil
subst (Cons h t)     u = Cons (subst h u) (subst t u)
subst  LRec          u = LRec
subst (Pair a b)     u = Pair (subst a u) (subst b u)
subst (Pr1 w)        u = Pr1 (subst w u)
subst (Pr2 w)        u = Pr2 (subst w u)
subst (Lam t)        u = Lam (subst (exch t) (wkn u))
subst (f · a)        u = subst f u · subst a u

--_[_] : {Γ : Cxt} {A C : Ty} → Tm (Γ ₊ A) C → Tm Γ A → Tm Γ C
t [ u ] = subst t u

subst-mid : {Γ : Cxt} (Δ : Cxt) {A C : Ty}
          → Tm (Γ ₊ A ₊₊ Δ) C → Tm (Γ ₊₊ Δ) A → Tm (Γ ₊₊ Δ) C
subst-mid Δ t u = (wk (⊆-exch-end Δ) t) [ u ]

\end{code}

Some auxiliary terms

\begin{code}

⟪_⟫ : {Γ : Cxt} {σ : Ty} → Tm Γ σ → Tm Γ (σ *)
⟪ x ⟫ = Cons x Nil

inhabitant : {Γ : Cxt} {σ : Ty} → Tm Γ σ
inhabitant {σ = ①}    = ✹
inhabitant {σ = ②}    = TT
inhabitant {σ = Ⓝ}    = Zero
inhabitant {σ = σ *}   = ⟪ inhabitant ⟫
inhabitant {σ = σ ⊠ τ} = Pair inhabitant inhabitant
inhabitant {σ = σ ⇾ τ} = Lam inhabitant

𝒄 : {Γ : Cxt} {σ : Ty} → Tm Γ σ
𝒄 = inhabitant

⟦𝒄⟧ : (σ : Ty) → ⟦ σ ⟧ʸ
⟦𝒄⟧  ①     = ⋆
⟦𝒄⟧  ②     = ⊤
⟦𝒄⟧  Ⓝ     = 0
⟦𝒄⟧ (σ *)   = ⟨ ⟦𝒄⟧ σ ⟩
⟦𝒄⟧ (σ ⊠ τ) = ⟦𝒄⟧ σ , ⟦𝒄⟧ τ
⟦𝒄⟧ (σ ⇾ τ) = λ _ → ⟦𝒄⟧ τ


ν₃ : {Γ : Cxt} {σ σ₁ σ₂ σ₃ : Ty} → Tm (Γ ₊ σ ₊ σ₁ ₊ σ₂ ₊ σ₃) σ
ν₃ = Var (succ (succ (succ zero)))

ν₄ : {Γ : Cxt} {σ σ₁ σ₂ σ₃ σ₄ : Ty} → Tm (Γ ₊ σ ₊ σ₁ ₊ σ₂ ₊ σ₃ ₊ σ₄) σ
ν₄ = Var (succ (succ (succ (succ zero))))

ν₅ : {Γ : Cxt} {σ σ₁ σ₂ σ₃ σ₄ σ₅ : Ty} → Tm (Γ ₊ σ ₊ σ₁ ₊ σ₂ ₊ σ₃ ₊ σ₄ ₊ σ₅) σ
ν₅ = Var (succ (succ (succ (succ (succ zero)))))

ν₆ : {Γ : Cxt} {σ σ₁ σ₂ σ₃ σ₄ σ₅ σ₆ : Ty} → Tm (Γ ₊ σ ₊ σ₁ ₊ σ₂ ₊ σ₃ ₊ σ₄ ₊ σ₅ ₊ σ₆) σ
ν₆ = Var (succ (succ (succ (succ (succ (succ zero))))))


infixl 20 _++_

_++_ : {Γ : Cxt} {σ : Ty} → Tm Γ (σ *) → Tm Γ (σ *) → Tm Γ (σ *)
xs ++ ys = LRec · xs · Lam (Lam (Cons ν₁ ν₀)) · ys

Mapᴸ : {Γ : Cxt} {σ τ : Ty} → Tm Γ (σ ⇾ τ) → Tm Γ (σ *) → Tm Γ (τ *)
Mapᴸ f xs = LRec · Nil · Lam (Lam (Cons (wkn² f · ν₁) ν₀)) · xs

Appᴸ : {Γ : Cxt} {σ τ : Ty} → Tm Γ ((σ ⇾ τ)*) → Tm Γ (σ *) → Tm Γ (τ *)
Appᴸ fs xs = LRec · Nil · Lam (Lam (Mapᴸ ν₁ (wkn² xs) ++ ν₀)) · fs

_⟪_⟫ᴸ : {Γ : Cxt} {σ τ : Ty} → Tm Γ ((σ ⇾ τ *)*) → Tm Γ σ → Tm Γ (τ *)
F ⟪ x ⟫ᴸ = LRec · Nil · Lam (Lam (ν₁ · wkn² x ++ ν₀)) · F

_⟪_ₓ_⟫ᴸ : {Γ : Cxt} {σ τ ρ : Ty} → Tm Γ ((σ ⇾ τ ⇾ ρ *)*) → Tm Γ σ → Tm Γ τ → Tm Γ (ρ *)
F ⟪ x ₓ y ⟫ᴸ = LRec · Nil · Lam (Lam (ν₁ · wkn² x · wkn² y ++ ν₀)) · F

Pr₁ : {Γ : Cxt} {σ τ : Ty} → Tm Γ (σ ⊠ τ ⇾ σ)
Pr₁ = Lam (Pr1 ν₀)

Pr₂ : {Γ : Cxt} {σ τ : Ty} → Tm Γ (σ ⊠ τ ⇾ τ)
Pr₂ = Lam (Pr2 ν₀)

Pr1ᴸ : {Γ : Cxt} {σ τ : Ty} → Tm Γ ((σ ⊠ τ)*) → Tm Γ (σ *)
Pr1ᴸ = Mapᴸ Pr₁

Pr2ᴸ : {Γ : Cxt} {σ τ : Ty} → Tm Γ ((σ ⊠ τ)*) → Tm Γ (τ *)
Pr2ᴸ = Mapᴸ Pr₂

Pairˡ : {Γ : Cxt} {σ τ : Ty} → Tm Γ (σ *) → Tm Γ τ → Tm Γ ((σ ⊠ τ)*)
Pairˡ xs y = LRec · Nil · Lam (Lam (Cons (Pair ν₁ (wkn² y)) ν₀)) · xs

Pairʳ : {Γ : Cxt} {σ τ : Ty} → Tm Γ σ → Tm Γ (τ *) → Tm Γ ((σ ⊠ τ)*)
Pairʳ x ys = LRec · Nil · Lam (Lam (Cons (Pair (wkn² x) ν₁) ν₀)) · ys

Pairᴸ : {Γ : Cxt} {σ τ : Ty} → Tm Γ (σ *) → Tm Γ (τ *) → Tm Γ ((σ ⊠ τ)*)
Pairᴸ xs ys = LRec · Nil · Lam (Lam (Pairʳ ν₁ (wkn² ys) ++ ν₀)) · xs

\end{code}

Weakening and substitution on formulas

\begin{code}

wkᶠ : {Γ Δ : Cxt} → Γ ⊆ Δ → Fml Γ → Fml Δ
wkᶠ ξ (st a)   = st (wk ξ a)
wkᶠ ξ (a =ᴴ b) = wk ξ a =ᴴ wk ξ b
wkᶠ ξ (a ≤ᴴ b) = wk ξ a ≤ᴴ wk ξ b
wkᶠ ξ (a ∈ᴴ w) = wk ξ a ∈ᴴ wk ξ w
wkᶠ ξ (A ∧ᴴ B) = wkᶠ ξ A ∧ᴴ wkᶠ ξ B
wkᶠ ξ (A ∨ᴴ B) = wkᶠ ξ A ∨ᴴ wkᶠ ξ B
wkᶠ ξ (A ⇒ᴴ B) = wkᶠ ξ A ⇒ᴴ wkᶠ ξ B
wkᶠ ξ (∀ᴴ A)   = ∀ᴴ (wkᶠ (⊆-cons ξ) A)
wkᶠ ξ (∃ᴴ A)   = ∃ᴴ (wkᶠ (⊆-cons ξ) A)
wkᶠ ξ (∀ˢᵗ A)  = ∀ˢᵗ (wkᶠ (⊆-cons ξ) A)
wkᶠ ξ (∃ˢᵗ A)  = ∃ˢᵗ (wkᶠ (⊆-cons ξ) A)
wkᶠ ξ (Even n) = Even (wk ξ n)

--wknᶠ : {Γ : Cxt} {σ : Ty} → Fml Γ → Fml (Γ ₊ σ)
wknᶠ = wkᶠ succ

--wkn₁ᶠ : {Γ : Cxt} {σ τ : Ty} → Fml (Γ ₊ σ) → Fml (Γ ₊ τ ₊ σ)
wkn₁ᶠ {σ = σ} = wkᶠ (⊆-ext (ε ₊ σ))

--wkn₂ᶠ : {Γ : Cxt} {σ τ ρ : Ty} → Fml (Γ ₊ σ ₊ τ) → Fml (Γ ₊ ρ ₊ σ ₊ τ)
wkn₂ᶠ {σ = σ} {τ} = wkᶠ (⊆-ext (ε ₊ σ ₊ τ))

--wkn²ᶠ : {Γ : Cxt} {σ τ : Ty} → Fml Γ → Fml (Γ ₊ σ ₊ τ)
wkn²ᶠ = wkᶠ (succ ∘ succ)

exchᶠ : {Γ : Cxt} {σ τ : Ty} → Fml (Γ ₊ σ ₊ τ) → Fml (Γ ₊ τ ₊ σ)
exchᶠ = wkᶠ ⊆-exch

substᶠ : {Γ : Cxt} {σ : Ty} → Fml (Γ ₊ σ) → Tm Γ σ → Fml Γ
substᶠ (st a)   u = st (a [ u ])
substᶠ (a =ᴴ b) u = a [ u ] =ᴴ b [ u ]
substᶠ (a ≤ᴴ b) u = a [ u ] ≤ᴴ b [ u ]
substᶠ (a ∈ᴴ w) u = a [ u ] ∈ᴴ w [ u ]
substᶠ (A ∧ᴴ B) u = substᶠ A u ∧ᴴ substᶠ B u
substᶠ (A ∨ᴴ B) u = substᶠ A u ∨ᴴ substᶠ B u
substᶠ (A ⇒ᴴ B) u = substᶠ A u ⇒ᴴ substᶠ B u
substᶠ (∀ᴴ A)   u = ∀ᴴ (substᶠ (exchᶠ A) (wkn u))
substᶠ (∃ᴴ A)   u = ∃ᴴ (substᶠ (exchᶠ A) (wkn u))
substᶠ (∀ˢᵗ A)  u = ∀ˢᵗ (substᶠ (exchᶠ A) (wkn u))
substᶠ (∃ˢᵗ A)  u = ∃ˢᵗ (substᶠ (exchᶠ A) (wkn u))
substᶠ (Even n) u = Even (n [ u ])

--_[_]ᶠ : {Γ : Cxt} {σ : Ty} → Fml (Γ ₊ σ) → Tm Γ σ → Fml Γ
A [ u ]ᶠ = substᶠ A u

\end{code}

The following operator replaces the last variable by its successor,
i.e. A(x) ↦ A(succ x)

\begin{code}

_[s] : {Γ : Cxt} {σ : Ty} → Tm (Γ ₊ Ⓝ) σ → Tm (Γ ₊ Ⓝ) σ
Var zero [s] = Succ (Var zero)
Var (succ i) [s] = Var (succ i)
✹ [s] = ✹
Zero [s] = Zero
(Succ n) [s] = Succ (n [s])
Rec [s] = Rec
TT [s] = TT
FF [s] = FF
IF [s] = IF
Nil [s] = Nil
Cons h t [s] = Cons (h [s]) (t [s])
LRec [s] = LRec
Pair a b [s] = Pair (a [s]) (b [s])
Pr1 w [s] = Pr1 (w [s])
Pr2 w [s] = Pr2 (w [s])
Lam t [s] = Lam (exch ((exch t) [s]))
(f · a) [s] = (f [s]) · (a [s])

--_[s]ᶠ : {Γ : Cxt} → Fml (Γ ₊ Ⓝ) → Fml (Γ ₊ Ⓝ)
(st a) [s]ᶠ   = st (a [s])
(a =ᴴ b) [s]ᶠ = (a [s]) =ᴴ (b [s])
(a ≤ᴴ b) [s]ᶠ = (a [s]) ≤ᴴ (b [s])
(a ∈ᴴ w) [s]ᶠ = (a [s]) ∈ᴴ (w [s])
(A ∧ᴴ B) [s]ᶠ = (A [s]ᶠ) ∧ᴴ (B [s]ᶠ)
(A ∨ᴴ B) [s]ᶠ = (A [s]ᶠ) ∨ᴴ (B [s]ᶠ)
(A ⇒ᴴ B) [s]ᶠ = (A [s]ᶠ) ⇒ᴴ (B [s]ᶠ)
(∀ᴴ A) [s]ᶠ   = ∀ᴴ (exchᶠ ((exchᶠ A) [s]ᶠ))
(∃ᴴ A) [s]ᶠ   = ∃ᴴ (exchᶠ ((exchᶠ A) [s]ᶠ))
(∀ˢᵗ A) [s]ᶠ  = ∀ˢᵗ (exchᶠ ((exchᶠ A) [s]ᶠ))
(∃ˢᵗ A) [s]ᶠ  = ∃ˢᵗ (exchᶠ ((exchᶠ A) [s]ᶠ))
(Even n) [s]ᶠ = Even (n [s])

\end{code}

Some auxiliary proofs

\begin{code}

κ₀ : {Γ : Cxt} {Ξ : Asmpt Γ} {A : Fml Γ} → Prf (Ξ ₊ A) A
κ₀ {Ξ = ε}     = Id
κ₀ {Ξ = Ξ ₊ _} = Swap ε (Wkn κ₀)

κ₁ : {Γ : Cxt} {Ξ : Asmpt Γ} {A B : Fml Γ} → Prf (Ξ ₊ A ₊ B) A
κ₁ = Wkn κ₀

κ₂ : {Γ : Cxt} {Ξ : Asmpt Γ} {A B C : Fml Γ} → Prf (Ξ ₊ A ₊ B ₊ C) A
κ₂ = Wkn κ₁

κ₃ : {Γ : Cxt} {Ξ : Asmpt Γ} {A B C D : Fml Γ} → Prf (Ξ ₊ A ₊ B ₊ C ₊ D) A
κ₃ = Wkn κ₂

\end{code}