\begin{code}
{-# OPTIONS --without-K #-}
module Two where
open import SetsAndFunctions
open import CurryHoward
open import Equality
\end{code}
\begin{code}
data ₂ : Set where
₀ : ₂
₁ : ₂
\end{code}
\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}
\begin{code}
_≤_ : (a b : ₂) → Prp
a ≤ b = a ≡ ₁ → b ≡ ₁
_≥_ : (a b : ₂) → Prp
a ≥ b = b ≤ a
\end{code}
\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}