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}

Ξ  : {X : 𝓀 Μ‡} (Y : X β†’ π“₯ Μ‡) β†’ 𝓀 βŠ” π“₯ Μ‡
Ξ  Y = (x : _) β†’ Y x

syntax Ξ  {A} (Ξ» x β†’ B) = Π( x ∢ A οΌ‰ B

\end{code}

Identity and dependent function composition:

\begin{code}

id : {X : 𝓀 Μ‡} β†’ X β†’ X
id x = x

_∘_ : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {Z : Y β†’ 𝓦 Μ‡}
    β†’ ((y : Y) β†’ Z y)
    β†’ (f : X β†’ Y) (x : X) β†’ Z (f x)
g ∘ f = Ξ» x β†’ g(f x)

\end{code}

Empty type.

\begin{code}

data 𝟘 {𝓀} : 𝓀 Μ‡ where

unique-from-𝟘 : {A : 𝓀 Μ‡} β†’ 𝟘 {π“₯} β†’ A
unique-from-𝟘 = λ ()

𝟘-elim = unique-from-𝟘

\end{code}

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

\begin{code}

data πŸ™ {𝓀} : 𝓀 Μ‡ where
 * : πŸ™

unique-to-πŸ™ : {A : 𝓀 Μ‡} β†’ A β†’ πŸ™ {π“₯}
unique-to-πŸ™ {𝓀} {π“₯} a = * {π“₯}

open import Sigma public

\end{code}

Binary sums

\begin{code}

data _+_ {𝓀 π“₯} (X : 𝓀 Μ‡) (Y : π“₯ Μ‡) : 𝓀 βŠ” π“₯ Μ‡ where
  inl : X β†’ X + Y
  inr : Y β†’ X + Y

dep-cases : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {A : X + Y β†’ 𝓦 Μ‡}
          β†’ ((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 : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {A : 𝓦 Μ‡} β†’ (X β†’ A) β†’ (Y β†’ A) β†’ X + Y β†’ A
cases = dep-cases

Cases : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {A : 𝓦 Μ‡} β†’ X + Y β†’ (X β†’ A) β†’ (Y β†’ A) β†’ A
Cases z f g = cases f g z

+-commutative : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} β†’ A + B β†’ B + A
+-commutative = cases inr inl

\end{code}

Some basic Curry--Howard logic.

\begin{code}

Β¬_ : 𝓀 Μ‡ β†’ 𝓀 Μ‡
Β¬ A = A β†’ 𝟘 {𝓀₀}

is-empty : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-empty = Β¬_

decidable : 𝓀 Μ‡ β†’ 𝓀 Μ‡
decidable A = A + Β¬ A

_⇔_ : 𝓀 Μ‡ β†’ π“₯ Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
A ⇔ B = (A β†’ B) Γ— (B β†’ A)

dual : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} (R : 𝓦 Μ‡) β†’ (X β†’ Y) β†’ (Y β†’ R) β†’ (X β†’ R)
dual R f p = p ∘ f

contrapositive : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} β†’ (A β†’ B) β†’ Β¬ B β†’ Β¬ A
contrapositive = dual _

¬¬ : 𝓀 Μ‡ β†’ 𝓀 Μ‡
¬¬ A = ¬(¬ A)

¬¬-functor : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} β†’ (A β†’ B) β†’ ¬¬ A β†’ ¬¬ B
¬¬-functor = contrapositive ∘ contrapositive

double-negation-intro : {A : 𝓀 Μ‡} β†’ A β†’ ¬¬ A
double-negation-intro x u = u x

three-negations-imply-one : {A : 𝓀 Μ‡} β†’ Β¬(¬¬ A) β†’ Β¬ A
three-negations-imply-one = contrapositive double-negation-intro

double-negation-unshift : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡} β†’ ¬¬((x : X) β†’ A x) β†’ (x : X) β†’ ¬¬(A x)
double-negation-unshift f x g = f (Ξ» h β†’ g (h x))

dnu : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} β†’ ¬¬(A Γ— B) β†’ ¬¬ A Γ— ¬¬ B
dnu Ο† = (¬¬-functor pr₁ Ο†) , (¬¬-functor prβ‚‚ Ο†)

und : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} β†’ ¬¬ A Γ— ¬¬ B β†’ ¬¬(A Γ— B)
und (Ο† , Ξ³) w = Ξ³ (Ξ» y β†’ Ο† (Ξ» x β†’ w (x , y)))

not-Ξ£-implies-Ξ -not : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡}
                    β†’ Β¬(Ξ£ \(x : X) β†’ A x) β†’ (x : X) β†’ Β¬(A x)
not-Ξ£-implies-Ξ -not = curry

