Martin Escardo 2011.

Our Spartan (intensional) Martin-LΓΆf type theory has a countable tower
of universes, the empty type β, the unit type π, product types Ξ , sum
types Ξ£ (and hence binary product types _Γ_), sum types _+_.
identity types _β‘_.

\begin{code}

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

module SpartanMLTT where

open import Universes public

\end{code}

The module Universes allows us to write e.g. the following instead of

Ξ  : β {i j} {X : Set i} (Y : X β Set j) β Set (i β j)
Ξ  Y = (x : _) β Y x

\begin{code}

Ξ  : β {U V} {X : U Μ} (Y : X β V Μ) β U β V Μ
Ξ  Y = (x : _) β Y x

syntax Ξ  {A} (Ξ» x β B) = Ξ οΌ x βΆ A οΌ, B

\end{code}

Identity and dependent function composition:

\begin{code}

id : β {U} {X : U Μ} β X β X
id x = x

_β_ : β {U V W} {X : U Μ} {Y : V Μ} {Z : Y β W Μ}
β Ξ  Z β (f : X β Y) β Ξ  (Ξ» x β Z (f x))
g β f = Ξ» x β g(f x)

\end{code}

Empty type.

\begin{code}

data π {U} : U Μ where

unique-from-π : β {U V} {A : U Μ} β π {V} β A
unique-from-π = Ξ» ()

π-elim = unique-from-π

\end{code}

The one-element type is defined by induction with one case:

\begin{code}

data π {U} : U Μ where
* : π

unique-to-π : β {U V} {A : U Μ} β A β π {V}
unique-to-π {U} {V} a = * {V}

\end{code}

Using our conventions below, a sum can be written Ξ£ {X} Y or as
Ξ£ \(x : X) β Y x, or even Ξ£ \x β Y x when Agda can infer the type of
the element x from the context. I prefer to use \ rather than Ξ» in
such cases.

\begin{code}

record Ξ£ {U V} {X : U Μ} (Y : X β V Μ) : U β V Μ where
constructor _,_
field
prβ : X
prβ : Y prβ

open Ξ£ public

syntax Ξ£ {A} (Ξ» x β B) = Ξ£οΌ x βΆ A οΌ, B

Ξ£-elim : β {U V} {X : U Μ} {Y : X β V Μ} {A : Ξ£ Y β U β V Μ}
β ((x : X) (y : Y x) β A (x , y)) β Ξ  A
Ξ£-elim f (x , y) = f x y

uncurry : β {U V W} {X : U Μ} {Y : X β V Μ} {Z : W Μ}
β ((x : X) β Y x β Z) β Ξ£ Y β Z
uncurry f (x , y) = f x y

curry :  β {U V W} {X : U Μ} {Y : X β V Μ} {Z : W Μ}
β (Ξ£ Y β Z) β ((x : X) β Y x β Z)
curry f x y = f (x , y)

\end{code}

Equivalently, Ξ£-elim f t = f (prβ t) (prβ t).

As usual in type theory, binary products are particular cases of
dependent sums.

\begin{code}

_Γ_ : β {U V} β U Μ β V Μ β U β V Μ
X Γ Y = Ξ£ \(x : X) β Y

\end{code}

Binary sums

\begin{code}

data _+_ {U V} (X : U Μ) (Y : V Μ) : U β V Μ where
inl : X β X + Y
inr : Y β X + Y

dep-cases : β {U V W} {X : U Μ} {Y : V Μ} {A : X + Y β W Μ}
β ((x : X) β A(inl x))
β ((y : Y) β A(inr y))
β ((z : X + Y) β A z)
dep-cases f g (inl x) = f x
dep-cases f g (inr y) = g y

cases : β {U V W} {X : U Μ} {Y : V Μ} {A : W Μ} β (X β A) β (Y β A) β X + Y β A
cases = dep-cases

Cases : β {U V W} {X : U Μ} {Y : V Μ} {A : W Μ} β X + Y β (X β A) β (Y β A) β A
Cases z f g = cases f g z

+-commutative : β {U V} {A : U Μ} {B : V Μ} β A + B β B + A
+-commutative = cases inr inl

\end{code}

Some basic Curry--Howard logic.

\begin{code}

