Martin Escardo, 4th August 2020. (Going back to 1993 or earlier.)

A construction of the initial binary system in Spartan MLTT, without
HITs or quotients, or extensionality axioms.

A binary system is a set A with distinguished points a b : A and
functions f g : A β†’ A such that

 (1) a = f a,
 (2) b = g b,
 (3) f b = g a.

The initial binary system is the closed interval of dyadic rationals
(see below for a picture).

We construct it as a quotient of the following type 𝔹, with L,R,l,r
corresponding to a,b,f,g, without assuming that our type theory has
quotients - it just happens to have the quotient we want.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module BinarySystems.InitialBinarySystem where

open import MLTT.Spartan
open import UF.Sets-Properties
open import UF.Subsingletons-Properties

data 𝔹 : 𝓀₀ Μ‡ where
 L R : 𝔹
 l r : 𝔹 β†’ 𝔹

\end{code}

We want to perform the identifications

 (1) L = l L,
 (2) R = r R,
 (3) l R = C = r L,

so that l and r become congruences. We call C (for "center") the equal
points of (3).

Here is a pictorial illustration of what we have in mind:


    Left endpoint    center  right endpoint

    L                  C                  R
    [------------------+------------------]  (the dyadic closed interval)
                       |
    [ image of l       |       image of r ]
                       v
          common point of the images


Geometrically, the functions l and r are supposed to be affine
transformations that scale and translate the interval to two smaller
copies with a common overlapping point.

To perform the identifications, we could quotient or use a HIT (higher
inductive type). We instead take a retract, defined by the fixed
points of an idempotent normalization function.

We take the biased choice l R for C before we perform the
identification (3). This will be the canonical, or normal-form
representative of the common point of the images.

More generally, a binary system is a type A with distinguished points
a b : A and functions f g : A β†’ A such that

 (1) a = f a,
 (2) b = g b,
 (3) f b = g a.

What we want to do is to quotient the type 𝔹, so that the quotient map
is retraction, to get the initial binary system.

\begin{code}

C : 𝔹
C = l R

is-normal : 𝔹 β†’ 𝓀₀ Μ‡
is-normal L         = πŸ™
is-normal R         = πŸ™
is-normal (l L)     = 𝟘
is-normal (l R)     = πŸ™
is-normal (l (l x)) = is-normal (l x)
is-normal (l (r x)) = is-normal (r x)
is-normal (r L)     = 𝟘
is-normal (r R)     = 𝟘
is-normal (r (l x)) = is-normal (l x)
is-normal (r (r x)) = is-normal (r x)

\end{code}

The following can be proved directly, but it also follows from the
result proved below that we have an idempotent normalization function
with the normal elements as its fixed points, and from the fact that 𝔹
has decidable equality (not proved here).

\begin{code}

normality-is-decidable : (x : 𝔹) β†’ is-normal x + Β¬ is-normal x
normality-is-decidable L         = inl ⋆
normality-is-decidable R         = inl ⋆
normality-is-decidable (l L)     = inr id
normality-is-decidable (l R)     = inl ⋆
normality-is-decidable (l (l x)) = normality-is-decidable (l x)
normality-is-decidable (l (r x)) = normality-is-decidable (r x)
normality-is-decidable (r L)     = inr id
normality-is-decidable (r R)     = inr id
normality-is-decidable (r (l x)) = normality-is-decidable (l x)
normality-is-decidable (r (r x)) = normality-is-decidable (r x)

\end{code}

We don't use the fact that normality is decidable anywhere in this
file, but, because the proof is so easy, we couldn't resist including
it.

To define the normalization function, we define versions 𝕝 and 𝕣 of l
and r that preserve normality.

\begin{code}

𝕝 : 𝔹 β†’ 𝔹
𝕝 L     = L
𝕝 R     = C
𝕝 (l x) = l (l x)
𝕝 (r x) = l (r x)

𝕣 : 𝔹 β†’ 𝔹
𝕣 L         = C
𝕣 R         = R
𝕣 (l x)     = r (l x)
𝕣 (r L)     = r C
𝕣 (r R)     = R
𝕣 (r (l x)) = r (r (l x))
𝕣 (r (r x)) = r (r (r x))

\end{code}

The fact that the construction of 𝕣 is not the symmetric version of
that of 𝕝 (and that it is longer) corresponds to the fact that we made
a biased choice for the normal form of the center C, favouring l.

The preservation proofs are by case analysis without induction:

\begin{code}

𝕝-preserves-normality : (x : 𝔹) β†’ is-normal x β†’ is-normal (𝕝 x)
𝕝-preserves-normality L     i = ⋆
𝕝-preserves-normality R     i = ⋆
𝕝-preserves-normality (l x) i = i
𝕝-preserves-normality (r x) i = i

𝕣-preserves-normality : (x : 𝔹) β†’ is-normal x β†’ is-normal (𝕣 x)
𝕣-preserves-normality L         ⋆ = ⋆
𝕣-preserves-normality R         ⋆ = ⋆
𝕣-preserves-normality (l R)     ⋆ = ⋆
𝕣-preserves-normality (l (l x)) i = i
𝕣-preserves-normality (l (r x)) i = i
𝕣-preserves-normality (r (l x)) i = i
𝕣-preserves-normality (r (r x)) i = i

\end{code}

The normalization function replaces l and r by their "semantic"
versions 𝕝 and 𝕣:

\begin{code}

normalize : 𝔹 β†’ 𝔹
normalize L     = L
normalize R     = R
normalize (l x) = 𝕝 (normalize x)
normalize (r x) = 𝕣 (normalize x)

\end{code}

By construction, the result of normalization is normal, with a direct
proof by induction:

\begin{code}

normalize-is-normal : (x : 𝔹) β†’ is-normal (normalize x)
normalize-is-normal L     = ⋆
normalize-is-normal R     = ⋆
normalize-is-normal (l x) = 𝕝-preserves-normality (normalize x) (normalize-is-normal x)
normalize-is-normal (r x) = 𝕣-preserves-normality (normalize x) (normalize-is-normal x)

\end{code}

We now prove that normal points are fixed points of the normalization
function. We need a simple lemma for that purpose, proved by case
analysis.

\begin{code}

𝕣r-equation : (x : 𝔹) β†’ is-normal (r x) β†’ 𝕣 (r x) ＝ r (r x)
𝕣r-equation L     i = 𝟘-elim i
𝕣r-equation R     i = 𝟘-elim i
𝕣r-equation (l x) i = refl
𝕣r-equation (r x) i = refl

\end{code}

To prove that normal points are fixed points of the normalization
function, we need to simultaneously prove two lemmas by induction:

\begin{code}

nfp-lemma-l : (x : 𝔹) β†’ is-normal (l x) β†’ 𝕝 (normalize x) ＝ l x
nfp-lemma-r : (x : 𝔹) β†’ is-normal (r x) β†’ 𝕣 (normalize x) ＝ r x

nfp-lemma-l L     i = 𝟘-elim i
nfp-lemma-l R     ⋆ = refl
nfp-lemma-l (l x) i = ap 𝕝 (nfp-lemma-l x i)
nfp-lemma-l (r x) i = ap 𝕝 (nfp-lemma-r x i)

nfp-lemma-r L     i = 𝟘-elim i
nfp-lemma-r R     i = 𝟘-elim i
nfp-lemma-r (l x) i = ap 𝕣 (nfp-lemma-l x i)
nfp-lemma-r (r x) i = 𝕣 (𝕣 (normalize x)) ＝⟨ ap 𝕣 (nfp-lemma-r x i) ⟩
                      𝕣 (r x)             ＝⟨ 𝕣r-equation x i ⟩
                      r (r x)             ∎
\end{code}

Now the proof of the desired result is by cases (without induction),
using the above two lemmas.

\begin{code}

normals-are-fixed-points : (x : 𝔹) β†’ is-normal x β†’ normalize x ＝ x
normals-are-fixed-points L     ⋆ = refl
normals-are-fixed-points R     ⋆ = refl
normals-are-fixed-points (l x) i = nfp-lemma-l x i
normals-are-fixed-points (r x) i = nfp-lemma-r x i

\end{code}

We have the following two corollaries:

\begin{code}

fixed-points-are-normal : (x : 𝔹) β†’ normalize x ＝ x β†’ is-normal x
fixed-points-are-normal x p = transport is-normal p (normalize-is-normal x)

normalization-idemp : (x : 𝔹) β†’ normalize (normalize x) ＝ normalize x
normalization-idemp x = normals-are-fixed-points (normalize x) (normalize-is-normal x)

\end{code}

