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 --auto-inline #-}

module Two-Properties where

open import SpartanMLTT
open import Unit-Properties
open import OrderNotation

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 ⁻¹)

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

βŠ•-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-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

\end{code}


Fixities and precedences:

\begin{code}

infixr 31 _βŠ•_

\end{code}