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 _+_, and
identity types _≑_.

\begin{code}

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

module SpartanMLTT where

open import Agda.Primitive using (_βŠ”_) renaming (lzero to Uβ‚€ ; lsuc to usuc ; Level to Universe) public

_Μ‡ : (U : Universe) β†’ _
U Μ‡ = Set U -- This should be the only use of the Agda keyword 'Set' in this development.

_β€² : Universe β†’ Universe
_β€² = usuc

U₁ = Uβ‚€ β€²

\end{code}

For example, we write the following instead of the usual

  unique-from-βˆ… : βˆ€ {β„“} {A : Set β„“} β†’ βˆ… β†’ A
  unique-from-βˆ… = Ξ» ()

\begin{code}

data 𝟘 : Uβ‚€ Μ‡ where

unique-from-𝟘 : βˆ€ {U} {A : U Μ‡} β†’ 𝟘 β†’ A
unique-from-𝟘 = λ ()

𝟘-elim = unique-from-𝟘


\end{code}

The one-element set is defined by induction with one case:
\begin{code}

data πŸ™ : Uβ‚€ Μ‡ where
 * : πŸ™ 

unique-to-πŸ™ : βˆ€ {U} {A : U Μ‡} β†’ A β†’ πŸ™
unique-to-πŸ™ a = *

\end{code}

Product types are built-in, but we may introduce the standard notation:

\begin{code}

Ξ  : βˆ€ {U V} {X : U Μ‡} β†’ (Y : X β†’ V Μ‡) β†’ U βŠ” V Μ‡
Ξ  Y = (x : _) β†’ Y x
 
\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 : Universe} {X : U Μ‡} (Y : X β†’ V Μ‡) : U βŠ” V Μ‡ where
  constructor _,_
  field
   pr₁ : X
   prβ‚‚ : Y pr₁

open Ξ£ public

Ξ£-elim : βˆ€ {U V} {X : U Μ‡} {Y : X β†’ V Μ‡} {A : (Ξ£ \(x : X) β†’ Y x) β†’ U βŠ” V Μ‡}
   β†’ ((x : X) (y : Y x) β†’ A(x , y)) β†’ (t : (Ξ£ \(x : X) β†’ Y x)) β†’ A t
Ξ£-elim f (x , y) = f x y


uncurry : βˆ€ {U V W} {X : U Μ‡} {Y : X β†’ V Μ‡} {Z : W Μ‡}
        β†’ ((x : X) β†’ Y x β†’ Z) β†’ (Ξ£ \(x : X) β†’ Y x) β†’ Z
uncurry f (x , y) = f x y


curry :  βˆ€ {U V W} {X : U Μ‡} {Y : X β†’ V Μ‡} {Z : W Μ‡}
      β†’ ((Ξ£ \(x : X) β†’ Y x) β†’ 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}

This can also be considered as a special case, but I won't
bother:

\begin{code}