We now show that 𝔹is a set in the sense of univalent mathematics and
that it has decidable equality. There are short proofs of some of the
following lemmas in Agda. But we are restricting ourselves to a
fragment of Agda corresponding to a spartan Martin-LΓΆf type theory. In
particular, in MLTT, it is not possible to prove that L β‰  R without
using a universe, but Agda just gives this as a fact.

We want to show that the equality of 𝔹is truth valued, as opposed to
arbitrary-type valued, where a truth value, or proposition, is a type
with at most one element. For that purpose, we first define our own
truth valued equality, where Ξ©β‚€ is the type of truth values in the
first universe 𝓀₀.

\begin{code}

open import UF.Hedberg
open import UF.Sets
open import UF.SubtypeClassifier
open import UF.Subsingletons hiding (center)

Ο‡ : 𝔹 β†’ 𝔹 β†’ Ξ©β‚€
Ο‡ L    L      = ⊀
Ο‡ L    R      = βŠ₯
Ο‡ L    (l y)  = βŠ₯
Ο‡ L    (r y)  = βŠ₯
Ο‡ R    L      = βŠ₯
Ο‡ R    R      = ⊀
Ο‡ R    (l y)  = βŠ₯
Ο‡ R    (r y)  = βŠ₯
Ο‡ (l x) L     = βŠ₯
Ο‡ (l x) R     = βŠ₯
Ο‡ (l x) (l y) = Ο‡ x y
Ο‡ (l x) (r y) = βŠ₯
Ο‡ (r x) L     = βŠ₯
Ο‡ (r x) R     = βŠ₯
Ο‡ (r x) (l y) = βŠ₯
Ο‡ (r x) (r y) = Ο‡ x y

_＝[𝔹]_ : 𝔹 β†’ 𝔹 β†’ 𝓀₀ Μ‡
x ＝[𝔹] y = Ο‡ x y holds

＝[𝔹]-is-prop-valued : (x y : 𝔹) β†’ is-prop (x ＝[𝔹] y)
＝[𝔹]-is-prop-valued x y = holds-is-prop (Ο‡ x y)

refl[𝔹] : (x : 𝔹) β†’ x ＝[𝔹] x
refl[𝔹] L     = ⋆
refl[𝔹] R     = ⋆
refl[𝔹] (l x) = refl[𝔹] x
refl[𝔹] (r x) = refl[𝔹] x

\end{code}

The induction principle for our notion of equality:

\begin{code}

J𝔹 : (x : 𝔹) (A : (y : 𝔹) β†’ x ＝[𝔹] y β†’ π“₯ Μ‡ )
    β†’ A x (refl[𝔹] x) β†’ (y : 𝔹) (r : x ＝[𝔹] y) β†’ A y r
J𝔹 L     A b L     ⋆ = b
J𝔹 L     A b R     p = 𝟘-elim p
J𝔹 L     A b (l y) p = 𝟘-elim p
J𝔹 L     A b (r y) p = 𝟘-elim p
J𝔹 R     A b L     p = 𝟘-elim p
J𝔹 R     A b R     ⋆ = b
J𝔹 R     A b (l y) p = 𝟘-elim p
J𝔹 R     A b (r y) p = 𝟘-elim p
J𝔹 (l x) A b L     p = 𝟘-elim p
J𝔹 (l x) A b R     p = 𝟘-elim p
J𝔹 (l x) A b (l y) p = J𝔹 x (A ∘ l) b y p
J𝔹 (l x) A b (r y) p = 𝟘-elim p
J𝔹 (r x) A b L     p = 𝟘-elim p
J𝔹 (r x) A b R     p = 𝟘-elim p
J𝔹 (r x) A b (l y) p = 𝟘-elim p
J𝔹 (r x) A b (r y) p = J𝔹 x (A ∘ r) b y p

\end{code}

From this we get back and forth conversions between our notion of
equality and the one of MLTT, where Jbased is the "based" induction
principle for MLTT equality.

\begin{code}

from-＝[𝔹] : (x y : 𝔹) β†’ x ＝[𝔹] y β†’ x ＝ y
from-＝[𝔹] x = J𝔹 x (Ξ» y p β†’ x ＝ y) refl

to-＝[𝔹] : (x y : 𝔹) β†’ x ＝ y β†’ x ＝[𝔹] y
to-＝[𝔹] x = Jbased x (Ξ» y p β†’ x ＝[𝔹] y) (refl[𝔹] x)

\end{code}

To show that 𝔹is a set, it is enough to prove that the type x ＝ y has
a constant endomap. We construct it as the composition of our forth
and back conversions. It is constant because our notion of equality is
truth valued (any two elements of our equality type are equal).

\begin{code}

𝔹-is-set : is-set 𝔹
𝔹-is-set = Id-collapsibles-are-sets (f , ΞΊ)
 where
  f : {x y : 𝔹} β†’ x ＝ y β†’ x ＝ y
  f {x} {y} p = from-＝[𝔹] x y (to-＝[𝔹] x y p)

  ΞΊ : {x y : 𝔹} (p q : x ＝ y) β†’ f p ＝ f q
  ΞΊ {x} {y} p q = u
   where
    t : to-＝[𝔹] x y p ＝ to-＝[𝔹] x y q
    t = ＝[𝔹]-is-prop-valued x y (to-＝[𝔹] x y p) (to-＝[𝔹] x y q)

    u : from-＝[𝔹] x y (to-＝[𝔹] x y p) ＝ from-＝[𝔹] x y (to-＝[𝔹] x y q)
    u = ap (from-＝[𝔹] x y) t

\end{code}

Another way to show that a type is a set is to show that it has
decidable equality, as is well known, which is the original version of
Hedberg's Theorem.

\begin{code}

＝[𝔹]-is-decidable : (x y : 𝔹) β†’ (x ＝[𝔹] y) + Β¬ (x ＝[𝔹] y)
＝[𝔹]-is-decidable L     L     = inl ⋆
＝[𝔹]-is-decidable L     R     = inr id
＝[𝔹]-is-decidable L     (l y) = inr id
＝[𝔹]-is-decidable L     (r y) = inr id
＝[𝔹]-is-decidable R     L     = inr id
＝[𝔹]-is-decidable R     R     = inl ⋆
＝[𝔹]-is-decidable R     (l y) = inr id
＝[𝔹]-is-decidable R     (r y) = inr id
＝[𝔹]-is-decidable (l x) L     = inr id
＝[𝔹]-is-decidable (l x) R     = inr id
＝[𝔹]-is-decidable (l x) (l y) = ＝[𝔹]-is-decidable x y
＝[𝔹]-is-decidable (l x) (r y) = inr id
＝[𝔹]-is-decidable (r x) L     = inr id
＝[𝔹]-is-decidable (r x) R     = inr id
＝[𝔹]-is-decidable (r x) (l y) = inr id
＝[𝔹]-is-decidable (r x) (r y) = ＝[𝔹]-is-decidable x y

𝔹-has-decidable-equality : (x y : 𝔹) β†’ (x ＝ y) + Β¬ (x ＝ y)
𝔹-has-decidable-equality x y = Ξ΄ (＝[𝔹]-is-decidable x y)
 where
  Ξ΄ : (x ＝[𝔹] y) + Β¬ (x ＝[𝔹] y) β†’ (x ＝ y) + Β¬ (x ＝ y)
  Ξ΄ (inl p) = inl (from-＝[𝔹] x y p)
  Ξ΄ (inr Ξ½) = inr (contrapositive (to-＝[𝔹] x y) Ξ½)

\end{code}

So we get an alternative proof that normality is decidable: an element
x of 𝔹 is normal if and only if normalize x ＝ x.

But we actually don't need the normalization procedure to construct
the initial binary system, whose underlying type will be called 𝕄.
However, we will use some of the above machinery.

\begin{code}

𝕄 : 𝓀₀ Μ‡
𝕄 = Ξ£ x κž‰ 𝔹 , is-normal x

being-normal-is-prop : (x : 𝔹) β†’ is-prop (is-normal x)
being-normal-is-prop L         = πŸ™-is-prop
being-normal-is-prop R         = πŸ™-is-prop
being-normal-is-prop (l L)     = 𝟘-is-prop
being-normal-is-prop (l R)     = πŸ™-is-prop
being-normal-is-prop (l (l x)) = being-normal-is-prop (l x)
being-normal-is-prop (l (r x)) = being-normal-is-prop (r x)
being-normal-is-prop (r L)     = 𝟘-is-prop
being-normal-is-prop (r R)     = 𝟘-is-prop
being-normal-is-prop (r (l x)) = being-normal-is-prop (l x)
being-normal-is-prop (r (r x)) = being-normal-is-prop (r x)

