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 Μ‡}
    β†’ ((y : Y) β†’ Z y) β†’ (f : X β†’ Y) β†’ (x : X) β†’ Z (f x)
g ∘ f = Ξ» x β†’ g(f x)

\end{code}

xsEmpty 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β‚€}

is-empty : βˆ€ {U} β†’ U Μ‡ β†’ U Μ‡
is-empty = Β¬_

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

lhs : βˆ€ {U} {X : U Μ‡} {x y : X} β†’ x ≑ y β†’ X
lhs {U} {X} {x} {y} p = x

rhs : βˆ€ {U} {X : U Μ‡} {x y : X} β†’ x ≑ y β†’ X
rhs {U} {X} {x} {y} p = y

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 (lhs p)) q p

_⁻¹ : βˆ€ {U} {X : U Μ‡} β†’ {x y : X} β†’ x ≑ y β†’ y ≑ x
p ⁻¹ = transport (Ξ» - β†’ - ≑ lhs p) 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 (Ξ» - β†’ f (lhs p) ≑ f -) 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}

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

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

Cases-equality-l : βˆ€ {U V W} {X : U Μ‡} {Y : V Μ‡} {A : W Μ‡} (f : X β†’ A) (g : Y β†’ A)
                 β†’ (z : X + Y) (x : X) β†’ z ≑ inl x β†’ Cases z f g ≑ f x
Cases-equality-l f g .(inl x) x refl = refl

Cases-equality-r : βˆ€ {U V W} {X : U Μ‡} {Y : V Μ‡} {A : W Μ‡} (f : X β†’ A) (g : Y β†’ A)
                 β†’ (z : X + Y) (y : Y) β†’ z ≑ inr y β†’ Cases z f g ≑ g y
Cases-equality-r f g .(inr y) y refl = refl

\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'

Ξ£! : βˆ€ {U V} {X : U Μ‡} (A : X β†’ V Μ‡) β†’ U βŠ” V Μ‡
Ξ£! {U} {V} {X} A = (Ξ£ \(x : X) β†’ A x) Γ— ((x x' : X) β†’ A x β†’ A x' β†’ x ≑ x')

\end{code}

Note: Ξ£! is to be avoided, in favour of the contractibility of Ξ£, following univalent mathematics.

The following is properly proved using universes, but we don't bother
for 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

πŸ™-all-* : βˆ€ {U} (x : πŸ™) β†’ x ≑ *
πŸ™-all-* {U} * = refl {U}

\end{code}

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

\begin{code}

type-of : βˆ€ {U} {X : U Μ‡} β†’ X β†’ U Μ‡
type-of {U} {X} x = X

universe-of : βˆ€ {U} (X : U Μ‡) β†’ Universe
universe-of {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
 β‚€ : 𝟚
 ₁ : 𝟚

𝟚-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

\end{code}

Alternative coproduct:

\begin{code}

_+'_ : βˆ€ {U} β†’ U Μ‡ β†’ U Μ‡ β†’ U Μ‡
Xβ‚€ +' X₁ = Ξ£ \(i : 𝟚) β†’ 𝟚-cases Xβ‚€ X₁ i

\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)

_^_ : βˆ€ {U} {X : U Μ‡} β†’ (X β†’ X) β†’ β„• β†’ (X β†’ X)
(f ^ n) x = 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-lc : {i j : β„•} β†’ succ i ≑ succ j β†’ i ≑ j
succ-lc = ap pred

succ-no-fp : βˆ€ {U} (n : β„•) β†’ n ≑ succ n β†’ 𝟘 {U}
succ-no-fp zero ()
succ-no-fp (succ n) p = succ-no-fp n (succ-lc p)

\end{code}

We use the following to indicate the type of a subterm:

\begin{code}

-id : βˆ€ {U} (X : U Μ‡) β†’ X β†’ X
-id X x = x

syntax -id X x = x ∢ X

\end{code}

And the following to make explicit the type of hypotheses:

\begin{code}

have : βˆ€ {U V} {A : U Μ‡} {B : V Μ‡} β†’ A β†’ B β†’ B
have _ y = y

\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 _∎
infixr 0 _β‰‘βŸ¨_⟩_
infixl 2 _βˆ™_
infix  4  _∼_
infixl 0 -id

\end{code}