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 (lzero ; lsuc ; _⊔_) renaming (Level to 𝕃) public

\end{code}

We want to work in univalent type theory, where a set is a special
kind of type, and hence the word Set to denote type universes is not
appropriate. This should be the only place in the whole development in
which we use Set (rather than U, U₀, U₁ or 𝕌):

\begin{code}

𝕌 : (i : 𝕃)  Set (lsuc i)
𝕌 i = Set i

U₀ = 𝕌 lzero
U = U₀
U₁ = 𝕌 (lsuc lzero)

\end{code}

Eventually everything here should be made universe polymorphic.

The empty set is defined by induction by an empty set of
clauses: 

\begin{code}

data  : U where

unique-from-∅ : {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-𝟙 : {A : U}  A  𝟙
unique-to-𝟙 a = *

\end{code}

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

\begin{code}

Π : {i j : 𝕃} {X : 𝕌 i}  (Y : X  𝕌 j)  𝕌(i  j)
Π 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}

infixr 3 _,_

record Σ {i j : 𝕃} {X : 𝕌 i} (Y : X  𝕌 j) : 𝕌(i  j) where
  constructor _,_
  field
   pr₁ : X
   pr₂ : Y pr₁

open Σ public

Σ-elim : {X : U} {Y : X  U} {A : (Σ \(x : X)  Y x)  U}
    ((x : X) (y : Y x)  A(x , y))  (t : (Σ \(x : X)  Y x))  A t
Σ-elim f (x , y) = f x y


uncurry : {X Z : U} {Y : X  U}
         ((x : X)  Y x  Z)  (Σ \(x : X)  Y x)  Z
uncurry f (x , y) = f x y


