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 --safe --without-K #-}

module MLTT.Two-Properties where

open import MLTT.Spartan
open import MLTT.Unit-Properties
open import Naturals.Properties
open import Notation.Order
open import UF.FunExt
open import UF.Retracts
open import UF.Subsingletons

π-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 β»ΒΉ)

π-ext : {b c : π} β (b οΌ β β c οΌ β) β (c οΌ β β b οΌ β) β b οΌ c
π-ext {β} {β} f g = refl
π-ext {β} {β} f g = π-elim (zero-is-not-one (g refl))
π-ext {β} {β} f g = π-elim (zero-is-not-one (f refl))
π-ext {β} {β} f g = refl

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 : π) β π€β Μ
β <β β = π
β <β β = π
β <β b = π

_β€β_ : (a b : π) β π€β Μ
β β€β b = π
β β€β β = π
β β€β β = π

instance
strict-order-π-π : Strict-Order π π
_<_ {{strict-order-π-π}} = _<β_

order-π-π : Order π π
_β€_ {{order-π-π}} = _β€β_

<β-is-prop-valued : {b c : π} β is-prop (b < c)
<β-is-prop-valued {β} {β} = π-is-prop
<β-is-prop-valued {β} {β} = π-is-prop
<β-is-prop-valued {β} {c} = π-is-prop

β€β-is-prop-valued : {b c : π} β is-prop (b β€ c)
β€β-is-prop-valued {β} {c} = π-is-prop
β€β-is-prop-valued {β} {β} = π-is-prop
β€β-is-prop-valued {β} {β} = π-is-prop

<β-criterion : {a b : π} β (a οΌ β) β (b οΌ β) β a <β b
<β-criterion {β} {β} refl refl = β

<β-criterion-converse : {a b : π} β a <β b β (a οΌ β) Γ (b οΌ β)
<β-criterion-converse {β} {β} l = refl , refl

β€β-criterion : {a b : π} β (a οΌ β β b οΌ β) β a β€β b
β€β-criterion {β} {b} f = β
β€β-criterion {β} {β} f = π-elim (zero-is-not-one (f refl))
β€β-criterion {β} {β} f = β

β€β-criterion-converse : {a b : π} β a β€β b β a οΌ β β b οΌ β
β€β-criterion-converse {β} {β} l refl = refl

<β-gives-β€β : {a b : π} β a < b β a β€ b
<β-gives-β€β {β} {β} ()
<β-gives-β€β {β} {β} β = β
<β-gives-β€β {β} {c} ()

<β-trans : (a b c : π) β a < b β b < c β a < c
<β-trans β β c l m = m
<β-trans β β c l ()

Lemma[aοΌββb<cβa<c] : {a b c : π} β a οΌ β β b < c β a < c
Lemma[aοΌββb<cβa<c] {β} {β} {c} refl l = l

Lemma[a<bβcβ ββa<c] : {a b c : π} β a < b β c β  β β a < c
Lemma[a<bβcβ ββa<c] {β} {β} {β} l Ξ½ = Ξ½ refl
Lemma[a<bβcβ ββa<c] {β} {β} {β} l Ξ½ = β

β-top : {b : π} β b β€ β
β-top {β} = β
β-top {β} = β

β-bottom : {b : π} β β β€ b
β-bottom {β} = β
β-bottom {β} = β

β-maximal : {b : π} β β β€ b β b οΌ β
β-maximal {β} l = refl

β-maximal-converse : {b : π} β b οΌ β β β β€ b
β-maximal-converse {β} refl = β

β-minimal : {b : π} β b β€ β β b οΌ β
β-minimal {β} l = refl

β-minimal-converse : {b : π} β b οΌ β β b β€ β
β-minimal-converse {β} refl = β

_β€β'_ : (a b : π) β π€β Μ
a β€β' b = b οΌ β β a οΌ β

β€β-gives-β€β' : {a b : π} β a β€ b β a β€β' b
β€β-gives-β€β' {β} {b} _ p = refl
β€β-gives-β€β' {β} {β} () p
β€β-gives-β€β' {β} {β} _ p = p

β€β'-gives-β€β : {a b : π} β a β€β' b β a β€ b
β€β'-gives-β€β {β} {b} _ = β
β€β'-gives-β€β {β} {β} l = π-elim (one-is-not-zero (l refl))
β€β'-gives-β€β {β} {β} _ = β

β€β-refl : {b : π} β b β€ b
β€β-refl {β} = β
β€β-refl {β} = β

β€β-trans : (a b c : π) β a β€ b β b β€ c β a β€ c
β€β-trans β b c l m = β
β€β-trans β β β l m = β

