Chuangjie Xu, January 2016

We explore the Dialectica interpretation of first order logic into
Martin-Löf type theory (in Agda notation).

The idea of the Dialectica interpretation is that each formula A is
transformed to a classically equivalent one of the form ∃x.∀y.|A|
where with ∣A∣ quantifier-free.

In this study, the language to interpret is a subset of Agda equipped
with a first order logic.  We adopt the inference rules of the system
IL from Oliva[1] to define the interpreted logic.  The Dialectica
interpretation is slightly adapted for dependent types as in Bauer[2].

References.

[1] Paulo Oliva, Unifying Functional Interpretation.  Notre Dame
Journal of Formal Logic 47 (2):263-290, 2006.

[2] Andrej Bauer, The Dialectica interpretation in Coq.  Available at
http://math.andrej.com/2011/01/03/the-dialectica-interpertation-in-coq/

\begin{code}

module Dialectica where

open import Preliminaries

\end{code}

The term language is the full hierarchy of finite types in which every
type is inhabited.

\begin{code}

infixr 20 _⊗_
infixr 10 _⇾_

data Ty : Set where
Ⓝ : Ty
_⊗_ : Ty → Ty → Ty
_⇾_ : Ty → Ty → Ty

⟦_⟧ : Ty → Set
⟦ Ⓝ ⟧ = ℕ
⟦ σ ⊗ τ ⟧ = ⟦ σ ⟧ × ⟦ τ ⟧
⟦ σ ⇾ τ ⟧ = ⟦ σ ⟧ → ⟦ τ ⟧

⟦inhabitant⟧ : {σ : Ty} → ⟦ σ ⟧
⟦inhabitant⟧ {Ⓝ} = 0
⟦inhabitant⟧ {σ ⊗ τ} = ⟦inhabitant⟧ , ⟦inhabitant⟧
⟦inhabitant⟧ {σ ⇾ τ} = λ _ → ⟦inhabitant⟧

\end{code}

We inductively define a first order logic on the full type hierarchy
consisting of types Prp of propositions and Prf of proofs.

Notice that predicates are represented as (Agda) functions into Prp.
This forces us to adapt the original Dialectica interpretation by
introducing certain type dependencies.

\begin{code}

infix 50 _==_
infix 40 _∧_
infix 30 _⇒_

data Prp : Set where
_==_ : {σ : Ty} → ⟦ σ ⟧ → ⟦ σ ⟧ → Prp
_∧_ : Prp → Prp → Prp
_⇒_ : Prp → Prp → Prp
∀′ : {σ : Ty} → (⟦ σ ⟧ → Prp) → Prp
∃′ : {σ : Ty} → (⟦ σ ⟧ → Prp) → Prp

\end{code}

An element of Prf Γ A represents a proof of A under the assumption Γ
where an assumption is simply a list of propositions.

Each constructor represents an inference rule. For example,

Γ ⊢ A         Δ ⊢ B
----------------------- ∧-intro
Γ , Δ ⊢ A ∧ B

is represented by the constructor

∧-intro : {Γ Δ : Asmpt} {A B : Prp}
→ Prf Γ A → Prf Δ B → Prf (Γ ₊₊ Δ) (A ∧ B)

Notice that the constructors J and ind should have more general
assumptions.  We work with the ones in empty assumption for simplicity.

\begin{code}

Asmpt : Set
Asmpt = List Prp

data Prf : Asmpt → Prp → Set where
refl : {σ : Ty} {a : ⟦ σ ⟧}
→ Prf ε (a == a)
J    : {σ : Ty} (φ : ⟦ σ ⟧ → ⟦ σ ⟧ → Prp)
→ ((a : ⟦ σ ⟧) → Prf ε (φ a a))
→ {a b : ⟦ σ ⟧} → Prf ε (a == b) → Prf ε (φ a b)
id   : {A : Prp}
→ Prf (ε ₊ A) A
wkn  : {Γ : Asmpt} {A B : Prp}
→ Prf Γ B → Prf (Γ ₊ A) B
cut  : {Γ Δ : Asmpt} {A B : Prp}
→ Prf (Γ ₊ A) B → Prf Δ A → Prf (Γ ₊₊ Δ) B
swap : {Γ : Asmpt} (Δ : Asmpt) {A B C : Prp}
→ Prf (Γ ₊ A ₊ B ₊₊ Δ) C → Prf (Γ ₊ B ₊ A ₊₊ Δ) C
∧-intro : {Γ Δ : Asmpt} {A B : Prp}
→ Prf Γ A → Prf Δ B → Prf (Γ ₊₊ Δ) (A ∧ B)
∧-elim₀ : {Γ : Asmpt} {A B : Prp}
→ Prf Γ (A ∧ B) → Prf Γ A
∧-elim₁ : {Γ : Asmpt} {A B : Prp}
→ Prf Γ (A ∧ B) → Prf Γ B
⇒-intro : {Γ : Asmpt} {A B : Prp}
→ Prf (Γ ₊ A) B → Prf Γ (A ⇒ B)
⇒-elim  : {Γ : Asmpt} {A B : Prp}
→ Prf Γ (A ⇒ B) → Prf (Γ ₊ A) B
∀-intro : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp}
→ ((x : ⟦ σ ⟧) → Prf Γ (φ x)) → Prf Γ (∀′ φ)
∀-elim  : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp}
→ Prf Γ (∀′ φ) → (a : ⟦ σ ⟧) → Prf Γ (φ a)
∃-intro : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp}
→ (a : ⟦ σ ⟧) → Prf Γ (φ a) → Prf Γ (∃′ φ)
∃-elim  : {Γ : Asmpt} {σ : Ty} {φ : ⟦ σ ⟧ → Prp} {A : Prp}
→ ((x : ⟦ σ ⟧) → Prf Γ (φ x ⇒ A)) → Prf Γ ((∃′ φ) ⇒ A)
ind : (φ : ℕ → Prp)
→ Prf ε (φ 0) → Prf ε (∀′ (λ n → φ n ⇒ φ (succ n))) → Prf ε (∀′ φ)

