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
open import Unit-Properties
π-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
π-excluded-third : (b : π) β b β’ β β b β’ β β π {π€β}
π-excluded-third β u v = u refl
π-excluded-third β u v = v refl
π-things-distinct-from-a-third-are-equal : (x y z : π) β x β’ z β y β’ z β x β‘ y
π-things-distinct-from-a-third-are-equal β β z u v = refl
π-things-distinct-from-a-third-are-equal β β z u v = π-elim (π-excluded-third z (β’-sym u) (β’-sym v))
π-things-distinct-from-a-third-are-equal β β z u v = π-elim (π-excluded-third z (β’-sym v) (β’-sym u))
π-things-distinct-from-a-third-are-equal β β z u v = refl
one-is-not-zero : β β’ β
one-is-not-zero p = π-is-not-π q
where
f : π β π€β Μ
f β = π
f β = π
q : π β‘ π
q = ap f p
zero-is-not-one : β β’ β
zero-is-not-one p = one-is-not-zero (p β»ΒΉ)
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 β p = π-elim (zero-is-not-one p)
complement-no-fp β p = π-elim (one-is-not-zero p)
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 {b} p = π-elim (zero-is-not-one p)
_β€β'_ : (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 : π} β (a β‘ β) + (b β‘ β) β minπ a b β‘ β
Lemma[minπabβ‘β] {β} {b} (inl p) = refl
Lemma[minπabβ‘β] {β} {β} (inr q) = refl
Lemma[minπabβ‘β] {β} {β} (inr q) = 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] {β} {β} r = r β»ΒΉ
Lemma[bβcβ‘ββbβ‘c] {β} {β} r = r
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}