curry : {X Z : U} {Y : X  U}
       ((Σ \(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}

infixr 20 _×_

_×_ : U  U  U
X × Y = Σ \(x : X)  Y

\end{code}

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

\begin{code}

infixr 20 _+_

data _+_ (X₀ X₁ : U) : U where
  inl : X₀  X₀ + X₁
  inr : X₁  X₀ + X₁

dep-cases : {X₀ X₁ : U} {Y : X₀ + X₁  U}  ((x₀ : X₀)  Y(inl x₀))
           ((x₁ : X₁)  Y(inr x₁))  ((p : X₀ + X₁)  Y p)
dep-cases f₀ f₁ (inl x₀) = f₀ x₀
dep-cases f₀ f₁ (inr x₁) = f₁ x₁

cases : {X₀ X₁ Y : U}  (X₀  Y)  (X₁  Y)  X₀ + X₁  Y
cases = dep-cases

+-commutative : {A B : U}  A + B  B + A
+-commutative = cases inr inl


\end{code}

General constructions on functions:

\begin{code}

infixl 31 _∘_ 

_∘_ : {X Y : U} {Z : Y  U}
     ((y : Y)  Z y)  (f : X  Y)  (x : X)  Z(f x)
g  f = λ x  g(f x)

id : {i : 𝕃} {X : 𝕌 i}  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  U  U
KK R X = (X  R)  R

contra-variant : {R X Y : U}  (X  Y)  (Y  R)  (X  R)
contra-variant f p = p  f

K-functor : {R X Y : U}  (X  Y)  KK R X  KK R Y
K-functor = contra-variant  contra-variant

ηK : {R X : U}  X  KK R X
ηK x p = p x

\end{code}

K-unshift:

\begin{code}

KU : {R X : U} {Y : X  U}
    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 : {R X Y : U}  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 : {X R : U} {Y : X  U}
     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  U  U
JJ R X = (X  R)  X

sel-prod : {R : U} {X : U} {Y : X  U}
          JJ R X  ((x : X)  JJ R (Y x))  JJ R (Σ \(x : X)  Y x)
sel-prod {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 : {X R : U}  JJ R X  KK R X
overline ε p = p(ε p)

sel-prod' : {R : U} {X : U} {Y : X  U}
           JJ R X  ((x : X)  JJ R (Y x))  JJ R (Σ \(x : X)  Y x)
sel-prod' {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  U  U
A  B = (A  B) × (B  A)

infix  50 ¬_

¬_ : U  U
¬ A = A  


contra-positive : {A B : U}  (A  B)  ¬ B  ¬ A
contra-positive = contra-variant

\end{code}

Double-negation monad:

\begin{code}

¬¬ : U  U
¬¬ A = ¬(¬ A)

¬¬-functor : {A B : U}  (A  B)  ¬¬ A  ¬¬ B
¬¬-functor = K-functor

double-negation-intro : {A : U}  A  ¬¬ A
double-negation-intro = ηK


three-negations-imply-one : {A : U}  ¬(¬¬ A)  ¬ A
three-negations-imply-one = contra-positive double-negation-intro


not-exists-implies-forall-not : {X : U} {A : X  U}
     ¬(Σ \(x : X)  A x)  (x : X)  ¬(A x)
not-exists-implies-forall-not = curry


forall-not-implies-not-Σ : {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 : {X : U} {A : X  U}  ¬¬((x : X)  A x)  (x : X)  ¬¬(A x)
DNU = KU

\end{code}

Special case, if you like:

\begin{code}

dnu : {A B : U}  ¬¬(A × B)  ¬¬ A × ¬¬ B
dnu = ku
 
\end{code}

Binary relations:

\begin{code}

bin-rel : U  U₁
bin-rel X = X  X  U

\end{code}

Equality.

\begin{code}

infix  30 _≡_
infix  30 _≢_

data _≡_ {i : 𝕃} {X : 𝕌 i} : X  X  𝕌 i where
  refl : {x : X}  x  x

_≢_ : {X : U}  (x y : X)  U
x  y = x  y  

\end{code}

Induction on ≡:

\begin{code}

J : {X : U}
   (A : (x x' : X)  x  x'  U)
   ((x : X)  A x x refl)
    {x x' : X} (r : x  x')
   A x x' r
J A f {x} refl = f x

\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 : {X : U} {x x' : X} (r : x  x')  (x , refl)  (x' , r)
pseudo-uip {X} = J {X} A  x  refl)
 where
   A : (x x' : X)  x  x'  U
   A x x' r = _≡_ {_} {Σ \(x' : X)  x  x'} (x , refl) (x' , r)

-- 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:
transport : {i j : 𝕃} {X : 𝕌 i}(Y : X  𝕌 j){x x' : X}
           x  x'  Y x  Y x'
transport Y refl y = y 


trans : {i : 𝕃} {X : 𝕌 i}
      {x y z : X}   x  y    y  z    x  z
trans refl refl = refl

_∙_ = trans

infixl 32 _∙_

sym : {i : 𝕃} {X : 𝕌 i}  {x y : X}  x  y  y  x
sym refl = refl

_⁻¹ = sym

≢-sym : {X : U}  {x y : X}  x  y  y  x
≢-sym f r = f(sym r)

trans-sym : {X : U} {x y : X} (r : x  y)  trans (sym r) r  refl
trans-sym refl = refl

ap : {i j : 𝕃} {X : 𝕌 i} {Y : 𝕌 j} (f : X  Y) {x₀ x₁ : X}  x₀  x₁  f x₀  f x₁
ap f refl = refl

Lemma-ap-ap : {X Y Z : U} (f : X  Y) (g : Y  Z) {x x' : X}
              (r : x  x')
            ap g (ap f r)  ap (g  f) r
Lemma-ap-ap {X} {Y} {Z} f g = J A  x  refl)
 where
  A : (x x' : X)  x  x'  U
  A x x' r = ap g (ap f r)  ap (g  f) r

ap₂ : {X Y Z : U} (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

ap-eval : {X Y : U} {f g : X  Y}  f  g  (x : X)  f x  g x
ap-eval {X} {Y} {f} {g} r x = ap  h  h x) r

sym-is-inverse : {X : U} {x y : X} (p : x  y)
                refl  trans (sym p) p
sym-is-inverse {X} = J {X}  x y p  refl  trans (sym p) p)  x  refl)

Lemma[x≡y→y≡z→y≡z] : {X : U} {x y z : X}  x  y  x  z  y  z
Lemma[x≡y→y≡z→y≡z] refl refl = refl

Lemma[x≡y→x≡z→z≡y] : {X : U} {x y z : X}  x  y  x  z  z  y
Lemma[x≡y→x≡z→z≡y] refl refl = refl

Lemma[x≡y→x≡z→y≡z] : {X : U} {x y z : X}  x  y  x  z  y  z
Lemma[x≡y→x≡z→y≡z] refl refl = refl

Lemma[x≡z→y≡z→x≡y] : {X : U} {x y z : X}  x  z  y  z  x  y
Lemma[x≡z→y≡z→x≡y] refl refl = refl

Lemma[fx≡y→x≡x'→fx'≡y] : {X Y : U} (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 : {X Y : U} {A : U} (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


Σ! : {X : U} (A : X  U)  U 
Σ! {X} A = (Σ \(x : X)  A x) × ((x x' : X)  A x  A x'  x  x')

Σ-≡-lemma : {X : U} {Y : X  U} (u v : Σ Y) (r : u  v)
           transport Y (ap pr₁ r) (pr₂ u)  (pr₂ v)
Σ-≡-lemma {X} {Y} u v = J A  u  refl) {u} {v}
 where
  A : (u v : Σ Y)  u  v  U
  A u v r = transport Y (ap pr₁ r) (pr₂ u)  (pr₂ v)

Σ-≡-lemma' : {X : U} {Y : X  U} (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')

Σ-≡ : {i j : 𝕃} {X : 𝕌 i} {Y : X  𝕌 j} (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

Σ-≡' : {X : U} {Y : X  U} (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}

infix  2 _∎
infixr 2 _≡〈_〉_ 
 
_≡〈_〉_ : {X : U} (x : X) {y z : X}  x  y  y  z  x  z
_ ≡〈 r  s = trans r s


_∎ : {X : U}  (x : X)  x  x
_∎ _ = refl

𝟙-all-* : (x : 𝟙)  x  *
𝟙-all-* * = refl 

\end{code}