Ξ -not-implies-not-Ξ£ : {X : 𝓀 Μ‡} {A : X β†’ 𝓀 Μ‡}
                    β†’ ((x : X) β†’ Β¬(A x)) β†’ Β¬(Ξ£ \(x : X) β†’ A x)
Ξ -not-implies-not-Ξ£ = uncurry

Left-fails-then-right-holds : {P : 𝓀 Μ‡} {Q : π“₯ Μ‡} β†’ 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 : {P : 𝓀 Μ‡} {Q : π“₯ Μ‡} β†’ 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 _≑_ {𝓀} {X : 𝓀 Μ‡} : X β†’ X β†’ 𝓀 Μ‡ where
  refl : {x : X} β†’ x ≑ x

lhs : {X : 𝓀 Μ‡} {x y : X} β†’ x ≑ y β†’ X
lhs {𝓀} {X} {x} {y} p = x

rhs : {X : 𝓀 Μ‡} {x y : X} β†’ x ≑ y β†’ X
rhs {𝓀} {X} {x} {y} p = y

Id : {X : 𝓀 Μ‡} β†’ X β†’ X β†’ 𝓀 Μ‡
Id = _≑_

_β‰’_ : {X : 𝓀 Μ‡} β†’ (x y : X) β†’ 𝓀 Μ‡
x β‰’ y = Β¬(x ≑ y)

Jbased : {X : 𝓀 Μ‡} (x : X) (A : (y : X) β†’ x ≑ y β†’ π“₯ Μ‡)
       β†’ A x refl β†’ (y : X) (r : x ≑ y) β†’ A y r
Jbased x A b .x refl = b

