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}

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