\end{code}

Our goal is to transform each proposition A into a type Σx.Πy.∣A∣.  To
determine the types of x and y, we assign to each proposition A types
d⁺(A) and d⁻(A), where d⁺(A) is intended to be the type of a realizer
to be extracted from a proof of A and d⁻(A) is the type of a challenge
for the claim that this term realizes A.

The types of realizers and challenges are inhabited.  We make a
canonical choice of an inhabitant of each type.

\begin{code}

d⁺ d⁻ : Prp → Set
d⁺ (u == v) = 𝟙
d⁺ (A ∧ B) = (d⁺ A) × (d⁺ B)
d⁺ (A ⇒ B) = (d⁺ A → d⁺ B) × (d⁺ A → d⁻ B → d⁻ A)
d⁺ (∀′ {σ} φ) = (x : ⟦ σ ⟧) → d⁺ (φ x)
d⁺ (∃′ {σ} φ) = Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)
d⁻ (u == v) = 𝟙
d⁻ (A ∧ B) = (d⁻ A) × (d⁻ B)
d⁻ (A ⇒ B) = (d⁺ A) × (d⁻ B)
d⁻ (∀′ {σ} φ) = Σ \(x : ⟦ σ ⟧) → d⁻ (φ x)
d⁻ (∃′ {σ} φ) = (x : ⟦ σ ⟧) → d⁺ (φ x) → d⁻ (φ x)

inhabitant⁺ : (A : Prp) → d⁺ A
inhabitant⁻ : (A : Prp) → d⁻ A
inhabitant⁺ (u == v) = ⋆
inhabitant⁺ (A ∧ B) = inhabitant⁺ A , inhabitant⁺ B
inhabitant⁺ (A ⇒ B) = (λ _ → inhabitant⁺ B) , (λ _ _ → inhabitant⁻ A)
inhabitant⁺ (∀′ φ) = λ x → inhabitant⁺ (φ x)
inhabitant⁺ (∃′ φ) = ⟦inhabitant⟧ , inhabitant⁺ (φ ⟦inhabitant⟧)
inhabitant⁻ (u == v) = ⋆
inhabitant⁻ (A ∧ B) = inhabitant⁻ A , inhabitant⁻ B
inhabitant⁻ (A ⇒ B) = inhabitant⁺ A , inhabitant⁻ B
inhabitant⁻ (∀′ φ) = ⟦inhabitant⟧ , inhabitant⁻ (φ ⟦inhabitant⟧)
inhabitant⁻ (∃′ φ) = λ x _ → inhabitant⁻ (φ x)

dd⁺ dd⁻ : Asmpt → Set
dd⁺ Γ = (i : Index Γ) → d⁺ (Γ ₍ i ₎)
dd⁻ Γ = (i : Index Γ) → d⁻ (Γ ₍ i ₎)

iA⁺ : (Γ : Asmpt) → dd⁺ Γ
iA⁺ Γ i = inhabitant⁺ (Γ ₍ i ₎)

iA⁻ : (Γ : Asmpt) → dd⁻ Γ
iA⁻ Γ i = inhabitant⁻ (Γ ₍ i ₎)

\end{code}

The dialectica interpretation (of propositions and assumptions)

\begin{code}

∣_∣ : (φ : Prp) → d⁺ φ → d⁻ φ → Set
∣ u == v ∣ _ _ = u ≡ v
∣ A ∧ B ∣ (t₀ , t₁) (y₀ , y₁)  = ∣ A ∣ t₀ y₀ × ∣ B ∣ t₁ y₁
∣ A ⇒ B ∣ (t₀ , t₁) (y₀ , y₁) = ∣ A ∣ y₀ (t₁ y₀ y₁) → ∣ B ∣ (t₀ y₀) y₁
∣ ∀′ φ ∣ t (a , y) =  ∣ φ a ∣ (t a) y
∣ ∃′ φ ∣ (a , t) y = ∣ φ a ∣ t (y a t)

∥_∥ : (Γ : Asmpt) → dd⁺ Γ → dd⁻ Γ → Set
∥ ε ∥ _ _ = 𝟙
∥ Γ ₊ X ∥ xs rs = ∥ Γ ∥ (xs ∘ succ) (rs ∘ succ) × ∣ X ∣ (xs zero) (rs zero)

\end{code}

