=============================================
 =                                           =
 =  Gödel's System T with products and sums  =
 =                                           =
 =============================================

    Chuangjie Xu, July 2019

\begin{code}

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

module Tplus where

open import Preliminaries

\end{code}

■ Types, contexts and terms of T

Here we work with the lambda-calculus version of system T, and with de
Bruijn indices instead of variables.  We also extend T with product
and coproduct types.

\begin{code}

infixr  _⊠_
infixr  _⊞_
infixr  _⇾_
infixl  _₊_
infixl  _·_

--
-- finite types
--
data Ty : Set where
 ι           : Ty
 _⊠_ _⊞_ _⇾_ : Ty → Ty → Ty

--
-- contexts as finite lists of types
--
data Cxt : Set where
 ε   : Cxt
 _₊_ : Cxt → Ty → Cxt

--
-- indices of types/variables in context
--
data ∥_∈_∥ (σ : Ty) : Cxt → Set where
 zero : {Γ : Cxt} → ∥ σ ∈ (Γ ₊ σ) ∥
 succ : {τ : Ty} {Γ : Cxt} → ∥ σ ∈ Γ ∥ → ∥ σ ∈ Γ ₊ τ ∥

--
-- terms
--
data T (Γ : Cxt) : Ty → Set where
 Var  : {σ : Ty} → ∥ σ ∈ Γ ∥ → T Γ σ
 Lam  : {σ τ : Ty} → T (Γ ₊ σ) τ → T Γ (σ ⇾ τ)
 _·_  : {σ τ : Ty} → T Γ (σ ⇾ τ) → T Γ σ → T Γ τ
 Zero : T Γ ι
 Succ : T Γ (ι ⇾ ι)
 Rec  : {σ : Ty} → T Γ (σ ⇾ (ι ⇾ σ ⇾ σ) ⇾ ι ⇾ σ)
 Pair : {σ τ : Ty} → T Γ (σ ⇾ τ ⇾ σ ⊠ τ)
 Pr1  : {σ τ : Ty} → T Γ (σ ⊠ τ ⇾ σ)
 Pr2  : {σ τ : Ty} → T Γ (σ ⊠ τ ⇾ τ)
 Inj1 : {σ τ : Ty} → T Γ (σ ⇾ σ ⊞ τ)
 Inj2 : {σ τ : Ty} → T Γ (τ ⇾ σ ⊞ τ)
 Case : {ρ σ τ : Ty} → T Γ ((σ ⇾ ρ) ⇾ (τ ⇾ ρ) ⇾ σ ⊞ τ ⇾ ρ)

\end{code}

■ The standard interpretation of T into Agda

\begin{code}

⟦_⟧ʸ : Ty → Set
⟦ ι ⟧ʸ     = ℕ
⟦ σ ⊠ τ ⟧ʸ = ⟦ σ ⟧ʸ × ⟦ τ ⟧ʸ
⟦ σ ⊞ τ ⟧ʸ = ⟦ σ ⟧ʸ + ⟦ τ ⟧ʸ
⟦ σ ⇾ τ ⟧ʸ = ⟦ σ ⟧ʸ → ⟦ τ ⟧ʸ

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

_₍_₎ : {Γ : Cxt} {ρ : Ty} → ⟦ Γ ⟧ˣ → ∥ ρ ∈ Γ ∥ → ⟦ ρ ⟧ʸ
(_ , a) ₍ zero ₎   = a
(γ , _) ₍ succ i ₎ = γ ₍ i ₎

⟦_⟧ᵐ : {Γ : Cxt} {σ : Ty} → T Γ σ → ⟦ Γ ⟧ˣ → ⟦ σ ⟧ʸ
⟦ Var i ⟧ᵐ γ = γ ₍ i ₎
⟦ Lam t ⟧ᵐ γ = λ a → ⟦ t ⟧ᵐ (γ , a)
⟦ f · a ⟧ᵐ γ = ⟦ f ⟧ᵐ γ (⟦ a ⟧ᵐ γ)
⟦ Zero ⟧ᵐ  _ = 
⟦ Succ ⟧ᵐ  _ = succ
⟦ Rec ⟧ᵐ   _ = rec
⟦ Pair ⟧ᵐ  _ = _,_
⟦ Pr1 ⟧ᵐ   _ = pr₁
⟦ Pr2 ⟧ᵐ   _ = pr₂
⟦ Inj1 ⟧ᵐ  _ = inl
⟦ Inj2 ⟧ᵐ  _ = inr
⟦ Case ⟧ᵐ  _ = case

⟦_⟧ : {ρ : Ty} → T ε ρ → ⟦ ρ ⟧ʸ
⟦ t ⟧ = ⟦ t ⟧ᵐ ⋆

--
-- An (Agda) element a is "T-definable" if one can find a closed T
-- term whose standard interpretation is a.
--
T-definable : {ρ : Ty} → ⟦ ρ ⟧ʸ → Set
T-definable {ρ} a = Σ \(t : T ε ρ) → ⟦ t ⟧ ≡ a

\end{code}

■ Some auxiliaries

\begin{code}

ν₀ : {Γ : Cxt} {ρ : Ty} → T (Γ ₊ ρ) ρ
ν₀ = Var zero

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

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

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

Max : {Γ : Cxt} → T Γ (ι ⇾ ι ⇾ ι)
Max = Rec · Lam ν₀ · Lam (Lam (Rec · (Succ · ν₁) · Lam (Lam (Succ · (ν₂ · ν₁)))))

max : ℕ → ℕ → ℕ
max = ⟦ Max ⟧

Max-spec₀ : (n m : ℕ) → n ≤ max n m
Max-spec₀          m       = ≤zero
Max-spec₀ (succ n)         = ≤refl
Max-spec₀ (succ n) (succ m) = ≤succ (Max-spec₀ n m)

Max-spec₁ : (n m : ℕ) → m ≤ max n m
Max-spec₁          m       = ≤refl
Max-spec₁ (succ n)         = ≤zero
Max-spec₁ (succ n) (succ m) = ≤succ (Max-spec₁ n m)

\end{code}

■ Weakening

\begin{code}

infix  _⊆_

_⊆_ : Cxt → Cxt → Set
Γ ⊆ Δ = ∀{ρ} → ∥ ρ ∈ Γ ∥ → ∥ ρ ∈ Δ ∥

⊆-cons : {Γ Δ : Cxt} {ρ : Ty}
       → Γ ⊆ Δ → Γ ₊ ρ ⊆ Δ ₊ ρ
⊆-cons ξ  zero    = zero
⊆-cons ξ (succ i) = succ (ξ i)

wk : {Γ Δ : Cxt} {ρ : Ty} → Γ ⊆ Δ → T Γ ρ → T Δ ρ
wk ξ (Var i) = Var (ξ i)
wk ξ (Lam t) = Lam (wk (⊆-cons ξ) t)
wk ξ (f · a) = wk ξ f · wk ξ a
wk ξ Zero    = Zero
wk ξ Succ    = Succ
wk ξ Rec     = Rec
wk ξ Pair    = Pair
wk ξ Pr1     = Pr1
wk ξ Pr2     = Pr2
wk ξ Inj1    = Inj1
wk ξ Inj2    = Inj2
wk ξ Case    = Case

wkn : {Γ : Cxt} {σ ρ : Ty} → T Γ ρ → T (Γ ₊ σ) ρ
wkn = wk succ

\end{code}