Martin Escardo

The two-point type is defined, together with its induction principle,
in the module SpartanMLTT. Here we develop some general machinery.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module Two-Properties where

open import SpartanMLTT


𝟚-Cases : {A : 𝓀 Μ‡ } β†’ 𝟚 β†’ A β†’ A β†’ A
𝟚-Cases a b c = 𝟚-cases b c a

𝟚-equality-cases : {A : 𝓀 Μ‡ } {b : 𝟚} β†’ (b ≑ β‚€ β†’ A) β†’ (b ≑ ₁ β†’ A) β†’ A
𝟚-equality-cases {𝓀} {A} {β‚€} fβ‚€ f₁ = fβ‚€ refl
𝟚-equality-cases {𝓀} {A} {₁} fβ‚€ f₁ = f₁ refl

𝟚-equality-casesβ‚€ : {A : 𝓀 Μ‡ } {b : 𝟚} {fβ‚€ : b ≑ β‚€ β†’ A} {f₁ : b ≑ ₁ β†’ A}
                 β†’ (p : b ≑ β‚€) β†’ 𝟚-equality-cases {𝓀} {A} {b} fβ‚€ f₁ ≑ fβ‚€ p
𝟚-equality-casesβ‚€ {𝓀} {A} {.β‚€} refl = refl

𝟚-equality-cases₁ : {A : 𝓀 Μ‡ } {b : 𝟚} {fβ‚€ : b ≑ β‚€ β†’ A} {f₁ : b ≑ ₁ β†’ A}
                 β†’ (p : b ≑ ₁) β†’ 𝟚-equality-cases {𝓀} {A} {b} fβ‚€ f₁ ≑ f₁ p
𝟚-equality-cases₁ {𝓀} {A} {.₁} refl = refl

𝟚-equality-cases' : {Aβ‚€ A₁ : 𝓀 Μ‡ } {b : 𝟚} β†’ (b ≑ β‚€ β†’ Aβ‚€) β†’ (b ≑ ₁ β†’ A₁) β†’ Aβ‚€ + A₁
𝟚-equality-cases' {𝓀} {Aβ‚€} {A₁} {β‚€} fβ‚€ f₁ = inl(fβ‚€ refl)
𝟚-equality-cases' {𝓀} {Aβ‚€} {A₁} {₁} fβ‚€ f₁ = inr(f₁ refl)

𝟚-possibilities : (b : 𝟚) β†’ (b ≑ β‚€) + (b ≑ ₁)
𝟚-possibilities β‚€ = inl refl
𝟚-possibilities ₁ = inr refl

zero-is-not-one : β‚€ β‰’ ₁
zero-is-not-one ()

equal-₁-different-from-β‚€ : {b : 𝟚} β†’ b ≑ ₁ β†’ b β‰’ β‚€
equal-₁-different-from-β‚€ r s = zero-is-not-one (s ⁻¹ βˆ™ r)

different-from-β‚€-equal-₁ : {b : 𝟚} β†’ b β‰’ β‚€ β†’ b ≑ ₁
different-from-β‚€-equal-₁ f = 𝟚-equality-cases (𝟘-elim ∘ f) (Ξ» r β†’ r)

different-from-₁-equal-β‚€ : {b : 𝟚} β†’ b β‰’ ₁ β†’ b ≑ β‚€
different-from-₁-equal-β‚€ f = 𝟚-equality-cases (Ξ» r β†’ r) (𝟘-elim ∘ f)

equal-β‚€-different-from-₁ : {b : 𝟚} β†’ b ≑ β‚€ β†’ b β‰’ ₁
equal-β‚€-different-from-₁ r s = zero-is-not-one (r ⁻¹ βˆ™ s)

[a≑₁→b≑₁]-gives-[b≑₀→a≑₀] : {a b : 𝟚} β†’ (a ≑ ₁ β†’ b ≑ ₁) β†’ b ≑ β‚€ β†’ a ≑ β‚€
[a≑₁→b≑₁]-gives-[b≑₀→a≑₀] f = different-from-₁-equal-β‚€ ∘ (contrapositive f) ∘ equal-β‚€-different-from-₁

