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}