Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

module Two where

open import SetsAndFunctions
open import CurryHoward
open import Equality

\end{code}

Definition (The set ₂ of binary numbers):

\begin{code}

data ₂ : Set where
₀ : ₂
₁ : ₂

\end{code}

The set ₂ satisfies UIP without assuming UIP or extensionality (and so
do many other sets):

\begin{code}

zero-is-not-one : ₀ ≠ ₁
zero-is-not-one ()

two-induction : {A : ₂ → Prp} →

A ₀ → A ₁ → ∀(x : ₂) → A x

two-induction r s ₀ = r
two-induction r s ₁ = s

two-cases : {A : Set} →

A → A → ₂ → A

two-cases = two-induction

two-equality-cases : {A : Prp} →

∀{b : ₂} → (b ≡ ₀ → A) → (b ≡ ₁ → A) → A

two-equality-cases {A} {₀} f₀ f₁ = f₀ refl
two-equality-cases {A} {₁} f₀ f₁ = f₁ refl

Lemma[b≡₁→b≠₀] :
--------------------------
∀{b : ₂} → b ≡ ₁ → b ≠ ₀
--------------------------
Lemma[b≡₁→b≠₀] r s =
zero-is-not-one(Lemma[x≡y→y≡z→y≡z] s r)

Lemma[b≠₀→b≡₁] :

∀{b : ₂} → b ≠ ₀ → b ≡ ₁

Lemma[b≠₀→b≡₁] f = two-equality-cases (⊥-elim ∘ f) (λ r → r)

Lemma[b≠₁→b≡₀] :

∀{b : ₂} → b ≠ ₁ → b ≡ ₀

Lemma[b≠₁→b≡₀] f = two-equality-cases (λ r → r) (⊥-elim ∘ f)

Lemma[b≡₀→b≠₁] :

∀{b : ₂} → b ≡ ₀ → b ≠ ₁

Lemma[b≡₀→b≠₁] r s =
zero-is-not-one(Lemma[x≡y→y≡z→y≡z] r s)

Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] :

∀{a b : ₂} → (a ≡ ₁ → b ≡ ₁) → b ≡ ₀ → a ≡ ₀

Lemma[[a≡₁→b≡₁]→b≡₀→a≡₀] f =
Lemma[b≠₁→b≡₀] ∘ (contra-positive f) ∘ Lemma[b≡₀→b≠₁]

Lemma[[a≡₀→b≡₀]→b≡₁→a≡₁] :

∀{a b : ₂} → (a ≡ ₀ → b ≡ ₀) → b ≡ ₁ → a ≡ ₁

Lemma[[a≡₀→b≡₀]→b≡₁→a≡₁] f =
Lemma[b≠₀→b≡₁] ∘ (contra-positive f) ∘ Lemma[b≡₁→b≠₀]

\end{code}

Definition (Natural order of binary numbers):

\begin{code}

_≤_ : (a b : ₂) → Prp
a ≤ b = a ≡ ₁ → b ≡ ₁

_≥_ : (a b : ₂) → Prp
a ≥ b = b ≤ a

\end{code}

Definition (Minimum of binary numbers):

\begin{code}

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

\end{code}