β€β-anti : {a b : π} β a β€ b β b β€ a β a οΌ b
β€β-anti {β} {β} l m = refl
β€β-anti {β} {β} l ()
β€β-anti {β} {β} () m
β€β-anti {β} {β} l m = refl

minπ : π β π β π
minπ β b = β
minπ β b = b

minπ-comm : (b c : π) β minπ b c οΌ minπ c b
minπ-comm β β = refl
minπ-comm β β = refl
minπ-comm β β = refl
minπ-comm β β = refl

minπ-idemp : (b : π) β minπ b b οΌ b
minπ-idemp β = refl
minπ-idemp β = refl

minπ-propertyβ : (b : π) β minπ b β οΌ β
minπ-propertyβ β = refl
minπ-propertyβ β = refl

minπ-preserves-β€ : {a b a' b' : π} β a β€ a' β b β€ b' β minπ a b β€ minπ a' b'
minπ-preserves-β€ {β} {b} {a'} {b'} l m = l
minπ-preserves-β€ {β} {b} {β}  {b'} l m = m

Lemma[minabβ€βa] : {a b : π} β minπ a b β€ a
Lemma[minabβ€βa] {β} {b} = β
Lemma[minabβ€βa] {β} {β} = β
Lemma[minabβ€βa] {β} {β} = β

Lemma[minabβ€βb] : {a b : π} β minπ a b β€ b
Lemma[minabβ€βb] {β} {b} = β
Lemma[minabβ€βb] {β} {β} = β
Lemma[minabβ€βb] {β} {β} = β

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 = 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] {β} {β} 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π-comm : (b c : π) β maxπ b c οΌ maxπ c b
maxπ-comm β β = refl
maxπ-comm β β = refl
maxπ-comm β β = refl
maxπ-comm β β = refl

maxπ-idemp : (b : π) β maxπ b b οΌ b
maxπ-idemp β = refl
maxπ-idemp β = refl

maxπ-lemma : {a b : π} β maxπ a b οΌ β β (a οΌ β) + (b οΌ β)
maxπ-lemma {β} r = inr r
maxπ-lemma {β} r = inl refl

maxπ-lemma-converse : {a b : π} β (a οΌ β) + (b οΌ β) β maxπ a b οΌ β
maxπ-lemma-converse {β} (inl r) = unique-from-π (zero-is-not-one r)
maxπ-lemma-converse {β} (inr r) = r
maxπ-lemma-converse {β} x       = refl

maxπ-lemma' : {a b : π} β maxπ a b οΌ β β (a οΌ β) Γ (b οΌ β)
+ (a οΌ β) Γ (b οΌ β)
+ (a οΌ β) Γ (b οΌ β)
maxπ-lemma' {β} {β} r = inl (refl , refl)
maxπ-lemma' {β} {β} r = inr (inl (refl , refl))
maxπ-lemma' {β} {β} r = inr (inr (refl , refl))

maxπ-lemma'' : {a b : π} β maxπ a b οΌ β β (a οΌ β) Γ (b οΌ β)
+ (b οΌ β)
maxπ-lemma'' {β} {β} r = inl (refl , refl)
maxπ-lemma'' {β} {β} r = inr refl
maxπ-lemma'' {β} {β} r = inr refl

