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𝟚-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𝟚-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-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

complement-introβ‚€ : {a : 𝟚} β†’ a = β‚€ β†’ complement a = ₁
complement-introβ‚€ {β‚€} p = refl

complement-one-gives-argument-not-one : {a : 𝟚} β†’ complement a = ₁ β†’ a β‰  ₁
complement-one-gives-argument-not-one {β‚€} _ = zero-is-not-one

complement-intro₁ : {a : 𝟚} β†’ a = ₁ β†’ complement a = β‚€
complement-intro₁ {₁} p = 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)

𝟚-β„•-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}