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.CanonicalMap
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
complement-lc : (b c : π) β complement b οΌ complement c β b οΌ c
complement-lc β β refl = refl
complement-lc β β p = p β»ΒΉ
complement-lc β β p = p β»ΒΉ
complement-lc β β refl = 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}
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-β
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 = id
β€β-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)
π-to-β : π β β
π-to-β β = 0
π-to-β β = 1
instance
Canonical-Map-π-β : Canonical-Map π β
ΞΉ {{Canonical-Map-π-β}} = π-to-β
π-to-β-is-lc : left-cancellable π-to-β
π-to-β-is-lc {β} {β} refl = refl
π-to-β-is-lc {β} {β} r = π-elim (positive-not-zero 0 (r β»ΒΉ))
π-to-β-is-lc {β} {β} r = π-elim (positive-not-zero 0 r)
π-to-β-is-lc {β} {β} refl = refl
C-B-embedding : (β β π) β (β β β)
C-B-embedding Ξ± = π-to-β β Ξ±
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 = π-to-β-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}