Chuangjie Xu, 2013

This corresponds to part of Section 4.2 of the paper
http://www.cs.bham.ac.uk/~mhe/papers/kleene-kreisel.pdf

We borrow the definition of the lambda calculus version of system T
from Martin Escardo's Agda proof of Continuity of Godel's system T
functionals via effectful forcing, which is available on

http://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-lambda.html.

\begin{code}

module T where

open import MiniLibrary
open import Sequence
open import Space
open import Space-product
open import Space-exponential
open import Space-discrete
open import Inequality
open import UniformContinuity
open import Fan


infixl  _₊_

\end{code}

Vectors - to represent contexts:

\begin{code}

data _^_ (X : Set) : ℕ → Set where
 ε : X ^ 
 _₊_ : {n : ℕ} → X ^ n → X → X ^ (succ n)

\end{code}

Index function of vectors:

\begin{code}

_₍_₎ : {X : Set} {n : ℕ} → X ^ n → Fin n → X
(xs ₊ x) ₍ zero ₎   = x
(xs ₊ x) ₍ succ i ₎ = xs ₍ i ₎

infixr  _⇨_

\end{code}

Types of system T:

\begin{code}

data Ty : Set where
 ② : Ty
 Ⓝ : Ty
 _⇨_ : Ty → Ty → Ty

\end{code}

Contexts of system T:

\begin{code}

Cxt : ℕ → Set
Cxt n = Ty ^ n

infixl  _∙_

\end{code}

Terms in context of system T
with an extended constant for the Fan functional.

\begin{code}

data Tm : {n : ℕ} → Cxt n → Ty → Set where
 ⊥    : {n : ℕ}{Γ : Cxt n}           → Tm Γ ②
 ⊤    : {n : ℕ}{Γ : Cxt n}           → Tm Γ ②
 IF   : {n : ℕ}{Γ : Cxt n}{σ : Ty}   → Tm Γ (σ ⇨ σ ⇨ ② ⇨ σ)
 ZERO : {n : ℕ}{Γ : Cxt n}           → Tm Γ Ⓝ
 SUCC : {n : ℕ}{Γ : Cxt n}           → Tm Γ (Ⓝ ⇨ Ⓝ)
 REC  : {n : ℕ}{Γ : Cxt n}{σ : Ty}   → Tm Γ (σ ⇨ (Ⓝ ⇨ σ ⇨ σ) ⇨ Ⓝ ⇨ σ)
 VAR  : {n : ℕ}{Γ : Cxt n}           → (i : Fin n) → Tm Γ (Γ ₍ i ₎)
 LAM  : {n : ℕ}{Γ : Cxt n}{σ τ : Ty} → Tm (Γ ₊ σ) τ → Tm Γ (σ ⇨ τ)
 _∙_  : {n : ℕ}{Γ : Cxt n}{σ τ : Ty} → Tm Γ (σ ⇨ τ) → Tm Γ σ → Tm Γ τ
 FAN  : {n : ℕ}{Γ : Cxt n}           → Tm Γ (((Ⓝ ⇨ ②) ⇨ Ⓝ) ⇨ Ⓝ)


infix   _==_
infixr  _→→_
infixl  _∧∧_

\end{code}

Logic of system T.
Atoms are equations over T terms.

\begin{code}

data Fml : {n : ℕ} → Cxt n → Set where
 _==_ : {n : ℕ}{Γ : Cxt n}{σ : Ty} → Tm Γ σ → Tm Γ σ → Fml Γ
 _∧∧_ : {n : ℕ}{Γ : Cxt n}         → Fml Γ  → Fml Γ  → Fml Γ
 _→→_ : {n : ℕ}{Γ : Cxt n}         → Fml Γ  → Fml Γ  → Fml Γ

\end{code}