𝕄-is-set : is-set 𝕄
𝕄-is-set = subsets-of-sets-are-sets 𝔹 is-normal 𝔹-is-set
             (Ξ» {x} β†’ being-normal-is-prop x)

Left Center Right : 𝕄
Left   = L , ⋆
Center = C , ⋆
Right  = R , ⋆

left right : 𝕄 β†’ 𝕄
left  (x , i) = 𝕝 x , 𝕝-preserves-normality x i
right (x , i) = 𝕣 x , 𝕣-preserves-normality x i

𝕄-eq-lR-C : left Right ＝ Center
𝕄-eq-lR-C = refl

𝕄-eq-rL-C : right Left ＝ Center
𝕄-eq-rL-C = refl

𝕄-eq-l : Left ＝ left Left
𝕄-eq-l = refl

𝕄-eq-r : Right ＝ right Right
𝕄-eq-r = refl

𝕄-eq-lr : left Right ＝ right Left
𝕄-eq-lr = refl

𝕄-eq-lm : left Right ＝ Center
𝕄-eq-lm = refl

𝕄-eq-rm : right Left ＝ Center
𝕄-eq-rm = refl

\end{code}

We now use the above to show that 𝕄 is the initial binary system.

\begin{code}

binary-system-structure : 𝓀 Μ‡ β†’ 𝓀 Μ‡
binary-system-structure A = A Γ— A Γ— (A β†’ A) Γ— (A β†’ A)

binary-system-axioms : (A : 𝓀 Μ‡ ) β†’ binary-system-structure A β†’ 𝓀 Μ‡
binary-system-axioms A (a , b , f , g) = is-set A Γ— (a ＝ f a) Γ— (f b ＝ g a) Γ— (b ＝ g b)

BS : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
BS 𝓀 = Ξ£ A κž‰ 𝓀 Μ‡ , Ξ£ s κž‰ binary-system-structure A , binary-system-axioms A s

π“œ : BS 𝓀₀
π“œ = (𝕄 , (Left , Right , left , right) , (𝕄-is-set , 𝕄-eq-l , 𝕄-eq-lr , 𝕄-eq-r))

open import UF.SIP
open sip

\end{code}

The notion of homomorphism of binary systems is the expected one:

\begin{code}