Β¬_ : β {U} β U Μ β U Μ
Β¬ A = A β π {Uβ}

decidable : β {U} β U Μ β U Μ
decidable A = A + Β¬ A

_β_ : β {U V} β U Μ β V Μ β U β V Μ
A β B = (A β B) Γ (B β A)

dual : β {U V W} {X : U Μ} {Y : V Μ} (R : W Μ) β (X β Y) β (Y β R) β (X β R)
dual R f p = p β f

contrapositive : β {U V} {A : U Μ} {B : V Μ} β (A β B) β Β¬ B β Β¬ A
contrapositive = dual _

Β¬Β¬ : β {U} β U Μ β U Μ
Β¬Β¬ A = Β¬(Β¬ A)

Β¬Β¬-functor : β {U V} {A : U Μ} {B : V Μ} β (A β B) β Β¬Β¬ A β Β¬Β¬ B
Β¬Β¬-functor = contrapositive β contrapositive

double-negation-intro : β {U} {A : U Μ} β A β Β¬Β¬ A
double-negation-intro x u = u x

three-negations-imply-one : β {U} {A : U Μ} β Β¬(Β¬Β¬ A) β Β¬ A
three-negations-imply-one = contrapositive double-negation-intro

double-negation-unshift : β {U V} {X : U Μ} {A : X β V Μ} β Β¬Β¬((x : X) β A x) β (x : X) β Β¬Β¬(A x)
double-negation-unshift f x g = f (Ξ» h β g (h x))

dnu : β {U} {V} {A : U Μ} {B : V Μ} β Β¬Β¬(A Γ B) β Β¬Β¬ A Γ Β¬Β¬ B
dnu Ο = (Β¬Β¬-functor prβ Ο) , (Β¬Β¬-functor prβ Ο)

und : β {U} {V} {A : U Μ} {B : V Μ} β Β¬Β¬ A Γ Β¬Β¬ B β Β¬Β¬(A Γ B)
und (Ο , Ξ³) w = Ξ³ (Ξ» y β Ο (Ξ» x β w (x , y)))

not-Ξ£-implies-Ξ -not : β {U V} {X : U Μ} {A : X β V Μ}
β Β¬(Ξ£ \(x : X) β A x) β (x : X) β Β¬(A x)
not-Ξ£-implies-Ξ -not = curry

Ξ -not-implies-not-Ξ£ : β {U} {X : U Μ} {A : X β U Μ}
β ((x : X) β Β¬(A x)) β Β¬(Ξ£ \(x : X) β A x)
Ξ -not-implies-not-Ξ£ = uncurry

Left-fails-then-right-holds : β {U} {V} {P : U Μ} {Q : V Μ} β P + Q β Β¬ P β Q
Left-fails-then-right-holds (inl p) u = π-elim (u p)
Left-fails-then-right-holds (inr q) u = q

Right-fails-then-left-holds : β {U} {V} {P : U Μ} {Q : V Μ} β P + Q β Β¬ Q β P
Right-fails-then-left-holds (inl p) u = p
Right-fails-then-left-holds (inr q) u = π-elim (u q)

\end{code}

Equality (more in the module UF).

\begin{code}

data _β‘_ {U} {X : U Μ} : X β X β U Μ where
refl : {x : X} β x β‘ x

Id : β {U} {X : U Μ} β X β X β U Μ
Id = _β‘_

_β’_ : β {U} {X : U Μ} β (x y : X) β U Μ
x β’ y = Β¬(x β‘ y)

Jbased : β {U V} {X : U Μ} (x : X) (A : (y : X) β x β‘ y β V Μ)
β A x refl β (y : X) (r : x β‘ y) β A y r
Jbased x A b .x refl = b

J : β {U V} {X : U Μ} (A : (x y : X) β x β‘ y β V Μ)
β ((x : X) β A x x refl) β {x y : X} (r : x β‘ y) β A x y r
J A f {x} {y} = Jbased x (Ξ» y p β A x y p) (f x) y

transport' : β {U V} {X : U Μ} (A : X β V Μ) {x y : X}
β x β‘ y β A x β A y
transport' A {x} {y} p a = Jbased x (Ξ» y p β A y) a y p

transport : β {U V} {X : U Μ} (A : X β V Μ) {x y : X}
β x β‘ y β A x β A y
transport A refl = id