The soundness theorem says that each proof of a proposition A in the
interpreted logic is transformed to an element of type Σt.Πy.∣A∣(t,y)
in Agda.  Since we work more generally with proofs in assumptions, the
theorem is generalized to the following.

\begin{code}

Prfᴬ : Set → Set → Set
Prfᴬ Γ A = Γ → A

Thm[soundness] : {Γ : Asmpt} {A : Prp} → Prf Γ A
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)

\end{code}

The proof of Thm[soundness] is placed in the end of this file.  It's
done by induction on Prf.  We prove the cases (corresponding to the
constructors of Prf) one by one.

For this, we need the following auxiliary functions and lemmas of assumptions.

\begin{code}

pr₀ᴸ⁺ : {Γ : Asmpt} (Δ : Asmpt) → dd⁺ (Γ ₊₊ Δ) → dd⁺ Γ
pr₀ᴸ⁺ ε xs = xs
pr₀ᴸ⁺ (Δ ₊ _) xs = pr₀ᴸ⁺ Δ (xs ∘ succ)

pr₁ᴸ⁺ : {Γ : Asmpt} (Δ : Asmpt) → dd⁺ (Γ ₊₊ Δ) → dd⁺ Δ
pr₁ᴸ⁺ ε xs ()
pr₁ᴸ⁺ (Δ ₊ X) xs zero = xs zero
pr₁ᴸ⁺ (Δ ₊ X) xs (succ i) = pr₁ᴸ⁺ Δ (xs ∘ succ) i

pairᴸ⁺ : {Γ : Asmpt} (Δ : Asmpt) → dd⁺ Γ → dd⁺ Δ → dd⁺ (Γ ₊₊ Δ)
pairᴸ⁺ ε rs₀ rs₁ = rs₀
pairᴸ⁺ (Δ ₊ _) rs₀ rs₁ zero = rs₁ zero
pairᴸ⁺ (Δ ₊ _) rs₀ rs₁ (succ i) = pairᴸ⁺ Δ rs₀ (rs₁ ∘ succ) i

pr₀ᴸ⁻ : {Γ : Asmpt} (Δ : Asmpt) → dd⁻ (Γ ₊₊ Δ) → dd⁻ Γ
pr₀ᴸ⁻ ε xs = xs
pr₀ᴸ⁻ (Δ ₊ _) xs = pr₀ᴸ⁻ Δ (xs ∘ succ)

pr₁ᴸ⁻ : {Γ : Asmpt} (Δ : Asmpt) → dd⁻ (Γ ₊₊ Δ) → dd⁻ Δ
pr₁ᴸ⁻ ε xs ()
pr₁ᴸ⁻ (Δ ₊ X) xs zero = xs zero
pr₁ᴸ⁻ (Δ ₊ X) xs (succ i) = pr₁ᴸ⁻ Δ (xs ∘ succ) i

pairᴸ⁻ : {Γ : Asmpt} (Δ : Asmpt) → dd⁻ Γ → dd⁻ Δ → dd⁻ (Γ ₊₊ Δ)
pairᴸ⁻ ε rs₀ rs₁ = rs₀
pairᴸ⁻ (Δ ₊ _) rs₀ rs₁ zero = rs₁ zero
pairᴸ⁻ (Δ ₊ _) rs₀ rs₁ (succ i) = pairᴸ⁻ Δ rs₀ (rs₁ ∘ succ) i

∥₊₊∥→× : {Γ : Asmpt} (Δ : Asmpt) (xs : dd⁺ (Γ ₊₊ Δ)) (rs₀ : dd⁻ Γ) (rs₁ : dd⁻ Δ)
→ ∥ Γ ₊₊ Δ ∥ xs (pairᴸ⁻ Δ rs₀ rs₁) → ∥ Γ ∥ (pr₀ᴸ⁺ Δ xs) rs₀ × ∥ Δ ∥ (pr₁ᴸ⁺ Δ xs) rs₁
∥₊₊∥→× ε xs rs₀ rs₁ ρ = ρ , ⋆
∥₊₊∥→× (Δ ₊ _) xs rs₀ rs₁ (ρ , x) = pr₀ IH , pr₁ IH , x
where
IH = ∥₊₊∥→× Δ (xs ∘ succ) rs₀ (rs₁ ∘ succ) ρ

×→∥₊₊∥ : {Γ : Asmpt} (Δ : Asmpt) (xs : dd⁺ (Γ ₊₊ Δ)) (rs : dd⁻ (Γ ₊₊ Δ))
→ ∥ Γ ∥ (pr₀ᴸ⁺ Δ xs) (pr₀ᴸ⁻ Δ rs) × ∥ Δ ∥ (pr₁ᴸ⁺ Δ xs) (pr₁ᴸ⁻ Δ rs) → ∥ Γ ₊₊ Δ ∥ xs rs
×→∥₊₊∥ ε xs rs (ρ , ⋆) = ρ
×→∥₊₊∥ (Δ ₊ _) xs rs (γ , δ , x) = ×→∥₊₊∥ Δ (xs ∘ succ) (rs ∘ succ) (γ , δ) , x

