module Two where

open import Logic
open import Equality

-- Definition (The set ₂ of binary numbers).

data ₂ : Set where
 ₀ : ₂
 ₁ : ₂


two-equality-cases : {A : Ω} →
-------------------------------------------
 ∀{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≠₀] {₀} ()
Lemma[b≡₁→b≠₀] {₁} r = λ ()


Lemma[b≠₀→b≡₁] :
--------------------------
  ∀{b : ₂} → b ≠ ₀ → b ≡ ₁
--------------------------
Lemma[b≠₀→b≡₁] {₀} f = ⊥-elim(f refl)
Lemma[b≠₀→b≡₁] {₁} f = refl


Lemma[b≠₁→b≡₀] :
--------------------------
  ∀{b : ₂} → b ≠ ₁ → b ≡ ₀
--------------------------
Lemma[b≠₁→b≡₀] {₀} f = refl
Lemma[b≠₁→b≡₀] {₁} f = ⊥-elim(f refl)


Lemma[b≡₀→b≠₁] :
--------------------------
  ∀{b : ₂} → b ≡ ₀ → b ≠ ₁
--------------------------
Lemma[b≡₀→b≠₁] {₀} r = λ ()
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≠₁]


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≠₀]


-- Definition (Natural order of binary numbers)
_≤_ : (a b : ₂) → Ω
a ≤ b = a ≡ ₁ → b ≡ ₁

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


-- Definition (Minimum of binary numbers).
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