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}

Addition modulo 2:

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

\end{code}