swap⁺ : {Γ : Asmpt} (Δ : Asmpt) {A B : Prp}
→ dd⁺ (Γ ₊ A ₊ B ₊₊ Δ) → dd⁺ (Γ ₊ B ₊ A ₊₊ Δ)
swap⁺ ε xs zero = xs (succ zero)
swap⁺ ε xs (succ zero) = xs zero
swap⁺ ε xs (succ (succ i)) = xs (succ (succ i))
swap⁺ (Δ ₊ _) xs zero = xs zero
swap⁺ (Δ ₊ _) xs (succ i) = swap⁺ Δ (xs ∘ succ) i

swap⁻ : {Γ : Asmpt} (Δ : Asmpt) {A B : Prp}
→ dd⁻ (Γ ₊ A ₊ B ₊₊ Δ) → dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)
swap⁻ ε xs zero = xs (succ zero)
swap⁻ ε xs (succ zero) = xs zero
swap⁻ ε xs (succ (succ i)) = xs (succ (succ i))
swap⁻ (Δ ₊ _) xs zero = xs zero
swap⁻ (Δ ₊ _) xs (succ i) = swap⁻ Δ (xs ∘ succ) i

∥swap∥→× : {Γ : Asmpt} (Δ : Asmpt) {A B : Prp}
→ (xs : dd⁺ (Γ ₊ B ₊ A ₊₊ Δ)) (rs' : dd⁻ (Γ ₊ A ₊ B ₊₊ Δ))
→ ∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs (swap⁻ Δ rs')
→ ((∥ Γ ∥ (pr₀ᴸ⁺ Δ (swap⁺ Δ xs) ∘ succ ∘ succ) (pr₀ᴸ⁻ Δ rs' ∘ succ ∘ succ) ×
∣ B ∣ (pr₀ᴸ⁺ Δ (swap⁺ Δ xs) zero) (pr₀ᴸ⁻ Δ rs' zero)) ×
∣ A ∣ (pr₀ᴸ⁺ Δ (swap⁺ Δ xs) (succ zero)) (pr₀ᴸ⁻ Δ rs' (succ zero))) ×
∥ Δ ∥ (pr₁ᴸ⁺ Δ (swap⁺ Δ xs)) (pr₁ᴸ⁻ Δ rs')
∥swap∥→× ε xs rs' ρ = ρ , ⋆
∥swap∥→× (Δ ₊ _) xs rs' (ρ , x) = pr₀ IH , pr₁ IH , x
where
IH = ∥swap∥→× Δ (xs ∘ succ) (rs' ∘ succ) ρ

\end{code}

The cases of reflexivity and the J-eliminator

\begin{code}

case-refl : {σ : Ty} {a : ⟦ σ ⟧}
→ (_ : dd⁺ ε) → Σ \(t : d⁺ (a == a)) → (y : d⁻ (a == a)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ a == a ∣ t y)
case-refl _ = ⋆ , (λ _ → (λ()) , (λ _ → refl))

case-J : {σ : Ty} (φ : ⟦ σ ⟧ → ⟦ σ ⟧ → Prp)
→ ((a : ⟦ σ ⟧) → (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a a)) → (y : d⁻ (φ a a)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a a ∣ t y))
→ {a b : ⟦ σ ⟧} → ((_ : dd⁺ ε) → Σ \(t : d⁺ (a == b)) → (y : d⁻ (a == b)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ a == b ∣ t y))
→ (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a b)) → (y : d⁻ (φ a b)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a b ∣ t y)
case-J {σ} φ IH₀ {a} {b} IH₁ = goal
where
p : a ≡ b
p = pr₁ (pr₁ (IH₁ (λ())) ⋆) ⋆
Q : ⟦ σ ⟧ → Set
Q x = (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a x)) → (y : d⁻ (φ a x)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a x ∣ t y)
goal : (_ : dd⁺ ε) → Σ \(t : d⁺ (φ a b)) → (y : d⁻ (φ a b)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ a b ∣ t y)
goal = transport Q p (IH₀ a)

\end{code}

The cases of basic rules in sequent calculi

\begin{code}

case-id : (A : Prp)
→ (xs : dd⁺ (ε ₊ A)) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ (ε ₊ A)) → Prfᴬ (∥ ε ₊ A ∥ xs rs) (∣ A ∣ t y)
case-id A xs = t , goal
where
t :  d⁺ A
t = xs zero
frs : d⁻ A → dd⁻ (ε ₊ A)
frs y zero = y
frs y (succ ())
goal : (y : d⁻ A) → Σ \(rs : dd⁻ (ε ₊ A)) → Prfᴬ (∥ ε ₊ A ∥ xs rs) (∣ A ∣ t y)
goal y = frs y , pr₁

case-wkn : {Γ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ Γ) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y))
→ (xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
case-wkn {Γ} A B IH xs = t , goal
where
t : d⁺ B
t = pr₀ (IH (xs ∘ succ))
goal : (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
goal y = rs , claim
where
rs : dd⁻ (Γ ₊ A)
rs zero = inhabitant⁻ A
rs (succ i) = pr₀ (pr₁ (IH (xs ∘ succ)) y) i
claim : Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
claim (γ , _) = pr₁ (pr₁ (IH (xs ∘ succ)) y) γ

case-cut : {Γ Δ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y))
→ ((xs : dd⁺ Δ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Δ) → Prfᴬ (∥ Δ ∥ xs rs) (∣ A ∣ t y))
→ (xs : dd⁺ (Γ ₊₊ Δ)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ B ∣ t y)
case-cut {Γ} {Δ} A B IH₀ IH₁ xs = tb , goal
where
xs₁ : dd⁺ Δ
xs₁ = pr₁ᴸ⁺ Δ xs
ta : d⁺ A
ta = pr₀ (IH₁ xs₁)
xs₀' : dd⁺ Γ
xs₀' = pr₀ᴸ⁺ Δ xs
xs₀ : dd⁺ (Γ ₊ A)
xs₀ zero = ta
xs₀ (succ i) = xs₀' i
tb : d⁺ B
tb = pr₀ (IH₀ xs₀)
goal : (yb : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ B ∣ tb yb)
goal yb = rs , claim₃
where
rs₀ : dd⁻ (Γ ₊ A)
rs₀ = pr₀ (pr₁ (IH₀ xs₀) yb)
rs₀' : dd⁻ Γ
rs₀' = rs₀ ∘ succ
ya : d⁻ A
ya = rs₀ zero
rs₁ : dd⁻ Δ
rs₁ = pr₀ (pr₁ (IH₁ xs₁) ya)
rs : dd⁻ (Γ ₊₊ Δ)
rs = pairᴸ⁻ Δ rs₀' rs₁
claim₀ : Prfᴬ (∥ Γ ₊ A ∥ xs₀ rs₀) (∣ B ∣ tb yb)
claim₀ = pr₁ (pr₁ (IH₀ xs₀) yb)
claim₁ : Prfᴬ (∥ Δ ∥ xs₁ rs₁) (∣ A ∣ ta ya)
claim₁ = pr₁ (pr₁ (IH₁ xs₁) ya)
claim₂ : Prfᴬ (∥ Γ ∥ xs₀' rs₀' × ∥ Δ ∥ xs₁ rs₁) (∣ B ∣ tb yb)
claim₂ (γ , δ) = claim₀ (γ , claim₁ δ)
claim₃ : Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ B ∣ tb yb)
claim₃ ρ = claim₂ (∥₊₊∥→× Δ xs rs₀' rs₁ ρ)

case-swap : (Γ Δ : Asmpt) (A B C : Prp)
→ ((xs : dd⁺ (Γ ₊ A ₊ B ₊₊ Δ)) → Σ \(t : d⁺ C) → (y : d⁻ C) → Σ \(rs : dd⁻ (Γ ₊ A ₊ B ₊₊ Δ)) → Prfᴬ (∥ Γ ₊ A ₊ B ₊₊ Δ ∥ xs rs) (∣ C ∣ t y))
→ (xs : dd⁺ (Γ ₊ B ₊ A ₊₊ Δ)) → Σ \(t : d⁺ C) → (y : d⁻ C) → Σ \(rs : dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)) → Prfᴬ (∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs rs) (∣ C ∣ t y)
case-swap Γ Δ A B C IH xs = t , goal
where
xs' : dd⁺ (Γ ₊ A ₊ B ₊₊ Δ)
xs' = swap⁺ Δ xs
t : d⁺ C
t = pr₀ (IH xs')
goal : (y : d⁻ C) → Σ \(rs : dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)) → Prfᴬ (∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs rs) (∣ C ∣ t y)
goal y = rs , claim₃
where
rs' : dd⁻ (Γ ₊ A ₊ B ₊₊ Δ)
rs' = pr₀ (pr₁ (IH xs') y)
rs : dd⁻ (Γ ₊ B ₊ A ₊₊ Δ)
rs = swap⁻ Δ rs'
xs'₀ : dd⁺ (Γ ₊ A ₊ B)
xs'₀ = pr₀ᴸ⁺ Δ xs'
tb : d⁺ B
tb = xs'₀ zero
ta : d⁺ A
ta = xs'₀ (succ zero)
xs₀ : dd⁺ Γ
xs₀ = xs'₀ ∘ succ ∘ succ
xs₁ : dd⁺ Δ
xs₁ = pr₁ᴸ⁺ Δ xs'
rs'₀ : dd⁻ (Γ ₊ A ₊ B)
rs'₀ = pr₀ᴸ⁻ Δ rs'
yb : d⁻ B
yb = rs'₀ zero
ya : d⁻ A
ya = rs'₀ (succ zero)
rs₀ : dd⁻ Γ
rs₀ = rs'₀ ∘ succ ∘ succ
rs₁ : dd⁻ Δ
rs₁ = pr₁ᴸ⁻ Δ rs'
claim₀ : Prfᴬ (∥ Γ ₊ A ₊ B ₊₊ Δ ∥ xs' rs') (∣ C ∣ t y)
claim₀ = pr₁ (pr₁ (IH xs') y)
claim₁ : Prfᴬ (((∥ Γ ∥ xs₀ rs₀ × ∣ A ∣ ta ya) × ∣ B ∣ tb yb) × ∥ Δ ∥ xs₁ rs₁) (∣ C ∣ t y)
claim₁ ρ = claim₀ (×→∥₊₊∥ Δ xs' rs' ρ)
claim₂ : Prfᴬ (((∥ Γ ∥ xs₀ rs₀ × ∣ B ∣ tb yb) × ∣ A ∣ ta ya) × ∥ Δ ∥ xs₁ rs₁) (∣ C ∣ t y)
claim₂ (((γ , b) , a) , δ) = claim₁ (((γ , a) , b) , δ)
claim₃ : Prfᴬ (∥ Γ ₊ B ₊ A ₊₊ Δ ∥ xs rs) (∣ C ∣ t y)
claim₃ ρ = claim₂ (∥swap∥→× Δ xs rs' ρ)

\end{code}

The cases of inference rules of propositional logic

\begin{code}

case-∧-intro : {Γ Δ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ Γ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y))
→ ((xs : dd⁺ Δ) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ Δ) → Prfᴬ (∥ Δ ∥ xs rs) (∣ B ∣ t y))
→ (xs : dd⁺ (Γ ₊₊ Δ)) → Σ \(t : d⁺ (A ∧ B)) → (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ A ∧ B ∣ t y)
case-∧-intro {Γ} {Δ} A B IH₀ IH₁ xs = t , goal
where
xs₀ : dd⁺ Γ
xs₀ = pr₀ᴸ⁺ Δ xs
t₀ : d⁺ A
t₀ = pr₀ (IH₀ xs₀)
xs₁ : dd⁺ Δ
xs₁ = pr₁ᴸ⁺ Δ xs
t₁ : d⁺ B
t₁ = pr₀ (IH₁ xs₁)
t : d⁺ (A ∧ B)
t = t₀ , t₁
goal : (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ (Γ ₊₊ Δ)) → Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ A ∧ B ∣ t y)
goal (y₀ , y₁) = rs , claim₃
where
rs₀ : dd⁻ Γ
rs₀ = pr₀ (pr₁ (IH₀ xs₀) y₀)
rs₁ : dd⁻ Δ
rs₁ = pr₀ (pr₁ (IH₁ xs₁) y₁)
rs : dd⁻ (Γ ₊₊ Δ)
rs = pairᴸ⁻ Δ rs₀ rs₁
claim₀ : Prfᴬ (∥ Γ ∥ xs₀ rs₀) (∣ A ∣ t₀ y₀)
claim₀ = pr₁ (pr₁ (IH₀ xs₀) y₀)
claim₁ : Prfᴬ (∥ Δ ∥ xs₁ rs₁) (∣ B ∣ t₁ y₁)
claim₁ = pr₁ (pr₁ (IH₁ xs₁) y₁)
claim₂ : Prfᴬ (∥ Γ ∥ xs₀ rs₀ × ∥ Δ ∥ xs₁ rs₁) (∣ A ∣ t₀ y₀ × ∣ B ∣ t₁ y₁)
claim₂ (γ , δ) = claim₀ γ , claim₁ δ
claim₃ : Prfᴬ (∥ Γ ₊₊ Δ ∥ xs rs) (∣ A ∧ B ∣ (t₀ , t₁) (y₀ , y₁))
claim₃ ρ = claim₂ (∥₊₊∥→× Δ xs rs₀ rs₁ ρ)

case-∧-elim₀ : {Γ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ Γ) → Σ \(t : d⁺ (A ∧ B)) → (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∧ B ∣ t y))
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ A) → (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)
case-∧-elim₀ {Γ} A B IH xs = t , goal
where
t : d⁺ A
t = pr₀ (pr₀ (IH xs))
goal : (y : d⁻ A) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)
goal y = rs , claim
where
rs : dd⁻ Γ
rs = pr₀ (pr₁ (IH xs) (y , inhabitant⁻ B))
claim : Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ t y)
claim γ = pr₀ (pr₁ (pr₁ (IH xs) (y , inhabitant⁻ B)) γ)