maxπ-preserves-β€ : {a b a' b' : π} β a β€ a' β b β€ b' β maxπ a b β€ maxπ a' b'
maxπ-preserves-β€ {β} {b} {β} {b'} l m = m
maxπ-preserves-β€ {β} {β} {β} {b'} l m = m
maxπ-preserves-β€ {β} {β} {β} {b'} l m = l
maxπ-preserves-β€ {β} {b} {β} {b'} l m = l

maxπ-β-left : {a b : π} β maxπ a b οΌ β β a οΌ β
maxπ-β-left {β} {b} p = refl

maxπ-β-right : {a b : π} β maxπ a b οΌ β β b οΌ β
maxπ-β-right {β} {b} p = p

\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] {β} {β} 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-β

complementβ : {a : π} β complement a οΌ β β a οΌ β
complementβ {β} refl = refl

complementβ : {a : π} β complement a οΌ β β a οΌ β
complementβ {β} refl = refl

complementβ-back : {a : π} β a οΌ β β complement a οΌ β
complementβ-back {β} refl = refl

complementβ-back : {a : π} β a οΌ β β complement a οΌ β
complementβ-back {β} refl = refl

complement-one-gives-argument-not-one : {a : π} β complement a οΌ β β a β  β
complement-one-gives-argument-not-one {β} _ = zero-is-not-one

argument-not-one-gives-complement-one : {a : π} β a β  β β complement a οΌ β
argument-not-one-gives-complement-one {β} Ξ½ = refl
argument-not-one-gives-complement-one {β} Ξ½ = π-elim (Ξ½ refl)

complement-left : {b c : π} β complement b β€ c β complement c β€ b
complement-left {β} {β} l = β
complement-left {β} {β} l = β
complement-left {β} {β} l = β

complement-right : {b c : π} β b β€ complement c β c β€ complement b
complement-right {β} {β} l = β
complement-right {β} {β} l = β
complement-right {β} {β} l = β

complement-both-left : {b c : π} β complement b β€ complement c β c β€ b
complement-both-left {β} {β} l = β
complement-both-left {β} {β} l = β
complement-both-left {β} {β} l = β

complement-both-right : {b c : π} β b β€ c β complement c β€ complement b
complement-both-right {β} {β} l = β
complement-both-right {β} {β} l = β
complement-both-right {β} {β} l = β

β-involutive : {a b : π} β a β a β b οΌ b
β-involutive {β} {b} = refl
β-involutive {β} {b} = complement-involutive b

β-assoc : {a b c : π} β (a β b) β c οΌ a β (b β c)
β-assoc {β} {b} {c} = refl
β-assoc {β} {β} {c} = refl
β-assoc {β} {β} {c} = (complement-involutive c)β»ΒΉ

β-propertyβ : {a b : π} (g : a β₯ b)
β a β b οΌ β β (a οΌ β) Γ (b οΌ β)
β-propertyβ {β} {β} g ()
β-propertyβ {β} {β} () p
β-propertyβ {β} {β} g p = refl , refl

β-introββ : {a b : π} β a οΌ β β b οΌ β β a β b οΌ β
β-introββ {β} {β} p q = refl

β-introββ : {a b : π} β a οΌ β β b οΌ β β a β b οΌ β
β-introββ {β} {β} p q = refl

β-introββ : {a b : π} β a οΌ β β b οΌ β β a β b οΌ β
β-introββ {β} {β} p q = refl

β-introββ : {a b : π} β a οΌ β β b οΌ β β a β b οΌ β
β-introββ {β} {β} p q = refl

β-β-right-neutral : {a : π} β a β β οΌ a
β-β-right-neutral {β} = refl
β-β-right-neutral {β} = refl

β-β-right-neutral' : {a b : π} β b οΌ β β a β b οΌ a
β-β-right-neutral' {β} {β} p = refl
β-β-right-neutral' {β} {β} p = refl

β-left-complement : {a b : π} β b οΌ β β a β b οΌ complement a
β-left-complement {β} {β} p = refl
β-left-complement {β} {β} p = refl

β€β-add-left : (a b : π) β b β€ a β a β b β€ a
β€β-add-left β b = Ξ» _ β β-top

β€β-remove-left : (a b : π) β a β b β€ a β b β€ a
β€β-remove-left β b = id
β€β-remove-left β b = Ξ» _ β β-top

Lemma[bοΌβ+bοΌβ] : {b : π} β (b οΌ β) + (b οΌ β)
Lemma[bοΌβ+bοΌβ] {β} = inl refl
Lemma[bοΌβ+bοΌβ] {β} = inr refl

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)

π-β-embedding : π β β
π-β-embedding β = 0
π-β-embedding β = 1

π-β-embedding-is-lc : left-cancellable π-β-embedding
π-β-embedding-is-lc {β} {β} refl = refl
π-β-embedding-is-lc {β} {β} r    = π-elim (positive-not-zero 0 (r β»ΒΉ))
π-β-embedding-is-lc {β} {β} r    = π-elim (positive-not-zero 0 r)
π-β-embedding-is-lc {β} {β} refl = refl

C-B-embedding : (β β π) β (β β β)
C-B-embedding Ξ± = π-β-embedding β Ξ±

C-B-embedding-is-lc : funext π€β π€β β left-cancellable C-B-embedding
C-B-embedding-is-lc fe {Ξ±} {Ξ²} p = dfunext fe h
where
h : (n : β) β Ξ± n οΌ Ξ² n
h n = π-β-embedding-is-lc (ap (Ξ» - β - n) p)

π-retract-of-β : retract π of β
π-retract-of-β = r , s , rs
where
r : β β π
r 0        = β
r (succ n) = β

s : π β β
s β = 0
s β = 1

rs : r β s βΌ id
rs β = refl
rs β = refl

\end{code}

Fixities and precedences:

\begin{code}

infixr 31 _β_

\end{code}