data _+_ {U V : Universe} (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

+-commutative : βˆ€ {U V} {A : U Μ‡} {B : V Μ‡} β†’ A + B β†’ B + A
+-commutative = cases inr inl

\end{code}

General constructions on functions:

\begin{code}

_∘_ : βˆ€ {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)

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

\end{code}

I use JJ and KK to avoid confusion with J and K for
equality.

\begin{code}

KK : βˆ€ {U V} β†’ U Μ‡ β†’ V Μ‡ β†’ U βŠ” V Μ‡
KK R X = (X β†’ R) β†’ R

contravariant : βˆ€ {U V W} {X : U Μ‡} {Y : V Μ‡} {R : W Μ‡} β†’ (X β†’ Y) β†’ (Y β†’ R) β†’ (X β†’ R)
contravariant f p = p ∘ f 
K-functor : βˆ€ {U V W} {R : U Μ‡} {X : V Μ‡} {Y : W Μ‡} β†’ (X β†’ Y) β†’ KK R X β†’ KK R Y
K-functor = contravariant ∘ contravariant

Ξ·K : βˆ€ {U V} {R : U Μ‡} {X : V Μ‡} β†’ X β†’ KK R X
Ξ·K x p = p x

\end{code}

K-unshift:

\begin{code}

KU : βˆ€ {U V W} {R : U Μ‡} {X : V Μ‡} {Y : X β†’ W Μ‡}
   β†’ KK R ((x : X) β†’ Y x) β†’ (x : X) β†’ KK R (Y x)
KU = Ξ» f x g β†’ f(Ξ» h β†’ g(h x))

\end{code}

Special case, if you like:

\begin{code}

ku : βˆ€ {U V W} {R : U Μ‡} {X : V Μ‡} {Y : W Μ‡} β†’ KK R (X Γ— Y) β†’ KK R X Γ— KK R Y
ku Ο† = (K-functor pr₁ Ο† , K-functor prβ‚‚ Ο†)

\end{code}

I am not sure were to put the following (product of quantifiers and
selection functions). At the moment it goes in this module. It is not
used, but it is included for the sake of comparison with similar
patterns.

\begin{code}

quant-prod : βˆ€ {U V} {X R : U Μ‡} {Y : X β†’ V Μ‡}
    β†’ KK R X β†’ ((x : X)  β†’ KK R (Y x)) β†’ KK R ((Ξ£ \(x : X)  β†’ Y x))
quant-prod Ο† Ξ³ p = Ο†(Ξ» x β†’ Ξ³ x (Ξ» y β†’ p(x , y)))

JJ : βˆ€ {U V} β†’ U Μ‡ β†’ V Μ‡ β†’ U βŠ” V Μ‡
JJ R X = (X β†’ R) β†’ X

sel-prod : βˆ€ {U V W} {R : U Μ‡} {X : V Μ‡} {Y : X β†’ W Μ‡}
         β†’ JJ R X β†’ ((x : X) β†’ JJ R (Y x)) β†’ JJ R (Ξ£ \(x : X) β†’ Y x)
sel-prod {U} {V} {W} {R} {X} {Y} Ξ΅ Ξ΄ p = (xβ‚€ , yβ‚€)
   where 
    next : (x : X) β†’ Y x
    next x = Ξ΄ x (Ξ» y β†’ p(x , y))
    xβ‚€ : X
    xβ‚€ = Ξ΅(Ξ» x β†’ p(x , next x))
    yβ‚€ : Y xβ‚€
    yβ‚€ = next xβ‚€ 

\end{code}

Alternative, equivalent, construction:

\begin{code}

overline : βˆ€ {U V} {R : U Μ‡} {X : V Μ‡} β†’ JJ R X β†’ KK R X
overline Ξ΅ p = p(Ξ΅ p)

sel-prod' : βˆ€ {U V W} {R : U Μ‡} {X : V Μ‡} {Y : X β†’ W Μ‡}
          β†’ JJ R X β†’ ((x : X) β†’ JJ R (Y x)) β†’ JJ R (Ξ£ \(x : X) β†’ Y x)
sel-prod' {U} {V} {W} {R} {X} {Y} Ξ΅ Ξ΄ p = (xβ‚€ , yβ‚€)
   where 
    xβ‚€ : X
    xβ‚€ = Ξ΅(Ξ» x β†’ overline(Ξ΄ x) (Ξ» y β†’ p(x , y)))
    yβ‚€ : Y xβ‚€
    yβ‚€ = Ξ΄ xβ‚€ (Ξ» y β†’ p(xβ‚€ , y))

\end{code}

Some basic Curry--Howard logic. 

\begin{code}

_⇔_ : βˆ€ {U V} β†’ U Μ‡ β†’ V Μ‡ β†’ U βŠ” V Μ‡
A ⇔ B = (A β†’ B) Γ— (B β†’ A)

Β¬_ : βˆ€ {U}β†’ U Μ‡ β†’ U Μ‡
Β¬ A = A β†’ 𝟘


contrapositive : βˆ€ {U V} {A : U Μ‡} {B : V Μ‡} β†’ (A β†’ B) β†’ Β¬ B β†’ Β¬ A
contrapositive = contravariant

\end{code}

Double-negation monad:

\begin{code}

¬¬ : βˆ€ {U} β†’ U Μ‡ β†’ U Μ‡
¬¬ A = ¬(¬ A)

¬¬-functor : βˆ€ {U V} {A : U Μ‡} {B : V Μ‡} β†’ (A β†’ B) β†’ ¬¬ A β†’ ¬¬ B
¬¬-functor = K-functor

double-negation-intro : βˆ€ {U} {A : U Μ‡} β†’ A β†’ ¬¬ A
double-negation-intro = Ξ·K

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

not-exists-implies-forall-not : βˆ€ {U V} {X : U Μ‡} {A : X β†’ V Μ‡}
    β†’ Β¬(Ξ£ \(x : X) β†’ A x) β†’ (x : X) β†’ Β¬(A x)
not-exists-implies-forall-not = curry

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

\end{code}

Double-negation unshift:

\begin{code}

DNU : βˆ€ {U V} {X : U Μ‡} {A : X β†’ V Μ‡} β†’ ¬¬((x : X) β†’ A x) β†’ (x : X) β†’ ¬¬(A x)
DNU = KU

\end{code}

Special case, if you like:

\begin{code}

dnu : βˆ€ {U} {V} {A : U Μ‡} {B : V Μ‡} β†’ ¬¬(A Γ— B) β†’ ¬¬ A Γ— ¬¬ B
dnu = ku
 
\end{code}

Binary relations:

\begin{code}

bin-rel : βˆ€ {U} β†’ U Μ‡ β†’ U β€² Μ‡
bin-rel {U} X = X β†’ X β†’ U Μ‡

\end{code}

Equality (should be moved to UF.lagda).

\begin{code}

data _≑_ {U : Universe} {X : U Μ‡} : X β†’ X β†’ U Μ‡ where
  refl : {x : X} β†’ x ≑ x

idp : βˆ€ {U} {X : U Μ‡} (x : X) β†’ x ≑ x
idp _ = refl

_β‰’_ : βˆ€ {U} {X : U Μ‡} β†’ (x y : X) β†’ U Μ‡
x β‰’ y = x ≑ y β†’ 𝟘

Id : βˆ€ {U} {X : U Μ‡} β†’ X β†’ X β†’ U Μ‡
Id = _≑_

sum-disjoint : βˆ€ {U V} {X : U Μ‡} {Y : V Μ‡} {x : X} {y : Y} β†’ inl x ≑ inr y β†’ 𝟘
sum-disjoint ()

\end{code}

Induction on ≑:

\begin{code}

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

\end{code}

We will often use pattern matching rather than J, but we'll make sure
we don't use the K rule (UIP) inadvertently. But not in the following
definition:

\begin{code}

pseudo-uip : βˆ€ {U} {X : U Μ‡} {x x' : X} (r : x ≑ x') β†’ (x , refl) ≑ (x' , r)
pseudo-uip {U} {X} = J {U} {U} {X} A (Ξ» x β†’ refl)
 where
   A : (x x' : X) β†’ x ≑ x' β†’ U Μ‡
   A x x' r = _≑_ {_} {Ξ£ \(x' : X) β†’ x ≑ x'} (x , refl) (x' , r)

\end{code}

The parameter Y is not used explicitly in the definition of transport,
but hardly ever can be inferred by Agda, and hence we make it
explicit:

\begin{code}

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

_βˆ™_ : βˆ€ {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

β‰’-sym : βˆ€ {U} {X : U Μ‡} β†’ {x y : X} β†’ x β‰’ y β†’ y β‰’ x
β‰’-sym f r = f(r ⁻¹)

trans-sym : βˆ€ {U} {X : U Μ‡} {x y : X} (r : x ≑ y) β†’ r ⁻¹ βˆ™ r ≑ refl
trans-sym refl = refl

trans-sym' : βˆ€ {U} {X : U Μ‡} {x y : X} (r : x ≑ y) β†’ r βˆ™ r ⁻¹ ≑ refl
trans-sym' refl = refl

ap : βˆ€ {U V} {X : U Μ‡} {Y : V Μ‡} (f : X β†’ Y) {xβ‚€ x₁ : X} β†’ xβ‚€ ≑ x₁ β†’ f xβ‚€ ≑ f x₁
ap f p = transport (Ξ» y β†’ f _ ≑ f y) p refl

Lemma-ap-ap : βˆ€ {U V W} {X : U Μ‡} {Y : V Μ‡} {Z : W Μ‡} (f : X β†’ Y) (g : Y β†’ Z) {x x' : X}
              (r : x ≑ x')
           β†’ ap g (ap f r) ≑ ap (g ∘ f) r
Lemma-ap-ap {U} {V} {W} {X} {Y} {Z} f g = J A (Ξ» x β†’ refl)
 where
  A : (x x' : X) β†’ x ≑ x' β†’ W Μ‡
  A x x' r = ap g (ap f r) ≑ ap (g ∘ f) r

apβ‚‚ : βˆ€ {U V W} {X : U Μ‡} {Y : V Μ‡} {Z : W Μ‡} (f : X β†’ Y β†’ Z) {xβ‚€ x₁ : X} {yβ‚€ y₁ : Y}
   β†’ xβ‚€ ≑ x₁ β†’ yβ‚€ ≑ y₁ β†’ f xβ‚€ yβ‚€ ≑ f x₁ y₁
apβ‚‚ f refl refl = refl

_∼_ : βˆ€ {U V} {X : U Μ‡} {A : X β†’ V Μ‡} β†’ Ξ  A β†’ Ξ  A β†’ U βŠ” V Μ‡
f ∼ g = βˆ€ x β†’ f x ≑ g x

happly : βˆ€ {U V} {X : U Μ‡} {A : X β†’ V Μ‡} (f g : Ξ  A) β†’ f ≑ g β†’ f ∼ g
happly f g p x = ap (Ξ» h β†’ h x) p

ap-eval : βˆ€ {U V} {X : U Μ‡} {A : X β†’ V Μ‡} {f g : Ξ  A} β†’ f ≑ g β†’ f ∼ g
ap-eval = happly _ _

sym-is-inverse : βˆ€ {U} {X : U Μ‡} {x y : X} (p : x ≑ y)
               β†’ refl ≑ p ⁻¹ βˆ™ p
sym-is-inverse {X} = J (Ξ» x y p β†’ refl ≑ p ⁻¹ βˆ™ p) (Ξ» x β†’ refl)

Lemma[x≑yβ†’y≑zβ†’y≑z] : βˆ€ {U} {X : U Μ‡} {x y z : X} β†’ x ≑ y β†’ x ≑ z β†’ y ≑ z
Lemma[x≑yβ†’y≑zβ†’y≑z] refl p = p

Lemma[x≑yβ†’x≑zβ†’z≑y] : βˆ€ {U} {X : U Μ‡} {x y z : X} β†’ x ≑ y β†’ x ≑ z β†’ z ≑ y
Lemma[x≑yβ†’x≑zβ†’z≑y] p refl = p

Lemma[x≑yβ†’x≑zβ†’y≑z] : βˆ€ {U} {X : U Μ‡} {x y z : X} β†’ x ≑ y β†’ x ≑ z β†’ y ≑ z
Lemma[x≑yβ†’x≑zβ†’y≑z] refl p = p

Lemma[x≑zβ†’y≑zβ†’x≑y] : βˆ€ {U} {X : U Μ‡} {x y z : X} β†’ x ≑ z β†’ y ≑ z β†’ x ≑ y
Lemma[x≑zβ†’y≑zβ†’x≑y] p refl = p

Lemma[fx≑yβ†’x≑x'β†’fx'≑y] : βˆ€ {U V} {X : U Μ‡} {Y : V Μ‡} (f : X β†’ Y) {x x' : X} {y : Y}
                         β†’ f x ≑ y β†’  x ≑ x' β†’ f x' ≑ y
Lemma[fx≑yβ†’x≑x'β†’fx'≑y] f {x} {x'} {y} r s =  Lemma[x≑yβ†’x≑zβ†’z≑y] r (ap f s)

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


Ξ£! : βˆ€ {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')

Ξ£-≑-lemma : βˆ€ {U V} {X : U Μ‡} {Y : X β†’ V Μ‡} (u v : Ξ£ Y) (r : u ≑ v)
          β†’ transport Y (ap pr₁ r) (prβ‚‚ u) ≑ (prβ‚‚ v)
Ξ£-≑-lemma {U} {V} {X} {Y} u v = J A (Ξ» u β†’ refl) {u} {v}
 where
  A : (u v : Ξ£ Y) β†’ u ≑ v β†’ V Μ‡
  A u v r = transport Y (ap pr₁ r) (prβ‚‚ u) ≑ (prβ‚‚ v)

Ξ£-≑-lemma' : βˆ€ {U V} {X : U Μ‡} {Y : X β†’ V Μ‡} (x : X) (y y' : Y x)
           β†’ (r : (x , y) ≑ (x , y')) β†’ transport Y (ap pr₁ r) y ≑ y'
Ξ£-≑-lemma' x y y' = Ξ£-≑-lemma (x , y) (x , y')

Ξ£-≑ : βˆ€ {U V} {X : U Μ‡} {Y : X β†’ V Μ‡} (x x' : X) (y : Y x) (y' : Y x')
     β†’ (p : x ≑ x') β†’ transport Y p y ≑ y' β†’ (x , y) ≑ (x' , y') 
Ξ£-≑ .x' x' .y y refl refl = refl

Ξ£-≑' : βˆ€ {U V} {X : U Μ‡} {Y : X β†’ V Μ‡} (x : X) (y y' : Y x) 
     β†’ y ≑ y' β†’ _≑_ {_} {Ξ£ Y} (x , y) (x , y') 
Ξ£-≑' x y y' r = ap (Ξ» y β†’ (x , y)) 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

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

\end{code}

\begin{code}

infix  0 _Μ‡
infix  99 _β€²
infix  4  _∼_
infixl 2 _βˆ™_
infix  1 _∎
infixr 0 _β‰‘βŸ¨_⟩_ 
infixr 4 _,_
infixr 2 _Γ—_
infixr 0 _+_
infixl 5 _∘_ 
infix  50 Β¬_
infix  1 _≑_
infix  1 _β‰’_
infix  3  _⁻¹
infix  0 _⇔_

\end{code}