[a≑₀→b≑₀]-gives-[b≑₁→a≑₁] : {a b : 𝟚} β†’ (a ≑ β‚€ β†’ b ≑ β‚€) β†’ b ≑ ₁ β†’ a ≑ ₁
[a≑₀→b≑₀]-gives-[b≑₁→a≑₁] f = different-from-β‚€-equal-₁ ∘ (contrapositive f) ∘ equal-₁-different-from-β‚€

\end{code}

𝟚-Characteristic function of equality on 𝟚:

\begin{code}

complement : 𝟚 β†’ 𝟚
complement β‚€ = ₁
complement ₁ = β‚€

complement-no-fp : (n : 𝟚) β†’ n ≑ complement n β†’ 𝟘 {𝓀}
complement-no-fp β‚€ ()
complement-no-fp ₁ ()

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}

Natural order of binary numbers:

\begin{code}

_<β‚‚_ : (a b : 𝟚) β†’ 𝓀₀ Μ‡
a <β‚‚ b = (a ≑ β‚€) Γ— (b ≑ ₁)

_≀₂_ : (a b : 𝟚) β†’ 𝓀₀ Μ‡
a ≀₂ b = a ≑ ₁ β†’ b ≑ ₁

<β‚‚-gives-≀₂ : {a b : 𝟚} β†’ a <β‚‚ b β†’ a ≀₂ b
<β‚‚-gives-≀₂ (refl , refl) _ = refl

₁-top : {b : 𝟚} β†’ b ≀₂ ₁
₁-top r = refl

β‚€-bottom : {b : 𝟚} β†’ β‚€ ≀₂ b
β‚€-bottom ()

_≀₂'_ : (a b : 𝟚) β†’ 𝓀₀ Μ‡
a ≀₂' b = b ≑ β‚€ β†’ a ≑ β‚€

≀₂-gives-≀₂' : {a b : 𝟚} β†’ a ≀₂ b β†’ a ≀₂' b
≀₂-gives-≀₂' {β‚€} {b} f p = refl
≀₂-gives-≀₂' {₁} {β‚€} f p = (f refl)⁻¹
≀₂-gives-≀₂' {₁} {₁} f p = p

≀₂'-gives-≀₂ : {a b : 𝟚} β†’ a ≀₂' b β†’ a ≀₂ b
≀₂'-gives-≀₂ {β‚€} {β‚€} f p = p
≀₂'-gives-≀₂ {β‚€} {₁} f p = refl
≀₂'-gives-≀₂ {₁} {β‚€} f p = (f refl)⁻¹
≀₂'-gives-≀₂ {₁} {₁} f p = p

≀₂-anti : {a b : 𝟚} β†’ a ≀₂ b β†’ b ≀₂ a β†’ a ≑ b
≀₂-anti {β‚€} {β‚€} f g = refl
≀₂-anti {β‚€} {₁} f g = g refl
≀₂-anti {₁} {β‚€} f g = ≀₂-gives-≀₂' f refl
≀₂-anti {₁} {₁} f g = refl

₁-maximal : {b : 𝟚} β†’ ₁ ≀₂ b β†’ b ≑ ₁
₁-maximal = ≀₂-anti ₁-top

_β‰₯β‚‚_ : (a b : 𝟚) β†’ 𝓀₀ Μ‡
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(equal-₁-different-from-β‚€ r refl)
Lemma[minab≀₂a] {₁} {b} r = refl

Lemma[minab≀₂b] : {a b : 𝟚} β†’ min𝟚 a b ≀₂ b
Lemma[minab≀₂b] {β‚€} {b} r = 𝟘-elim(equal-₁-different-from-β‚€ 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≑₁] = different-from-β‚€-equal-₁ ∘ (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≑₀]) ∘ equal-₁-different-from-β‚€

\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}

Fixities and precedences:

\begin{code}

infixr 31 _βŠ•_

\end{code}