_β_ : β {U} {X : U Μ} β {x y z : X} β x β‘ y β y β‘ z β x β‘ z
p β q = transport (Id _) q p

_β»ΒΉ : β {U} {X : U Μ} β {x y : X} β x β‘ y β y β‘ x
p β»ΒΉ = transport (Ξ» x β x β‘ _) p refl

ap : β {U V} {X : U Μ} {Y : V Μ} (f : X β Y) {x x' : X} β x β‘ x' β f x β‘ f x'
ap f p = transport (Ξ» x' β f _ β‘ f x') p refl

back-transport : β {U V} {X : U Μ} (A : X β V Μ) {x y : X} β x β‘ y β A y β A x
back-transport B p = transport B (p β»ΒΉ)

β’-sym : β {U} {X : U Μ} β {x y : X} β x β’ y β y β’ x
β’-sym u r = u(r β»ΒΉ)

\end{code}

Some general definitions (perhaps we need to find a better place for
this):

\begin{code}

Nat : β {U V W} {X : U Μ} β (X β V Μ) β (X β W Μ) β U β V β W Μ
Nat A B = Ξ  \x β A x β B x

_βΌ_ : β {U V} {X : U Μ} {A : X β V Μ} β Ξ  A β Ξ  A β U β V Μ
f βΌ g = β x β f x β‘ g x

_β_ : β {U V} {X : U Μ} {x : X} {A : X β V Μ} β Nat (Id x) A β Nat (Id x) A β U β V Μ
Ξ· β ΞΈ = β y β Ξ· y βΌ ΞΈ y

NatΞ£ : β {U V W} {X : U Μ} {A : X β V Μ} {B : X β W Μ} β Nat A B β Ξ£ A β Ξ£ B
NatΞ£ ΞΆ (x , a) = (x , ΞΆ x a)

NatΞ  : β {U V W} {X : U Μ} {A : X β V Μ} {B : X β W Μ} β Nat A B β Ξ  A β Ξ  B
NatΞ  f g x = f x (g x) -- (S combinator from combinatory logic!)

left-cancellable : β {U V} {X : U Μ} {Y : V Μ} β (X β Y) β U β V Μ
left-cancellable f = β {x x'} β f x β‘ f x' β x β‘ x'

left-cancellable' : β {U V} {X : U Μ} {Y : V Μ} β (X β Y) β U β V Μ
left-cancellable' f = β x x' β f x β‘ f x' β x β‘ x'

\end{code}

Standard syntax for equality chain reasoning:

\begin{code}

_β‘β¨_β©_ : β {U} {X : U Μ} (x : X) {y z : X} β x β‘ y β y β‘ z β x β‘ z
_ β‘β¨ p β© q = p β q

_β : β {U} {X : U Μ} β (x : X) β x β‘ x
_β _ = refl

\end{code}

The following is properly proved using universes, but we don't both at
the moment:

\begin{code}

+disjoint : β {U V} {X : U Μ} {Y : V Μ} {x : X} {y : Y} β Β¬(inl x β‘ inr y)
+disjoint ()

+disjoint' : β {U V} {X : U Μ} {Y : V Μ} {x : X} {y : Y} β Β¬(inr y β‘ inl x)
+disjoint' ()

inl-lc : β {U V} {X : U Μ} {Y : V Μ} {x x' : X} β inl {U} {V} {X} {Y} x β‘ inl x' β x β‘ x'
inl-lc refl = refl

inr-lc : β {U V} {X : U Μ} {Y : V Μ} {y y' : Y} β inr {U} {V} {X} {Y} y β‘ inr y' β y β‘ y'
inr-lc refl = refl

\end{code}

\begin{code}

π-all-* : β {U} (x : π) β x β‘ *
π-all-* {U} * = refl {U}

equality-cases : β {U V W} {X : U Μ} {Y : V Μ} {A : W Μ} (z : X + Y)
β ((x : X) β z β‘ inl x β A) β ((y : Y) β z β‘ inr y β A) β A
equality-cases (inl x) f g = f x refl
equality-cases (inr y) f g = g y refl

\end{code}

General utilities to avoid (sometimes) mentionint implicit arguments
in function definitions.

\begin{code}

typeOf : β {U} {X : U Μ} β X β U Μ
typeOf {U} {X} x = X

universeOf : β {U} (X : U Μ) β Universe
universeOf {U} X = U

domain dom : β {U V} {X : U Μ} {Y : V Μ} β (X β Y) β U Μ
domain {U} {V} {X} {Y} f = X
dom = domain

codomain cod : β {U V} {X : U Μ} {Y : V Μ} β (X β Y) β V Μ
codomain {U} {V} {X} {Y} f = Y
cod = codomain

\end{code}

The two-point type (or booleans)

\begin{code}

data π : Uβ Μ where
β : π
β : π

π-possibilities : (b : π) β (b β‘ β) + (b β‘ β)
π-possibilities β = inl refl
π-possibilities β = inr refl

zero-is-not-one : β β’ β
zero-is-not-one ()

π-induction : β {U} {A : π β U Μ} β A β β A β β (x : π) β A x
π-induction r s β = r
π-induction r s β = s

π-cases : β {U} {A : U Μ} β A β A β π β A
π-cases = π-induction

π-equality-cases : β {U} {A : U Μ} {b : π} β (b β‘ β β A) β (b β‘ β β A) β A
π-equality-cases {U} {A} {β} fβ fβ = fβ refl
π-equality-cases {U} {A} {β} fβ fβ = fβ refl

two-equality-cases' : β {U} {Aβ Aβ : U Μ} {b : π} β (b β‘ β β Aβ) β (b β‘ β β Aβ) β Aβ + Aβ
two-equality-cases' {U} {Aβ} {Aβ} {β} fβ fβ = inl(fβ refl)
two-equality-cases' {U} {Aβ} {Aβ} {β} fβ fβ = inr(fβ refl)

Lemma[bβ‘ββbβ’β] : {b : π} β b β‘ β β b β’ β
Lemma[bβ‘ββbβ’β] r s = zero-is-not-one (s β»ΒΉ β r)

Lemma[bβ’ββbβ‘β] : {b : π} β b β’ β β b β‘ β
Lemma[bβ’ββbβ‘β] f = π-equality-cases (π-elim β f) (Ξ» r β r)

Lemma[bβ’ββbβ‘β] : {b : π} β b β’ β β b β‘ β
Lemma[bβ’ββbβ‘β] f = π-equality-cases (Ξ» r β r) (π-elim β f)

Lemma[bβ‘ββbβ’β] : {b : π} β b β‘ β β b β’ β
Lemma[bβ‘ββbβ’β] r s = zero-is-not-one (r β»ΒΉ β s)

Lemma[[aβ‘ββbβ‘β]βbβ‘ββaβ‘β] : {a b : π} β (a β‘ β β b β‘ β) β b β‘ β β a β‘ β
Lemma[[aβ‘ββbβ‘β]βbβ‘ββaβ‘β] f = Lemma[bβ’ββbβ‘β] β (contrapositive f) β Lemma[bβ‘ββbβ’β]

Lemma[[aβ‘ββbβ‘β]βbβ‘ββaβ‘β] : {a b : π} β (a β‘ β β b β‘ β) β b β‘ β β a β‘ β
Lemma[[aβ‘ββbβ‘β]βbβ‘ββaβ‘β] f = Lemma[bβ’ββbβ‘β] β (contrapositive f) β Lemma[bβ‘ββbβ’β]

\end{code}

π-Characteristic function of equality on π:

\begin{code}

complement : π β π
complement β = β
complement β = β

complement-involutive : (b : π) β complement(complement b) β‘ b
complement-involutive β = refl
complement-involutive β = refl

eqπ : π β π β π
eqπ β n = complement n
eqπ β n = n

eqπ-equal : (m n : π) β eqπ m n β‘ β β m β‘ n
eqπ-equal β n p = ap complement (p β»ΒΉ) β complement-involutive n
eqπ-equal β n p = p β»ΒΉ

equal-eqπ : (m n : π) β m β‘ n β eqπ m n β‘ β
equal-eqπ β β refl = refl
equal-eqπ β β refl = refl

\end{code}

Alternative coproduct:

\begin{code}

_+'_ : β {U} β U Μ β U Μ β U Μ
Xβ +' Xβ = Ξ£ \(i : π) β X i
where
X : π β _ Μ
X β = Xβ
X β = Xβ

\end{code}

Natural order of binary numbers:

\begin{code}

_<β_ : (a b : π) β Uβ Μ
a <β b = (a β‘ β) Γ (b β‘ β)

_β€β_ : (a b : π) β Uβ Μ
a β€β b = a β‘ β β b β‘ β

<β-coarser-than-β€β : {a b : π} β a <β b β a β€β b
<β-coarser-than-β€β (refl , refl) _ = refl

β-top : {b : π} β b β€β β
β-top r = refl

β-bottom : {b : π} β β β€β b
β-bottom ()

_β€β'_ : (a b : π) β Uβ Μ
a β€β' b = b β‘ β β a β‘ β

β€β-coarser-than-β€β' : {a b : π} β a β€β b β a β€β' b
β€β-coarser-than-β€β' {β} {b} f p = refl
β€β-coarser-than-β€β' {β} {β} f p = (f refl)β»ΒΉ
β€β-coarser-than-β€β' {β} {β} f p = p

β€β'-coarser-than-β€β : {a b : π} β a β€β' b β a β€β b
β€β'-coarser-than-β€β {β} {β} f p = p
β€β'-coarser-than-β€β {β} {β} f p = refl
β€β'-coarser-than-β€β {β} {β} f p = (f refl)β»ΒΉ
β€β'-coarser-than-β€β {β} {β} f p = p

β€β-anti : {a b : π} β a β€β b β b β€β a β a β‘ b
β€β-anti {β} {β} f g = refl
β€β-anti {β} {β} f g = g refl
β€β-anti {β} {β} f g = β€β-coarser-than-β€β' f refl
β€β-anti {β} {β} f g = refl

β-maximal : {b : π} β β β€β b β b β‘ β
β-maximal = β€β-anti β-top

_β₯β_ : (a b : π) β Uβ Μ
a β₯β b = b β€β a

minπ : π β π β π
minπ β b = β
minπ β b = b

Lemma[minabβ€βa] : {a b : π} β minπ a b β€β a
Lemma[minabβ€βa] {β} {b} r = π-elim(Lemma[bβ‘ββbβ’β] r refl)
Lemma[minabβ€βa] {β} {b} r = refl

Lemma[minabβ€βb] : {a b : π} β minπ a b β€β b
Lemma[minabβ€βb] {β} {b} r = π-elim(Lemma[bβ‘ββbβ’β] r refl)
Lemma[minabβ€βb] {β} {b} r = r

Lemma[minπabβ‘ββbβ‘β] : {a b : π} β minπ a b β‘ β β b β‘ β
Lemma[minπabβ‘ββbβ‘β] {β} {β} r = r
Lemma[minπabβ‘ββbβ‘β] {β} {β} r = refl
Lemma[minπabβ‘ββbβ‘β] {β} {β} r = r
Lemma[minπabβ‘ββbβ‘β] {β} {β} r = refl

Lemma[minπabβ‘ββaβ‘β]  : {a b : π} β minπ a b β‘ β β a β‘ β
Lemma[minπabβ‘ββaβ‘β] {β} r = r
Lemma[minπabβ‘ββaβ‘β] {β} r = refl

Lemma[aβ‘ββbβ‘ββminπabβ‘β] : {a b : π} β a β‘ β β b β‘ β β minπ a b β‘ β
Lemma[aβ‘ββbβ‘ββminπabβ‘β] {β} {β} p q = q
Lemma[aβ‘ββbβ‘ββminπabβ‘β] {β} {β} p q = p
Lemma[aβ‘ββbβ‘ββminπabβ‘β] {β} {β} p q = q
Lemma[aβ‘ββbβ‘ββminπabβ‘β] {β} {β} p q = refl

Lemma[aβ€βbβminπabβ‘a] : {a b : π} β a β€β b β minπ a b β‘ a
Lemma[aβ€βbβminπabβ‘a] {β} {b} p = refl
Lemma[aβ€βbβminπabβ‘a] {β} {b} p = p refl

lemma[minπabβ‘β] : {a b : π} β minπ a b β‘ β β (a β‘ β) + (b β‘ β)
lemma[minπabβ‘β] {β} {b} p = inl p
lemma[minπabβ‘β] {β} {b} p = inr p

maxπ : π β π β π
maxπ β b = b
maxπ β b = β

maxπ-lemma : (a b : π) β maxπ a b β‘ β β (a β‘ β) + (b β‘ β)
maxπ-lemma β b r = inr r
maxπ-lemma β b r = inl refl

maxπ-lemma-converse : (a b : π) β (a β‘ β) + (b β‘ β) β maxπ a b β‘ β
maxπ-lemma-converse β b (inl r) = unique-from-π (zero-is-not-one r)
maxπ-lemma-converse β b (inr r) = r
maxπ-lemma-converse β b x = refl

\end{code}

\begin{code}

_β_ : π β π β π
β β x = x
β β x = complement x

complement-of-eqπ-is-β : (m n : π) β complement(eqπ m n) β‘ m β n
complement-of-eqπ-is-β β n = complement-involutive n
complement-of-eqπ-is-β β n = refl

Lemma[bβbβ‘β] : {b : π} β b β b β‘ β
Lemma[bβbβ‘β] {β} = refl
Lemma[bβbβ‘β] {β} = refl

Lemma[bβ‘cβbβcβ‘β] : {b c : π} β b β‘ c β b β c β‘ β
Lemma[bβ‘cβbβcβ‘β] {b} {c} r = ap (Ξ» - β b β -) (r β»ΒΉ) β (Lemma[bβbβ‘β] {b})

Lemma[bβcβ‘ββbβ‘c] : {b c : π} β b β c β‘ β β b β‘ c
Lemma[bβcβ‘ββbβ‘c] {β} {β} r = refl
Lemma[bβcβ‘ββbβ‘c] {β} {β} ()
Lemma[bβcβ‘ββbβ‘c] {β} {β} ()
Lemma[bβcβ‘ββbβ‘c] {β} {β} r = refl

Lemma[bβ’cβbβcβ‘β] : {b c : π} β b β’ c β b β c β‘ β
Lemma[bβ’cβbβcβ‘β] = Lemma[bβ’ββbβ‘β] β (contrapositive Lemma[bβcβ‘ββbβ‘c])

Lemma[bβcβ‘ββbβ’c] : {b c : π} β b β c β‘ β β b β’ c
Lemma[bβcβ‘ββbβ’c] = (contrapositive Lemma[bβ‘cβbβcβ‘β]) β Lemma[bβ‘ββbβ’β]

\end{code}

Order and complements:

\begin{code}

complement-left : {b c : π} β complement b β€β c β complement c β€β b
complement-left {β} {β} f p = f p
complement-left {β} {β} f p = p
complement-left {β} {c} f p = refl

complement-right : {b c : π} β b β€β complement c β c β€β complement b
complement-right {β} {c} f p = refl
complement-right {β} {β} f p = p
complement-right {β} {β} f p = f p

complement-both-left : {b c : π} β complement b β€β complement c β c β€β b
complement-both-left {β} {β} f p = p
complement-both-left {β} {β} f p = f p
complement-both-left {β} {c} f p = refl

complement-both-right : {b c : π} β b β€β c β complement c β€β complement b
complement-both-right {β} {c} f p = refl
complement-both-right {β} {β} f p = f p
complement-both-right {β} {β} f p = p

\end{code}

The natural numbers:

\begin{code}

data β : Set where
zero : β
succ : β β β

{-# BUILTIN NATURAL β #-}

rec : β {U} {X : U Μ} β X β (X β X) β (β β X)
rec x f zero = x
rec x f (succ n) = f(rec x f n)

induction : β {U} {A : β β U Μ} β A 0 β ((k : β) β A k β A(succ k)) β (n : β) β A n
induction base step 0 = base
induction base step (succ n) = step n (induction base step n)

a-peano-axiom : {n : β} β succ n β’ 0
a-peano-axiom ()

pred : β β β
pred 0 = 0
pred (succ n) = n

succ-injective : {i j : β} β succ i β‘ succ j β i β‘ j
succ-injective = ap pred

\end{code}

Operator fixity and precedences.

\begin{code}

infixr 4 _,_
infixr 2 _Γ_
infixr 1 _+_
infixl 5 _β_
infix  50 Β¬_
infix  -1 _β_
infix  0 _β‘_
infix  0 _β’_
infix  3  _β»ΒΉ
infix  1 _β