case-∧-elim₁ : {Γ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ Γ) → Σ \(t : d⁺ (A ∧ B)) → (y : d⁻ (A ∧ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∧ B ∣ t y))
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y)
case-∧-elim₁ {Γ} A B IH xs = t , goal
where
t : d⁺ B
t = pr₁ (pr₀ (IH xs))
goal : (y : d⁻ B) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y)
goal y = rs , claim
where
rs : dd⁻ Γ
rs = pr₀ (pr₁ (IH xs) (inhabitant⁻ A , y))
claim : Prfᴬ (∥ Γ ∥ xs rs) (∣ B ∣ t y)
claim γ = pr₁ (pr₁ (pr₁ (IH xs) (inhabitant⁻ A , y)) γ)

case-⇒-intro : {Γ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y))
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ (A ⇒ B)) → (y : d⁻ (A ⇒ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t y)
case-⇒-intro {Γ} A B IH xs = t , goal
where
fxs' : d⁺ A → dd⁺ (Γ ₊ A)
fxs' ta zero = ta
fxs' _ (succ i) = xs i
t₀ : d⁺ A → d⁺ B
t₀ ta = pr₀ (IH (fxs' ta))
frs' : d⁺ A → d⁻ B → dd⁻ (Γ ₊ A)
frs' ta yb = pr₀ (pr₁ (IH (fxs' ta)) yb)
t₁ : d⁺ A → d⁻ B → d⁻ A
t₁ ta yb = (frs' ta yb) zero
t : d⁺ (A ⇒ B)
t = t₀ , t₁
goal : (y : d⁻ (A ⇒ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t y)
goal (ta , yb) = rs , claim₁
where
rs : dd⁻ Γ
rs = (frs' ta yb) ∘ succ
tb : d⁺ B
tb = pr₀ (IH (fxs' ta))
ya : d⁻ A
ya = (frs' ta yb) zero
claim₀ : Prfᴬ (∥ Γ ∥ xs rs × ∣ A ∣ ta ya) (∣ B ∣ tb yb)
claim₀ = pr₁ (pr₁ (IH (fxs' ta)) yb)
claim₁ : Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t (ta , yb))
claim₁ γ a = claim₀ (γ , a)

case-⇒-elim : {Γ : Asmpt} (A B : Prp)
→ ((xs : dd⁺ Γ) → Σ \(t : d⁺ (A ⇒ B)) → (y : d⁻ (A ⇒ B)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ A ⇒ B ∣ t y))
→ (xs : dd⁺ (Γ ₊ A)) → Σ \(t : d⁺ B) → (y : d⁻ B) → Σ \(rs : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs rs) (∣ B ∣ t y)
case-⇒-elim {Γ} A B IH xs' = tb , goal
where
xs : dd⁺ Γ
xs = xs' ∘ succ
t : d⁺ (A ⇒ B)
t = pr₀ (IH xs)
ta : d⁺ A
ta = xs' zero
tb : d⁺ B
tb = pr₀ t ta
goal : (yb : d⁻ B) → Σ \(rs' : dd⁻ (Γ ₊ A)) → Prfᴬ (∥ Γ ₊ A ∥ xs' rs') (∣ B ∣ tb yb)
goal yb = rs' , claim₁
where
ya : d⁻ A
ya = pr₁ t ta yb
y  : d⁻ (A ⇒ B)
y  = ta , yb
rs : dd⁻ Γ
rs = pr₀ (pr₁ (IH xs) y)
rs' : dd⁻ (Γ ₊ A)
rs' zero = ya
rs' (succ i) = rs i
claim₀ : Prfᴬ (∥ Γ ∥ xs rs) (∣ A ∣ ta ya → ∣ B ∣ tb yb)
claim₀ = pr₁ (pr₁ (IH xs) y)
claim₁ : Prfᴬ (∥ Γ ₊ A ∥ xs' rs') (∣ B ∣ tb yb)
claim₁ (γ , a) = claim₀ γ a

\end{code}

The cases of inference rules of quantifiers

\begin{code}

case-∀-intro : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp)
→ ((x : ⟦ σ ⟧) → (xs : dd⁺ Γ) → Σ \(t : d⁺ (φ x)) → (y : d⁻ (φ x)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ x ∣ t y))
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ (∀′ φ)) → (y : d⁻ (∀′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∀′ φ ∣ t y)
case-∀-intro {Γ} {σ} φ IH xs = t , goal
where
t : d⁺ (∀′ φ)
t x = pr₀ (IH x xs)
goal : (y : d⁻ (∀′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∀′ φ ∣ t y)
goal (a , y') = pr₁ (IH a xs) y'

case-∀-elim : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp)
→ ((xs : dd⁺ Γ) → Σ \(t : d⁺ (∀′ φ)) → (y : d⁻ (∀′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∀′ φ ∣ t y))
→ (a : ⟦ σ ⟧) → (xs : dd⁺ Γ) → Σ \(t : d⁺ (φ a)) → (y : d⁻ (φ a)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ a ∣ t y)
case-∀-elim {Γ} {σ} φ IH a xs = t , goal
where
t : d⁺ (φ a)
t = pr₀ (IH xs) a
goal : (y : d⁻ (φ a)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ a ∣ t y)
goal y = pr₁ (IH xs) (a , y)

case-∃-intro : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp)
→ (a : ⟦ σ ⟧) → ((xs : dd⁺ Γ) → Σ \(t : d⁺ (φ a)) → (y : d⁻ (φ a)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ a ∣ t y))
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ (∃′ φ)) → (y : d⁻ (∃′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∃′ φ ∣ t y)
case-∃-intro {Γ} {σ} φ a IH xs = t , goal
where
t : d⁺ (∃′ φ)
t = a , pr₀ (IH xs)
goal : (y : d⁻ (∃′ φ)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ ∃′ φ ∣ t y)
goal y = pr₁ (IH xs) (y a (pr₀ (IH xs)))

case-∃-elim : {Γ : Asmpt} {σ : Ty} (φ : ⟦ σ ⟧ → Prp) (A : Prp)
→ ((x : ⟦ σ ⟧) → (xs : dd⁺ Γ) → Σ \(t : d⁺ (φ x ⇒ A)) → (y : d⁻ (φ x ⇒ A)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ φ x ⇒ A ∣ t y))
→ (xs : dd⁺ Γ) → Σ \(t : d⁺ ((∃′ φ) ⇒ A)) → (y : d⁻ ((∃′ φ) ⇒ A)) → Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ (∃′ φ) ⇒ A ∣ t y)
case-∃-elim {Γ} {σ} φ A IH xs = t , goal
where
t₀ : (Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)) → d⁺ A
t₀ (x , w) = pr₀ (pr₀ (IH x xs)) w
t₁ : (Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)) → d⁻ A → (x : ⟦ σ ⟧) → d⁺ (φ x) → d⁻ (φ x)
t₁ _ y x w = pr₁ (pr₀ (IH x xs)) w y
t : d⁺ ((∃′ φ) ⇒ A)
t = t₀ , t₁
goal : (y : (Σ \(x : ⟦ σ ⟧) → d⁺ (φ x)) × d⁻ A)
→ Σ \(rs : dd⁻ Γ) → Prfᴬ (∥ Γ ∥ xs rs) (∣ (∃′ φ) ⇒ A ∣ t y)
goal ((x , w) , y) = pr₁ (IH x xs) (w , y)

\end{code}

The case of the induction principle (in empty assumption)

\begin{code}

ICond : (ℕ → Prp) → Prp
ICond φ = ∀′ (λ n → φ n ⇒ φ (succ n))

case-ind : (φ : ℕ → Prp)
→ ((_ : dd⁺ ε) → Σ \(t : d⁺ (φ 0)) → (y : d⁻ (φ 0)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ φ 0 ∣ t y))
→ ((_ : dd⁺ ε) → Σ \(t : d⁺ (ICond φ)) → (y : d⁻ (ICond φ)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ ICond φ ∣ t y))
→ (_ : dd⁺ ε) → Σ \(t : d⁺ (∀′ φ)) → (y : d⁻ (∀′ φ)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ ∀′ φ ∣ t y)
case-ind φ IH₀ IH₁ _ = t , uncurry goal -- I have to do this, otherwise Agda doesn't believe its termination.
where
t0 : d⁺ (φ 0)
t0 = pr₀ (IH₀ (λ()))
ts : (n : ℕ) → d⁺ (φ n) → d⁺ (φ (succ n))
ts n tn = pr₀ (pr₀ (IH₁ (λ())) n) tn
t : d⁺ (∀′ φ)
t 0 = t0
t (succ n) = ts n (t n)
goal : (n : ℕ) → (yn : d⁻ (φ n)) → Σ \(_ : dd⁻ ε) → Prfᴬ 𝟙 (∣ ∀′ φ ∣ t (n , yn))
goal 0 y0 = (λ()) , pr₁ (pr₁ (IH₀ (λ())) y0)
goal (succ n) ysn = (λ()) , claim₂
where
tn : d⁺ (φ n)
tn = t n
fy : (n : ℕ) → d⁺ (φ n) → d⁻ (φ (succ n)) → d⁻ (φ n)
fy n = pr₁ (pr₀ (IH₁ (λ())) n)
yn : d⁻ (φ n)
yn = fy n tn ysn
tsn : d⁺ (φ (succ n))
tsn = t (succ n)
claim₀ : Prfᴬ 𝟙 (∣ φ n ∣ tn yn)
claim₀ = pr₁ (goal n yn)
claim₁ : Prfᴬ 𝟙 (∣ φ n ∣ tn yn → ∣ φ (succ n) ∣ tsn ysn)
claim₁ = pr₁ (pr₁ (IH₁ (λ())) (n , tn , ysn))
claim₂ : Prfᴬ 𝟙 (∣ φ (succ n) ∣ tsn ysn)
claim₂ ⋆ = claim₁ ⋆ (claim₀ ⋆)

\end{code}

Finally we use the above to prove Thm[soundness].

\begin{code}

Thm[soundness] refl = case-refl
Thm[soundness] (J {σ} φ base {a} {b} p) = case-J φ (λ x → Thm[soundness] (base x)) (Thm[soundness] p)
Thm[soundness] (id {A}) = case-id A
Thm[soundness] (wkn {A = A} {B = B} p) = case-wkn A B (Thm[soundness] p)
Thm[soundness] (cut {A = A} {B = B} p q) = case-cut A B (Thm[soundness] p) (Thm[soundness] q)
Thm[soundness] (swap {Γ} Δ {A} {B} {C} p) = case-swap Γ Δ A B C (Thm[soundness] p)
Thm[soundness] (∧-intro {A = A} {B = B} p q) = case-∧-intro A B (Thm[soundness] p) (Thm[soundness] q)
Thm[soundness] (∧-elim₀ {A = A} {B = B} p) = case-∧-elim₀ A B (Thm[soundness] p)
Thm[soundness] (∧-elim₁ {A = A} {B = B} p) = case-∧-elim₁ A B (Thm[soundness] p)
Thm[soundness] (⇒-intro {A = A} {B = B} p) = case-⇒-intro A B (Thm[soundness] p)
Thm[soundness] (⇒-elim {A = A} {B = B} p) = case-⇒-elim A B (Thm[soundness] p)
Thm[soundness] (∀-intro {φ = φ} f) = case-∀-intro φ (λ x → Thm[soundness] (f x))
Thm[soundness] (∀-elim {φ = φ} p a) = case-∀-elim φ (Thm[soundness] p) a
Thm[soundness] (∃-intro {φ = φ} a p) = case-∃-intro φ a (Thm[soundness] p)
Thm[soundness] (∃-elim {φ = φ} {A = A} f) = case-∃-elim φ A (λ x → Thm[soundness] (f x))
Thm[soundness] (ind φ base ih) = case-ind φ (Thm[soundness] base) (Thm[soundness] ih)

\end{code}

Work in progress include