is-hom : (𝓐 : BS 𝓀) (𝓐' : BS π“₯) β†’ (⟨ 𝓐 ⟩ β†’ ⟨ 𝓐' ⟩) β†’ 𝓀 βŠ” π“₯ Μ‡
is-hom (A , (a , b , f , g) , _) (A' , (a' , b' , f' , g') , _) h =
   (h a ＝ a')
 Γ— (h b ＝ b')
 Γ— (h ∘ f ∼ f' ∘ h)
 Γ— (h ∘ g ∼ g' ∘ h)

\end{code}

In order to show that π“œ is the initial binary system, we first prove
(the expected) induction principle for its underlying type 𝕄 (with a
perhaps unexpected proof):

\begin{code}

𝕄-inductive : (P : 𝕄 β†’ 𝓀 Μ‡ )
            β†’ P Left
            β†’ P Right
            β†’ ((x : 𝕄) β†’ P x β†’ P (left x))
            β†’ ((x : 𝕄) β†’ P x β†’ P (right x))
            β†’ 𝓀 Μ‡
𝕄-inductive P a b f g = ((x : 𝕄) β†’ is-set (P x))
                       Γ— (a ＝ f Left a)
                       Γ— (f Right b ＝ g Left a)
                       Γ— (b ＝ g Right b)


𝕄-induction : (P : 𝕄 β†’ 𝓀 Μ‡ )
            β†’ (a : P Left)
            β†’ (b : P Right)
            β†’ (f : (x : 𝕄) β†’ P x β†’ P (left x))
            β†’ (g : (x : 𝕄) β†’ P x β†’ P (right x))
            β†’ 𝕄-inductive P a b f g
            β†’ (x : 𝕄) β†’ P x

𝕄-induction P a b f g ΞΉ (L ,           ⋆) = a
𝕄-induction P a b f g ΞΉ (R ,           ⋆) = b
𝕄-induction P a b f g ΞΉ (l R ,         i) = f (R , ⋆) b
𝕄-induction P a b f g ΞΉ (l (l x) ,     i) = f (l x , i) (𝕄-induction P a b f g ΞΉ (l x , i))
𝕄-induction P a b f g ΞΉ (l (r x) ,     i) = f (r x , i) (𝕄-induction P a b f g ΞΉ (r x , i))
𝕄-induction P a b f g ΞΉ (r (l R) ,     i) = g (l R , ⋆) (f (R , ⋆) b)
𝕄-induction P a b f g ΞΉ (r (l (l x)) , i) = g (l (l x) , i) (𝕄-induction P a b f g ΞΉ (l (l x) , i))
𝕄-induction P a b f g ΞΉ (r (l (r x)) , i) = g (l (r x) , i) (𝕄-induction P a b f g ΞΉ (l (r x) , i))
𝕄-induction P a b f g ΞΉ (r (r (l x)) , i) = g (r (l x) , i) (𝕄-induction P a b f g ΞΉ (r (l x) , i))
𝕄-induction P a b f g ΞΉ (r (r (r x)) , i) = g (r (r x) , i) (𝕄-induction P a b f g ΞΉ (r (r x) , i))

\end{code}

In MLTT, induction principles come with equations. In our case they
are the expected ones.

\begin{code}

𝕄-induction-eq-Left : (P : 𝕄 β†’ 𝓀 Μ‡ )
                      (a : P Left)
                      (b : P Right)
                      (f : (x : 𝕄) β†’ P x β†’ P (left x))
                      (g : (x : 𝕄) β†’ P x β†’ P (right x))
                      (ΞΉ : 𝕄-inductive P a b f g)
                    β†’ 𝕄-induction P a b f g ΞΉ Left ＝ a

𝕄-induction-eq-Left P a b f g _ = refl


𝕄-induction-eq-Right : (P : 𝕄 β†’ 𝓀 Μ‡ )
                      (a : P Left)
                      (b : P Right)
                      (f : (x : 𝕄) β†’ P x β†’ P (left x))
                      (g : (x : 𝕄) β†’ P x β†’ P (right x))
                      (ΞΉ : 𝕄-inductive P a b f g)
                     β†’ 𝕄-induction P a b f g ΞΉ Right ＝ b

𝕄-induction-eq-Right P a b f g _ = refl

\end{code}

For the next equation for the induction principle, we need the
assumption a ＝ f Left a:

\begin{code}

𝕄-induction-eq-left : (P : 𝕄 β†’ 𝓀 Μ‡ )
                      (a : P Left)
                      (b : P Right)
                      (f : (x : 𝕄) β†’ P x β†’ P (left x))
                      (g : (x : 𝕄) β†’ P x β†’ P (right x))
                    β†’ (ΞΉ : 𝕄-inductive P a b f g)
                    β†’ (x : 𝕄) β†’ 𝕄-induction P a b f g ΞΉ (left x) ＝ f x (𝕄-induction P a b f g ΞΉ x)

𝕄-induction-eq-left P a b f g ΞΉ (L ,   ⋆) = pr₁ (prβ‚‚ ΞΉ)
𝕄-induction-eq-left P a b f g ΞΉ (R ,   ⋆) = refl
𝕄-induction-eq-left P a b f g ΞΉ (l x , i) = refl
𝕄-induction-eq-left P a b f g ΞΉ (r x , i) = refl

\end{code}

And for the last equation for the induction principle, we need the two
equations f Right b ＝ g Left a and b ＝ g Right b as assumptions:

\begin{code}

𝕄-induction-eq-right : (P : 𝕄 β†’ 𝓀 Μ‡ )
                      (a : P Left)
                      (b : P Right)
                      (f : (x : 𝕄) β†’ P x β†’ P (left x))
                      (g : (x : 𝕄) β†’ P x β†’ P (right x))
                    β†’ (ΞΉ : 𝕄-inductive P a b f g)
                    β†’ (x : 𝕄) β†’ 𝕄-induction P a b f g ΞΉ (right x) ＝ g x (𝕄-induction P a b f g ΞΉ x)

𝕄-induction-eq-right P a b f g ΞΉ (L ,       ⋆) = pr₁ (prβ‚‚ (prβ‚‚ ΞΉ))
𝕄-induction-eq-right P a b f g ΞΉ (R ,       ⋆) = prβ‚‚ (prβ‚‚ (prβ‚‚ ΞΉ))
𝕄-induction-eq-right P a b f g ΞΉ (l R ,     i) = refl
𝕄-induction-eq-right P a b f g ΞΉ (l (l x) , i) = refl
𝕄-induction-eq-right P a b f g ΞΉ (l (r x) , i) = refl
𝕄-induction-eq-right P a b f g ΞΉ (r (l x) , i) = refl
𝕄-induction-eq-right P a b f g ΞΉ (r (r x) , i) = refl

\end{code}

From now on we don't rely on the particular construction of 𝕄. We only
use the induction principle and its equations.

As usual, the recursion principle is a particular case of the
induction principle:

\begin{code}

π“œ-rec : (𝓐 : BS 𝓀) β†’ (𝕄 β†’ ⟨ 𝓐 ⟩)
π“œ-rec (A , (a , b , f , g) , (ι₁ , ΞΉ')) = 𝕄-induction (Ξ» _ β†’ A) a b (Ξ» _ β†’ f) (Ξ» _ β†’ g) ((Ξ» _ β†’ ι₁) , ΞΉ')

\end{code}

And so are its equations, which amount to the fact that π“œ-rec
constructs a homomorphism:

\begin{code}

π“œ-rec-is-hom : (𝓐 : BS 𝓀)
              β†’ is-hom π“œ 𝓐 (π“œ-rec 𝓐)
π“œ-rec-is-hom (A , (a , b , f , g) , ΞΉ) = i , ii , iii , iv
 where
  𝓐 = (A , (a , b , f , g) , ΞΉ)

  i : π“œ-rec 𝓐 Left ＝ a
  i = 𝕄-induction-eq-Left (Ξ» _ β†’ A) a b (Ξ» _ β†’ f) (Ξ» _ β†’ g) ((Ξ» _ β†’ pr₁ ΞΉ) , prβ‚‚ ΞΉ)

  ii : π“œ-rec 𝓐 Right ＝ b
  ii = 𝕄-induction-eq-Right (Ξ» _ β†’ A) a b (Ξ» _ β†’ f) (Ξ» _ β†’ g) ((Ξ» _ β†’ pr₁ ΞΉ) , prβ‚‚ ΞΉ)

  iii : (x : 𝕄) β†’ π“œ-rec 𝓐 (left x) ＝ f (π“œ-rec 𝓐 x)
  iii = 𝕄-induction-eq-left (Ξ» _ β†’ A) a b (Ξ» _ β†’ f) (Ξ» _ β†’ g) ((Ξ» _ β†’ pr₁ ΞΉ) , prβ‚‚ ΞΉ)

  iv : (x : 𝕄) β†’ π“œ-rec 𝓐 (right x) ＝ g (π“œ-rec 𝓐 x)
  iv = 𝕄-induction-eq-right (Ξ» _ β†’ A) a b (Ξ» _ β†’ f) (Ξ» _ β†’ g) ((Ξ» _ β†’ pr₁ ΞΉ) , prβ‚‚ ΞΉ)

\end{code}

Some boiler plate code to name the projections follows:

\begin{code}

⟨_⟩-Left : (𝓐 : BS 𝓀) β†’ ⟨ 𝓐 ⟩
⟨ (A , (a , b , f , g) , ι) ⟩-Left = a


⟨_⟩-Right : (𝓐 : BS 𝓀) β†’ ⟨ 𝓐 ⟩
⟨ (A , (a , b , f , g) , ι) ⟩-Right = b


⟨_⟩-left : (𝓐 : BS 𝓀) β†’ ⟨ 𝓐 ⟩ β†’ ⟨ 𝓐 ⟩
⟨ (A , (a , b , f , g) , ι) ⟩-left = f


⟨_⟩-right : (𝓐 : BS 𝓀) β†’ ⟨ 𝓐 ⟩ β†’ ⟨ 𝓐 ⟩
⟨ (A , (a , b , f , g) , ι) ⟩-right = g

⟨_⟩-is-set : (𝓐 : BS 𝓀) β†’ is-set ⟨ 𝓐 ⟩
⟨ (A , (a , b , f , g) , ΞΉ) ⟩-is-set = pr₁ ΞΉ


is-hom-L : (𝓐 : BS 𝓀) (𝓑 : BS π“₯) (h : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
            β†’ is-hom 𝓐 𝓑 h β†’ h (⟨ 𝓐 ⟩-Left) ＝ ⟨ 𝓑 ⟩-Left
is-hom-L 𝓐 𝓑 h (i , ii , iii , iv) = i


is-hom-R : (𝓐 : BS 𝓀) (𝓑 : BS π“₯) (h : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
             β†’ is-hom 𝓐 𝓑 h β†’ h (⟨ 𝓐 ⟩-Right) ＝ ⟨ 𝓑 ⟩-Right
is-hom-R 𝓐 𝓑 h (i , ii , iii , iv) = ii


is-hom-l : (𝓐 : BS 𝓀) (𝓑 : BS π“₯) (h : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
            β†’ is-hom 𝓐 𝓑 h β†’ h ∘ ⟨ 𝓐 ⟩-left ∼ ⟨ 𝓑 ⟩-left ∘ h
is-hom-l 𝓐 𝓑 h (i , ii , iii , iv) = iii


is-hom-r : (𝓐 : BS 𝓀) (𝓑 : BS π“₯) (h : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
             β†’ is-hom 𝓐 𝓑 h β†’ h ∘ ⟨ 𝓐 ⟩-right ∼ ⟨ 𝓑 ⟩-right ∘ h
is-hom-r 𝓐 𝓑 h (i , ii , iii , iv) = iv

\end{code}

This is the end of the boiler plate code.

To conclude that π“œ is the initial binary system, it remains to prove
that there is at most one homomorphism from it to any other binary
system.

\begin{code}

π“œ-at-most-one-hom : (𝓐 : BS 𝓀) (h k : 𝕄 β†’ ⟨ 𝓐 ⟩)
                 β†’ is-hom π“œ 𝓐 h
                 β†’ is-hom π“œ 𝓐 k
                 β†’ h ∼ k
π“œ-at-most-one-hom 𝓐 h k u v = 𝕄-induction (Ξ» x β†’ h x ＝ k x) Ξ± Ξ² Ο• Ξ³
                                 ((Ξ» x β†’ props-are-sets ⟨ 𝓐 ⟩-is-set) ,
                                  ⟨ 𝓐 ⟩-is-set Ξ± (Ο• Left Ξ±) ,
                                  ⟨ 𝓐 ⟩-is-set (Ο• Right Ξ²) (Ξ³ Left Ξ±) ,
                                  ⟨ 𝓐 ⟩-is-set Ξ² (Ξ³ Right Ξ²))
 where
  Ξ± = h Left       ＝⟨ is-hom-L π“œ 𝓐 h u ⟩
      ⟨ 𝓐 ⟩-Left   ＝⟨ (is-hom-L π“œ 𝓐 k v)⁻¹ ⟩
      k Left ∎

  Ξ² = h Right       ＝⟨ is-hom-R π“œ 𝓐 h u ⟩
       ⟨ 𝓐 ⟩-Right   ＝⟨ (is-hom-R π“œ 𝓐 k v)⁻¹ ⟩
       k Right ∎

  Ο• : (x : 𝕄) β†’ h x ＝ k x β†’ h (left x) ＝ k (left x)
  Ο• x p = h (left x)       ＝⟨ is-hom-l π“œ 𝓐 h u x ⟩
          ⟨ 𝓐 ⟩-left (h x) ＝⟨ ap ⟨ 𝓐 ⟩-left p ⟩
          ⟨ 𝓐 ⟩-left (k x) ＝⟨ (is-hom-l π“œ 𝓐 k v x)⁻¹ ⟩
          k (left x)       ∎

  Ξ³ : (x : 𝕄) β†’ h x ＝ k x β†’ h (right x) ＝ k (right x)
  Ξ³ x p =  h (right x)       ＝⟨ is-hom-r π“œ 𝓐 h u x ⟩
           ⟨ 𝓐 ⟩-right (h x) ＝⟨ ap ⟨ 𝓐 ⟩-right p ⟩
           ⟨ 𝓐 ⟩-right (k x) ＝⟨ (is-hom-r π“œ 𝓐 k v x)⁻¹ ⟩
           k (right x)       ∎


π“œ-rec-unique : (𝓐 : BS 𝓀) (h : 𝕄 β†’ ⟨ 𝓐 ⟩)
             β†’ is-hom π“œ 𝓐 h
             β†’ h ∼ π“œ-rec 𝓐
π“œ-rec-unique 𝓐 h u = π“œ-at-most-one-hom 𝓐 h (π“œ-rec 𝓐) u (π“œ-rec-is-hom 𝓐)

\end{code}

Primitive (or parametric) recursion, which has the above as a special
case:

\begin{code}

𝕄-pinductive : {A : 𝓀 Μ‡ } β†’ A β†’ A β†’ (𝕄 β†’ A β†’ A) β†’ (𝕄 β†’ A β†’ A) β†’ 𝓀 Μ‡
𝕄-pinductive {𝓀} {A} a b f g = 𝕄-inductive (Ξ» _ β†’ A) a b f g

𝕄-primrec : {A : 𝓀 Μ‡ } (a b : A) (f g : 𝕄 β†’ A β†’ A) β†’ 𝕄-pinductive a b f g β†’ 𝕄 β†’ A
𝕄-primrec {𝓀} {A} a b f g = 𝕄-induction (Ξ» _ β†’ A) a b f g

primitive-recursive : {A : 𝓀 Μ‡ } β†’ A β†’ A β†’ (𝕄 β†’ A β†’ A) β†’ (𝕄 β†’ A β†’ A) β†’ (𝕄 β†’ A) β†’ 𝓀 Μ‡
primitive-recursive a b f g h =

         (h Left  ＝ a)
       Γ— (h Right ＝ b)
       Γ— ((x : 𝕄) β†’ h (left x)  ＝ f x (h x))
       Γ— ((x : 𝕄) β†’ h (right x) ＝ g x (h x))



𝕄-primrec-primitive-recursive : {A : 𝓀 Μ‡ }
                    (a b : A)
                    (f g : 𝕄 β†’ A β†’ A)
                  β†’ (ΞΉ : 𝕄-pinductive a b f g)
                  β†’ primitive-recursive a b f g (𝕄-primrec a b f g ΞΉ)

𝕄-primrec-primitive-recursive {𝓀} {A} a b f g ΞΉ =

   𝕄-induction-eq-Left (Ξ» _ β†’ A) a b f g ΞΉ ,
   𝕄-induction-eq-Right (Ξ» _ β†’ A) a b f g ΞΉ ,
   𝕄-induction-eq-left (Ξ» _ β†’ A) a b f g ΞΉ ,
   𝕄-induction-eq-right (Ξ» _ β†’ A) a b f g ΞΉ


𝕄-at-most-one-primrec : {A : 𝓀 Μ‡ }
                    (a b : A)
                    (f g : 𝕄 β†’ A β†’ A)
                   β†’ 𝕄-pinductive a b f g
                   β†’ (h k : 𝕄 β†’ A)
                   β†’ primitive-recursive a b f g h
                   β†’ primitive-recursive a b f g k
                   β†’ h ∼ k

𝕄-at-most-one-primrec {𝓀} {A} a b f g (ι₁ , ΞΉ')  h k (hL , hR , hl , hr) (kL , kR , kl , kr) = Ξ΄
 where
  arbitrary-element-of-𝕄 = Left

  A-is-set : is-set A
  A-is-set = ι₁ arbitrary-element-of-𝕄

  α = h Left ＝⟨ hL ⟩
      a      ＝⟨ kL ⁻¹ ⟩
      k Left ∎

  β = h Right ＝⟨ hR ⟩
      b       ＝⟨ kR ⁻¹ ⟩
      k Right ∎

  Ο• : (x : 𝕄) β†’ h x ＝ k x β†’ h (left x) ＝ k (left x)
  Ο• x p = h (left x) ＝⟨ hl x ⟩
          f x (h x)  ＝⟨ ap (f x) p ⟩
          f x (k x)  ＝⟨ (kl x)⁻¹ ⟩
          k (left x) ∎

  Ξ³ : (x : 𝕄) β†’ h x ＝ k x β†’ h (right x) ＝ k (right x)
  γ x p =  h (right x) ＝⟨ hr x ⟩
           g x (h x)   ＝⟨ ap (g x) p ⟩
           g x (k x)   ＝⟨ (kr x)⁻¹ ⟩
           k (right x) ∎

  set-condition : (x : 𝕄) β†’ is-set (h x ＝ k x)
  set-condition x = props-are-sets A-is-set

  eql : Ξ± ＝ Ο• Left Ξ±
  eql = A-is-set Ξ± (Ο• Left Ξ±)

  eqlr : Ο• Right Ξ² ＝ Ξ³ Left Ξ±
  eqlr = A-is-set (Ο• Right Ξ²) (Ξ³ Left Ξ±)

  eqr : β ＝ γ Right β
  eqr = A-is-set Ξ² (Ξ³ Right Ξ²)

  δ : h ∼ k
  Ξ΄ = 𝕄-induction (Ξ» x β†’ h x ＝ k x) Ξ± Ξ² Ο• Ξ³ (set-condition , eql , eqlr , eqr)


𝕄-primrec-uniqueness : {A : 𝓀 Μ‡ }
                    (a b : A)
                    (f g : 𝕄 β†’ A β†’ A)
                   β†’ (ΞΉ : 𝕄-pinductive a b f g)
                   β†’ (h : 𝕄 β†’ A)
                   β†’ primitive-recursive a b f g h
                   β†’ h ∼ 𝕄-primrec a b f g ΞΉ

𝕄-primrec-uniqueness a b f g ΞΉ h hph = 𝕄-at-most-one-primrec a b f g ΞΉ
                                            h (𝕄-primrec a b f g ΞΉ)
                                            hph (𝕄-primrec-primitive-recursive a b f g ΞΉ)

\end{code}

Under some special conditions that often hold in practice, we can
remove the "base" case in the uniqueness theorem.

\begin{code}

is-wprimrec : {A : 𝓀 Μ‡ } β†’ (𝕄 β†’ A β†’ A) β†’ (𝕄 β†’ A β†’ A) β†’ (𝕄 β†’ A) β†’ 𝓀 Μ‡
is-wprimrec f g h = ((x : 𝕄) β†’ h (left x)  ＝ f x (h x))
                  Γ— ((x : 𝕄) β†’ h (right x) ＝ g x (h x))


primrec-is-wprimrec : {A : 𝓀 Μ‡ } (a b : A) (f g : 𝕄 β†’ A β†’ A) (h : 𝕄 β†’ A)
                    β†’ primitive-recursive a b f g h β†’ is-wprimrec f g h
primrec-is-wprimrec a b f g h (hL , hR , hl , hr) = (hl , hr)


fixed-point-conditions : {A : 𝓀 Μ‡ } β†’ A β†’ A β†’ (𝕄 β†’ A β†’ A) β†’ (𝕄 β†’ A β†’ A) β†’ 𝓀 Μ‡
fixed-point-conditions a b f g = (βˆ€ a' β†’ a' ＝ f Left  a' β†’ a' ＝ a)
                              Γ— (βˆ€ b' β†’ b' ＝ g Right b' β†’ b' ＝ b)

wprimrec-primitive-recursive : {A : 𝓀 Μ‡ } (a b : A) (f g : 𝕄 β†’ A β†’ A) (h : 𝕄 β†’ A)
                             β†’ fixed-point-conditions a b f g
                             β†’ is-wprimrec f g h β†’ primitive-recursive a b f g h
wprimrec-primitive-recursive a b f g h (fixa , fixb) (hl , hr) = (hL , hR , hl , hr)
 where
  hL' = h Left          ＝⟨ refl ⟩
        h (left Left)   ＝⟨ hl Left ⟩
        f Left (h Left) ∎

  hL = h Left ＝⟨ fixa (h Left) hL' ⟩
       a      ∎

  hR : h Right ＝ b
  hR = fixb (h Right) (hr Right)


𝕄-at-most-one-wprimrec : {A : 𝓀 Μ‡ }
                    (a b : A)
                    (f g : 𝕄 β†’ A β†’ A)
                   β†’ (ΞΉ : 𝕄-pinductive a b f g)
                   β†’ fixed-point-conditions a b f g
                   β†’ (h k : 𝕄 β†’ A)
                   β†’ is-wprimrec f g h
                   β†’ is-wprimrec f g k
                   β†’ h ∼ k

𝕄-at-most-one-wprimrec a b f g ΞΉ fixc h k (hl , hr) (kl , kr) =

  𝕄-at-most-one-primrec a b f g ΞΉ h k
    (wprimrec-primitive-recursive a b f g h fixc (hl , hr))
    (wprimrec-primitive-recursive a b f g k fixc (kl , kr))


𝕄-wprimrec-uniqueness : {A : 𝓀 Μ‡ }
                    (a b : A)
                    (f g : 𝕄 β†’ A β†’ A)
                   β†’ (ΞΉ : 𝕄-pinductive a b f g)
                   β†’ fixed-point-conditions a b f g
                   β†’ (h : 𝕄 β†’ A)
                   β†’ is-wprimrec f g h
                   β†’ h ∼ 𝕄-primrec a b f g ΞΉ

𝕄-wprimrec-uniqueness a b f g ΞΉ fixc h hph =
  𝕄-at-most-one-wprimrec a b f g ΞΉ fixc h
   (𝕄-primrec a b f g ΞΉ) hph
   (primrec-is-wprimrec a b f g ( 𝕄-primrec a b f g ΞΉ) (𝕄-primrec-primitive-recursive a b f g ΞΉ))

\end{code}

Definition by cases of functions 𝕄 β†’ A is a particular case of
parametric recursion.

Given a b : A and f g : 𝕄 β†’ A, we want to define h : 𝕄 β†’ A by cases as
follows:

      h Left      ＝ a
      h Right     ＝ b
      h (left x)  = f x
      h (right x) = g x

For this to be well defined we need the following endpoint agreement
conditions:

  (1) a ＝ f Left,
  (2) f Right ＝ g Left,
  (3) b ＝ g Right.

If we take a = f Left and b = g Left, so that (1) and (2) hold, we are
left with condition (3) as the only assumption, and the condition on h
becomes

      h Left      ＝ f Left,
      h Right     ＝ g Right,
      h (left x)  = f x,
      h (right x) = g x.

But also the first two equations follow from the second two, since

     h Left  = h (left Left)   = f Left,
     h Right = h (right Right) = g right.

Hence it is enough to consider the endpoint agreement condition (3)
and work with the equations

      h (left x)  = f x,
      h (right x) = g x.

Hence 𝕄-cases gives the mediating map of a pushout diagram that glues
two copies of the dyadic interval, identifying the end of one with the
beginning of the other, so that 𝕄 is equivalent to the pushout 𝕄 +₁ 𝕄:

      𝕄 ≃ 𝕄 +₁ 𝕄

when f = left and g = right. The function 𝕄-cases defined below
produces the mediating map of the pushout:

The following constructions and facts are all particular cases of
those for 𝕄-primrec.

\begin{code}

𝕄-caseable : (A : 𝓀 Μ‡ ) β†’ (𝕄 β†’ A) β†’ (𝕄 β†’ A) β†’ 𝓀 Μ‡
𝕄-caseable A f g = is-set A Γ— (f Right ＝ g Left)

𝕄-caseable-gives-pinductive : (A : 𝓀 Μ‡ ) (f g : 𝕄 β†’ A)
                             β†’ 𝕄-caseable A f g
                             β†’ 𝕄-pinductive (f Left) (g Right) (Ξ» x _ β†’ f x) (Ξ» x _ β†’ g x)
𝕄-caseable-gives-pinductive A f g (A-is-set , p) = (Ξ» _ β†’ A-is-set) , refl , p , refl

𝕄-cases : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) β†’ 𝕄-caseable A f g β†’ 𝕄 β†’ A
𝕄-cases f g ΞΉ = 𝕄-primrec (f Left) (g Right) (Ξ» x _ β†’ f x) (Ξ» x _ β†’ g x) (𝕄-caseable-gives-pinductive _ f g ΞΉ)


case-equations : {A : 𝓀 Μ‡ } β†’ (𝕄 β†’ A) β†’ (𝕄 β†’ A) β†’ (𝕄 β†’ A) β†’ 𝓀 Μ‡
case-equations f g h = (h ∘ left  ∼ f)
                     Γ— (h ∘ right ∼ g)

𝕄-cases-redundant-equations : {A : 𝓀 Μ‡ }
                    (f g : 𝕄 β†’ A)
                  β†’ (p : 𝕄-caseable A f g)
                  β†’ (𝕄-cases f g p Left    ＝ f Left)
                  Γ— (𝕄-cases f g p Right   ＝ g Right)
                  Γ— (𝕄-cases f g p ∘ left  ∼ f)
                  Γ— (𝕄-cases f g p ∘ right ∼ g)

𝕄-cases-redundant-equations f g ΞΉ = 𝕄-primrec-primitive-recursive
                                      (f Left) (g Right)
                                      (Ξ» x _ β†’ f x)
                                      (Ξ» x _ β†’ g x)
                                      (𝕄-caseable-gives-pinductive _ f g ΞΉ)


𝕄-cases-equations : {A : 𝓀 Μ‡ }
                    (f g : 𝕄 β†’ A)
                  β†’ (p : 𝕄-caseable A f g)
                  β†’ case-equations f g (𝕄-cases f g p)

𝕄-cases-equations f g p = primrec-is-wprimrec (f Left) (g Right) (Ξ» x _ β†’ f x) (Ξ» x _ β†’ g x) (𝕄-cases f g p)
                           (𝕄-cases-redundant-equations f g p)

𝕄-at-most-one-cases : {A : 𝓀 Μ‡ }
                    (f g : 𝕄 β†’ A)
                   β†’ 𝕄-caseable A f g
                   β†’ (h k : 𝕄 β†’ A)
                   β†’ case-equations f g h
                   β†’ case-equations f g k
                   β†’ h ∼ k

𝕄-at-most-one-cases f g ΞΉ = 𝕄-at-most-one-wprimrec
                              (f Left)
                              (g Right)
                              (Ξ» x _ β†’ f x)
                              (Ξ» x _ β†’ g x)
                              (𝕄-caseable-gives-pinductive _ f g ΞΉ)
                              (u , v)
  where
   u : βˆ€ a' β†’ a' ＝ f Left β†’ a' ＝ f Left
   u a' p = p

   v : βˆ€ b' β†’ b' ＝ g Right β†’ b' ＝ g Right
   v a' p = p

𝕄-cases-uniqueness : {A : 𝓀 Μ‡ }
                 (f g : 𝕄 β†’ A)
                β†’ (p : 𝕄-caseable A f g)
                β†’ (h : 𝕄 β†’ A)
                β†’ case-equations f g h
                β†’ h ∼ 𝕄-cases f g p

𝕄-cases-uniqueness f g p h he = 𝕄-at-most-one-cases f g p h (𝕄-cases f g p) he (𝕄-cases-equations f g p)

𝕄-cases-L : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) (p : 𝕄-caseable A f g)
          β†’ 𝕄-cases f g p Left ＝ f Left
𝕄-cases-L f g p = pr₁ (𝕄-cases-redundant-equations f g p)

𝕄-cases-R : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) (p : 𝕄-caseable A f g)
          β†’ 𝕄-cases f g p Right ＝ g Right
𝕄-cases-R f g p = pr₁ (prβ‚‚ (𝕄-cases-redundant-equations f g p))

𝕄-cases-l : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) (p : 𝕄-caseable A f g)
          β†’ 𝕄-cases f g p ∘ left ∼ f
𝕄-cases-l f g p = pr₁ (prβ‚‚ (prβ‚‚ ((𝕄-cases-redundant-equations f g p))))

𝕄-cases-r : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) (p : 𝕄-caseable A f g)
          β†’ 𝕄-cases f g p ∘ right ∼ g
𝕄-cases-r f g p = prβ‚‚ (prβ‚‚ (prβ‚‚ ((𝕄-cases-redundant-equations f g p))))

\end{code}

We now specialize to A = 𝕄 for notational convenience:

\begin{code}

𝕄𝕄-caseable : (f g : 𝕄 β†’ 𝕄) β†’ 𝓀₀ Μ‡
𝕄𝕄-caseable f g = f Right ＝ g Left

𝕄𝕄-cases : (f g : 𝕄 β†’ 𝕄) β†’ 𝕄𝕄-caseable f g β†’ (𝕄 β†’ 𝕄)
𝕄𝕄-cases f g p = 𝕄-cases f g (𝕄-is-set , p)

\end{code}

Here are some examples:

\begin{code}

center : 𝕄 β†’ 𝕄
center = 𝕄𝕄-cases (left ∘ right) (right ∘ left) refl

center-l : (x : 𝕄) β†’ center (left x) ＝ left (right x)
center-l = 𝕄-cases-l _ _ (𝕄-is-set , refl)

center-r : (x : 𝕄) β†’ center (right x) ＝ right (left x)
center-r = 𝕄-cases-r _ _ (𝕄-is-set , refl)

left-by-cases : left ∼ 𝕄𝕄-cases (left ∘ left) (center ∘ left) refl
left-by-cases = 𝕄-cases-uniqueness _ _
                  (𝕄-is-set , refl) left ((Ξ» x β†’ refl) , Ξ» x β†’ (center-l x)⁻¹)

right-by-cases : right ∼ 𝕄𝕄-cases (center ∘ right) (right ∘ right) refl
right-by-cases = 𝕄-cases-uniqueness _ _
                   (𝕄-is-set , refl) right ((Ξ» x β†’ (center-r x)⁻¹) , (Ξ» x β†’ refl))

\end{code}

We now define the midpoint operation _βŠ•_ : 𝕄 β†’ (𝕄 β†’ 𝕄) by
initiality. We will work with a subset of the function type 𝕄 β†’ 𝕄 and
make it into a binary system.

\begin{code}

is-𝓛-function : (𝕄 β†’ 𝕄) β†’ 𝓀₀ Μ‡
is-𝓛-function f = 𝕄𝕄-caseable (left ∘ f) (center ∘ f)

is-𝓑-function : (𝕄 β†’ 𝕄) β†’ 𝓀₀ Μ‡
is-𝓑-function f = 𝕄𝕄-caseable (center ∘ f) (right ∘ f)

𝓛 : (f : 𝕄 β†’ 𝕄) β†’ is-𝓛-function f β†’ (𝕄 β†’ 𝕄)
𝓛 f = 𝕄𝕄-cases (left ∘ f) (center ∘ f)

𝓑 : (f : 𝕄 β†’ 𝕄) β†’ is-𝓑-function f β†’ (𝕄 β†’ 𝕄)
𝓑 f = 𝕄𝕄-cases (center ∘ f) (right ∘ f)

preservation-𝓛𝓛 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓛-function (𝓛 f 𝓡)
preservation-𝓛𝓛 f 𝓡 𝓻 =
  left (𝓛 f 𝓡 Right)      ＝⟨ ap left (𝕄-cases-R (left ∘ f) (center ∘ f) (𝕄-is-set , 𝓡)) ⟩
  left (center (f Right)) ＝⟨ ap left 𝓻 ⟩
  left (right (f Left))   ＝⟨ (center-l (f Left))⁻¹ ⟩
  center (left (f Left))  ＝⟨ (ap center (𝕄-cases-L (left ∘ f) (center ∘ f) (𝕄-is-set , 𝓡)))⁻¹ ⟩
  center (𝓛 f 𝓡 Left)     ∎

preservation-𝓛𝓑 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓑-function (𝓛 f 𝓡)
preservation-𝓛𝓑 f 𝓡 𝓻 =
  center (𝓛 f 𝓡 Right)      ＝⟨ ap center (𝕄-cases-R (left ∘ f) (center ∘ f) (𝕄-is-set , 𝓡)) ⟩
  center (center (f Right)) ＝⟨ ap center 𝓻 ⟩
  center (right (f Left))   ＝⟨ center-r (f Left) ⟩
  right (left (f Left))     ＝⟨ ap right ((𝕄-cases-L (left ∘ f) (center ∘ f) (𝕄-is-set , 𝓡))⁻¹) ⟩
  right (𝓛 f 𝓡 Left)        ∎

preservation-𝓑𝓛 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓛-function (𝓑 f 𝓻)
preservation-𝓑𝓛 f 𝓡 𝓻 =
  left (𝓑 f 𝓻 Right)       ＝⟨ ap left (𝕄-cases-R (center ∘ f) (right ∘ f) (𝕄-is-set , 𝓻)) ⟩
  left (right (f Right))   ＝⟨ (center-l (f Right))⁻¹ ⟩
  center (left (f Right))  ＝⟨ ap center 𝓡 ⟩
  center (center (f Left)) ＝⟨ ap center ((𝕄-cases-L (center ∘ f) (right ∘ f) (𝕄-is-set , 𝓻))⁻¹) ⟩
  center (𝓑 f 𝓻 Left)      ∎

preservation-𝓑𝓑 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓑-function (𝓑 f 𝓻)
preservation-𝓑𝓑 f 𝓡 𝓻 =
  center (𝓑 f 𝓻 Right)     ＝⟨ ap center (𝕄-cases-R (center ∘ f) (right ∘ f) (𝕄-is-set , 𝓻)) ⟩
  center (right (f Right)) ＝⟨ 𝕄-cases-r (left ∘ right) (right ∘ left) (𝕄-is-set , refl) (f Right) ⟩
  right (left (f Right))   ＝⟨ ap right 𝓡 ⟩
  right (center (f Left))  ＝⟨ ap right ((𝕄-cases-L (center ∘ f) (right ∘ f) (𝕄-is-set , 𝓻))⁻¹) ⟩
  right (𝓑 f 𝓻 Left)       ∎

is-𝓛𝓑-function : (𝕄 β†’ 𝕄) β†’ 𝓀₀ Μ‡
is-𝓛𝓑-function f = is-𝓛-function f Γ— is-𝓑-function f

being-𝓛𝓑-function-is-prop : (f : 𝕄 β†’ 𝕄) β†’ is-prop (is-𝓛𝓑-function f)
being-𝓛𝓑-function-is-prop f = Γ—-is-prop 𝕄-is-set 𝕄-is-set

\end{code}

The desired subset of the function type 𝕄 β†’ 𝕄 is this:

\begin{code}

F : 𝓀₀ Μ‡
F = Ξ£ f κž‰ (𝕄 β†’ 𝕄) , is-𝓛𝓑-function f

\end{code}

We now need to assume function extensionality.

\begin{code}

open import UF.Base
open import UF.FunExt

module _ (fe  : Fun-Ext) where

 F-is-set : is-set F
 F-is-set = subsets-of-sets-are-sets (𝕄 β†’ 𝕄) is-𝓛𝓑-function
             (Ξ -is-set fe (Ξ» _ β†’ 𝕄-is-set))
             (Ξ» {f} β†’ being-𝓛𝓑-function-is-prop f)

 𝑙𝑒𝑓𝑑 π‘Ÿπ‘–π‘”β„Žπ‘‘ : F β†’ F
 𝑙𝑒𝑓𝑑 (f , (𝓡 , 𝓻))  = 𝓛 f 𝓡 , preservation-𝓛𝓛 f 𝓡 𝓻 , preservation-𝓛𝓑 f 𝓡 𝓻
 π‘Ÿπ‘–π‘”β„Žπ‘‘ (f , (𝓡 , 𝓻)) = 𝓑 f 𝓻 , preservation-𝓑𝓛 f 𝓡 𝓻 , preservation-𝓑𝓑 f 𝓡 𝓻

 𝐿𝑒𝑓𝑑 π‘…π‘–π‘”β„Žπ‘‘ : F
 𝐿𝑒𝑓𝑑  = left , refl , refl
 π‘…π‘–π‘”β„Žπ‘‘ = right , refl , refl

 F-eq-l : 𝐿𝑒𝑓𝑑 ＝ 𝑙𝑒𝑓𝑑 𝐿𝑒𝑓𝑑
 F-eq-l = to-subtype-＝ being-𝓛𝓑-function-is-prop Ξ³
  where
   Ξ΄ : left ∼ 𝓛 left refl
   Ξ΄ = left-by-cases

   Ξ³ : left ＝ 𝓛 left refl
   Ξ³ = dfunext fe Ξ΄


 F-eq-lr : 𝑙𝑒𝑓𝑑 π‘…π‘–π‘”β„Žπ‘‘ ＝ π‘Ÿπ‘–π‘”β„Žπ‘‘ 𝐿𝑒𝑓𝑑
 F-eq-lr = to-subtype-＝ being-𝓛𝓑-function-is-prop v
  where
   i = Ξ» (x : 𝕄) β†’ 𝕄𝕄-cases (left ∘ right) (center ∘ right) refl (left x) ＝⟨ 𝕄-cases-l _ _ (𝕄-is-set , refl) x ⟩
                   left (right x)                                           ＝⟨ (center-l x)⁻¹ ⟩
                   center (left x)                                          ∎

   ii =  Ξ» (x : 𝕄) β†’ 𝕄𝕄-cases (left ∘ right) (center ∘ right) refl (right x)   ＝⟨ 𝕄-cases-r _ _ (𝕄-is-set , refl) x ⟩
                     center (right x)                                          ＝⟨ center-r x ⟩
                     right (left x)                                            ∎

   iii : 𝕄𝕄-cases (left ∘ right)  (center ∘ right) refl
       ∼ 𝕄𝕄-cases (center ∘ left) (right ∘ left)   refl
   iii = 𝕄-cases-uniqueness _ _ (𝕄-is-set , refl) (𝕄𝕄-cases _ _ refl) (i , ii)

   iv : 𝓛 right refl ∼ 𝓑 left refl
   iv = iii

   v : 𝓛 right refl ＝ 𝓑 left refl
   v = dfunext fe iv


 F-eq-r : π‘…π‘–π‘”β„Žπ‘‘ ＝ π‘Ÿπ‘–π‘”β„Žπ‘‘ π‘…π‘–π‘”β„Žπ‘‘
 F-eq-r = to-subtype-＝ being-𝓛𝓑-function-is-prop Ξ³
  where
   Ξ΄ : right ∼ 𝓑 right refl
   Ξ΄ = right-by-cases

   Ξ³ : right ＝ 𝓑 right refl
   Ξ³ = dfunext fe Ξ΄


 𝓕 : BS 𝓀₀
 𝓕 = (F , (𝐿𝑒𝑓𝑑 , π‘…π‘–π‘”β„Žπ‘‘ , 𝑙𝑒𝑓𝑑 , π‘Ÿπ‘–π‘”β„Žπ‘‘) , (F-is-set , F-eq-l , F-eq-lr , F-eq-r))

 mid : 𝕄 β†’ F
 mid = π“œ-rec 𝓕

 _βŠ•_ : 𝕄 β†’ 𝕄 β†’ 𝕄
 x βŠ• y = pr₁ (mid x) y

 βŠ•-property : (x : 𝕄)
            β†’ (left   (x βŠ• Right) ＝ center (x βŠ• Left))
            Γ— (center (x βŠ• Right) ＝ right  (x βŠ• Left))
 βŠ•-property x = prβ‚‚ (mid x)

 mid-is-hom : is-hom π“œ 𝓕 (π“œ-rec 𝓕)
 mid-is-hom = π“œ-rec-is-hom 𝓕

 mid-is-hom-L : mid Left ＝ 𝐿𝑒𝑓𝑑
 mid-is-hom-L = is-hom-L π“œ 𝓕 mid mid-is-hom

 mid-is-hom-L' : (y : 𝕄) β†’ Left βŠ• y ＝ left y
 mid-is-hom-L' y = ap (Ξ» - β†’ pr₁ - y) mid-is-hom-L

 mid-is-hom-R : mid Right ＝ π‘…π‘–π‘”β„Žπ‘‘
 mid-is-hom-R = is-hom-R π“œ 𝓕 mid mid-is-hom

 mid-is-hom-R' : (y : 𝕄) β†’ Right βŠ• y ＝ right y
 mid-is-hom-R' y = ap (Ξ» - β†’ pr₁ - y) mid-is-hom-R

 mid-is-hom-l : (x : 𝕄) β†’ mid (left x) ＝ 𝑙𝑒𝑓𝑑 (mid x)
 mid-is-hom-l = is-hom-l π“œ 𝓕 mid mid-is-hom

 mid-is-hom-l' : (x y : 𝕄)
               β†’ (left x βŠ• Left    ＝ left   (x βŠ• Left))
               Γ— (left x βŠ• Right   ＝ center (x βŠ• Right))
               Γ— (left x βŠ• left y  ＝ left   (x βŠ• y))
               Γ— (left x βŠ• right y ＝ center (x βŠ• y))
 mid-is-hom-l' x y = u , v , w , t
  where
   Ξ± = Ξ» y β†’ left x βŠ• y           ＝⟨ refl ⟩
             pr₁ (mid (left x)) y ＝⟨ happly (ap pr₁ (mid-is-hom-l x)) y ⟩
             pr₁ (𝑙𝑒𝑓𝑑 (mid x)) y   ＝⟨ refl ⟩
             𝕄𝕄-cases (left ∘ (x βŠ•_)) (center ∘ (x βŠ•_)) (pr₁ (βŠ•-property x)) y ∎

   u = Ξ± Left      βˆ™ 𝕄-cases-L (left ∘ (x βŠ•_)) (center ∘ (x βŠ•_)) (𝕄-is-set , pr₁ (βŠ•-property x))
   v = Ξ± Right     βˆ™ 𝕄-cases-R (left ∘ (x βŠ•_)) (center ∘ (x βŠ•_)) (𝕄-is-set , pr₁ (βŠ•-property x))
   w = Ξ± (left y)  βˆ™ 𝕄-cases-l (left ∘ (x βŠ•_)) (center ∘ (x βŠ•_)) (𝕄-is-set , pr₁ (βŠ•-property x)) y
   t = Ξ± (right y) βˆ™ 𝕄-cases-r (left ∘ (x βŠ•_)) (center ∘ (x βŠ•_)) (𝕄-is-set , pr₁ (βŠ•-property x)) y

 mid-is-hom-r : (x : 𝕄) β†’ mid (right x) ＝ π‘Ÿπ‘–π‘”β„Žπ‘‘ (mid x)
 mid-is-hom-r = is-hom-r π“œ 𝓕 mid mid-is-hom

 mid-is-hom-r' : (x y : 𝕄)
               β†’ (right x βŠ• Right   ＝ right  (x βŠ• Right))
               Γ— (right x βŠ• Left    ＝ center (x βŠ• Left))
               Γ— (right x βŠ• left y  ＝ center (x βŠ• y))
               Γ— (right x βŠ• right y ＝ right  (x βŠ• y))
 mid-is-hom-r' x y = u , v , w , t
  where
   Ξ± = Ξ» y β†’ right x βŠ• y           ＝⟨ refl ⟩
             pr₁ (mid (right x)) y ＝⟨ happly (ap pr₁ (mid-is-hom-r x)) y ⟩
             pr₁ (π‘Ÿπ‘–π‘”β„Žπ‘‘ (mid x)) y   ＝⟨ refl ⟩
             𝕄𝕄-cases (center ∘ (x βŠ•_)) (right ∘ (x βŠ•_)) (prβ‚‚ (βŠ•-property x)) y ∎

   u = Ξ± Right βˆ™ 𝕄-cases-R (center ∘ (x βŠ•_)) (right ∘ (x βŠ•_)) (𝕄-is-set , prβ‚‚ (βŠ•-property x))
   v = Ξ± Left βˆ™ 𝕄-cases-L (center ∘ (x βŠ•_)) (right ∘ (x βŠ•_)) (𝕄-is-set , prβ‚‚ (βŠ•-property x))
   w = Ξ± (left y)  βˆ™ 𝕄-cases-l (center ∘ (x βŠ•_)) (right ∘ (x βŠ•_)) (𝕄-is-set , prβ‚‚ (βŠ•-property x)) y
   t = Ξ± (right y) βˆ™ 𝕄-cases-r (center ∘ (x βŠ•_)) (right ∘ (x βŠ•_)) (𝕄-is-set , prβ‚‚ (βŠ•-property x)) y

\end{code}

So, the set of defining equations is the following, where it can be
seen that there is some redundancy:

     (  left   (x βŠ• Right) ＝ center (x βŠ• Left)  )
   Γ— (  center (x βŠ• Right) ＝ right  (x βŠ• Left)  )

   Γ— (  Left    βŠ• y        ＝ left y             )
   Γ— (  Right   βŠ• y        ＝ right y            )
   Γ— (  left x  βŠ• Left     ＝ left (x βŠ• Left)    )
   Γ— (  left x  βŠ• Right    ＝ center (x βŠ• Right) )
   Γ— (  left x  βŠ• left y   ＝ left (x βŠ• y)       )
   Γ— (  left x  βŠ• right y  ＝ center (x βŠ• y)     )
   Γ— (  right x βŠ• Right    ＝ right (x βŠ• Right)  )
   Γ— (  right x βŠ• Left     ＝ center (x βŠ• Left)  )
   Γ— (  right x βŠ• left y   ＝ center (x βŠ• y)     )
   Γ— (  right x βŠ• right y  ＝ right (x βŠ• y)      )

The first two come from the binary system F and the remaining ones from the homomorphism condition and cases analysis.

Next we want to show that

  _βŠ•_ : 𝕄 β†’ 𝕄 β†’ 𝕄

makes the initial binary system into the free midpoint algebra over
two generators (taken to be Left and Right, as expected), where the
midpoint axioms are

   (idempotency)    x βŠ• x ＝ x,
   (commutativity)  x βŠ• y ＝ y βŠ• x,
   (transposition)  (u βŠ• v) βŠ• (x βŠ• y) ＝ (u βŠ• x) βŠ• (v βŠ• y).

In fact, in the initial binary system, there is a unique midpoint
operation _βŠ•_ such that

   L βŠ• x = left x,
   R βŠ• x = right x.

To be continued.