J : {X : 𝓀 Μ‡} (A : (x y : X) β†’ x ≑ y β†’ π“₯ Μ‡)
  β†’ ((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' : {X : 𝓀 Μ‡} (A : X β†’ π“₯ Μ‡) {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 : {X : 𝓀 Μ‡} (A : X β†’ π“₯ Μ‡) {x y : X}
          β†’ x ≑ y β†’ A x β†’ A y
transport A refl = id

_βˆ™_ : {X : 𝓀 Μ‡} {x y z : X} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z
p βˆ™ q = transport (Id (lhs p)) q p

_⁻¹ : {X : 𝓀 Μ‡} β†’ {x y : X} β†’ x ≑ y β†’ y ≑ x
p ⁻¹ = transport (Ξ» - β†’ - ≑ lhs p) p refl

ap : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} (f : X β†’ Y) {x x' : X} β†’ x ≑ x' β†’ f x ≑ f x'
ap f p = transport (Ξ» - β†’ f (lhs p) ≑ f -) p refl

back-transport : {X : 𝓀 Μ‡} (A : X β†’ π“₯ Μ‡) {x y : X} β†’ x ≑ y β†’ A y β†’ A x
back-transport B p = transport B (p ⁻¹)

β‰’-sym : {X : 𝓀 Μ‡} β†’ {x y : X} β†’ x β‰’ y β†’ y β‰’ x
β‰’-sym u r = u(r ⁻¹)

\end{code}

Standard syntax for equality chain reasoning:

\begin{code}

_β‰‘βŸ¨_⟩_ : {X : 𝓀 Μ‡} (x : X) {y z : X} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z
_ β‰‘βŸ¨ p ⟩ q = p βˆ™ q

_∎ : {X : 𝓀 Μ‡} (x : X) β†’ x ≑ x
_∎ _ = refl

equality-cases : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {A : 𝓦 Μ‡} (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 : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {A : 𝓦 Μ‡} (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 : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {A : 𝓦 Μ‡} (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 : {X : 𝓀 Μ‡} β†’ (X β†’ π“₯ Μ‡) β†’ (X β†’ 𝓦 Μ‡) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
Nat A B = Ξ  \x β†’ A x β†’ B x

_∼_ : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡} β†’ Ξ  A β†’ Ξ  A β†’ 𝓀 βŠ” π“₯ Μ‡
f ∼ g = βˆ€ x β†’ f x ≑ g x

_β‰ˆ_ : {X : 𝓀 Μ‡} {x : X} {A : X β†’ π“₯ Μ‡} β†’ Nat (Id x) A β†’ Nat (Id x) A β†’ 𝓀 βŠ” π“₯ Μ‡
Ξ· β‰ˆ ΞΈ = βˆ€ y β†’ Ξ· y ∼ ΞΈ y

NatΞ£ : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡} {B : X β†’ 𝓦 Μ‡} β†’ Nat A B β†’ Ξ£ A β†’ Ξ£ B
NatΞ£ ΞΆ (x , a) = (x , ΞΆ x a)

NatΞ  : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡} {B : X β†’ 𝓦 Μ‡} β†’ Nat A B β†’ Ξ  A β†’ Ξ  B
NatΞ  f g x = f x (g x) -- (S combinator from combinatory logic!)

Ξ Ξ£-distr : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡} {P : (x : X) β†’ A x β†’ 𝓦 Μ‡}
         β†’ (Ξ  \(x : X) β†’ Ξ£ \(a : A x) β†’ P x a) β†’ Ξ£ \(f : Ξ  A) β†’ Ξ  \(x : X) β†’ P x (f x)
Ξ Ξ£-distr Ο† = (Ξ» x β†’ pr₁ (Ο† x)) , Ξ» x β†’ prβ‚‚ (Ο† x)

Ξ Ξ£-distr-back : {X : 𝓀 Μ‡} {A : X β†’ π“₯ Μ‡} {P : (x : X) β†’ A x β†’ 𝓦 Μ‡}
              β†’ (Ξ£ \(f : Ξ  A) β†’ Ξ  \(x : X) β†’ P x (f x)) β†’ Ξ  \(x : X) β†’ Ξ£ \(a : A x) β†’ P x a
Ξ Ξ£-distr-back (f , Ο†) x = f x , Ο† x

left-cancellable : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
left-cancellable f = βˆ€ {x x'} β†’ f x ≑ f x' β†’ x ≑ x'

left-cancellable' : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
left-cancellable' f = βˆ€ x x' β†’ f x ≑ f x' β†’ x ≑ x'

Ξ£! : {X : 𝓀 Μ‡} (A : X β†’ π“₯ Μ‡) β†’ 𝓀 βŠ” π“₯ Μ‡
Ξ£! {𝓀} {π“₯} {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 : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {x : X} {y : Y} β†’ Β¬(inl x ≑ inr y)
+disjoint ()

+disjoint' : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {x : X} {y : Y} β†’ Β¬(inr y ≑ inl x)
+disjoint' ()

inl-lc : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {x x' : X} β†’ inl {𝓀} {π“₯} {X} {Y} x ≑ inl x' β†’ x ≑ x'
inl-lc refl = refl

inr-lc : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} {y y' : Y} β†’ inr {𝓀} {π“₯} {X} {Y} y ≑ inr y' β†’ y ≑ y'
inr-lc refl = refl

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

\end{code}

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

\begin{code}

type-of : {X : 𝓀 Μ‡} β†’ X β†’ 𝓀 Μ‡
type-of {𝓀} {X} x = X

universe-of : (X : 𝓀 Μ‡) β†’ Universe
universe-of {𝓀} X = 𝓀

domain dom : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} β†’ (X β†’ Y) β†’ 𝓀 Μ‡
domain {𝓀} {π“₯} {X} {Y} f = X
dom = domain

codomain cod : {X : 𝓀 Μ‡} {Y : π“₯ Μ‡} β†’ (X β†’ Y) β†’ π“₯ Μ‡
codomain {𝓀} {π“₯} {X} {Y} f = Y
cod = codomain

\end{code}

The two-point type (or booleans)

\begin{code}

data 𝟚 : 𝓀₀ Μ‡ where
 β‚€ : 𝟚
 ₁ : 𝟚

𝟚-induction : {A : 𝟚 β†’ 𝓀 Μ‡} β†’ A β‚€ β†’ A ₁ β†’ (x : 𝟚) β†’ A x
𝟚-induction r s β‚€ = r
𝟚-induction r s ₁ = s

𝟚-cases : {A : 𝓀 Μ‡} β†’ A β†’ A β†’ 𝟚 β†’ A
𝟚-cases = 𝟚-induction

\end{code}

Alternative coproduct:

\begin{code}

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

\end{code}

The natural numbers:

\begin{code}

data β„• : Set where
  zero : β„•
  succ : β„• β†’ β„•

{-# BUILTIN NATURAL β„• #-}

rec : {X : 𝓀 Μ‡} β†’ X β†’ (X β†’ X) β†’ (β„• β†’ X)
rec x f zero = x
rec x f (succ n) = f(rec x f n)

_^_ : {X : 𝓀 Μ‡} β†’ (X β†’ X) β†’ β„• β†’ (X β†’ X)
(f ^ n) x = rec x f n

induction : {A : β„• β†’ 𝓀 Μ‡} β†’ 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 : (n : β„•) β†’ n ≑ succ n β†’ 𝟘 {𝓀}
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 : (X : 𝓀 Μ‡) β†’ 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 : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} β†’ A β†’ B β†’ B
have _ y = y

\end{code}

Operator fixity and precedences.

\begin{code}

infixr 1 _+_
infixl 5 _∘_
infix  50 Β¬_
infix  -1 _⇔_
infix  0 _≑_
infix  0 _β‰’_
infix  3  _⁻¹
infix  1 _∎
infixr 0 _β‰‘βŸ¨_⟩_
infixl 2 _βˆ™_
infix  4  _∼_
infix 0 -id

\end{code}