Martin Escardo, 7th August 2020.

This file improves the file InitialBinarySystem.lagda, which gives the
background for this file.

\begin{code}

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

module BinarySystems.InitialBinarySystem2 where

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

data 𝔹 :  𝓀₀ Μ‡ where
 center : 𝔹
 left   : 𝔹 β†’ 𝔹
 right  : 𝔹 β†’ 𝔹

data 𝕄 : 𝓀₀ Μ‡ where
 L : 𝕄
 R : 𝕄
 Ξ· : 𝔹 β†’ 𝕄

C : 𝕄
C = Ξ· center

l : 𝕄 β†’ 𝕄
l L     = L
l R     = C
l (Ξ· x) = Ξ· (left x)

r : 𝕄 β†’ 𝕄
r L     = C
r R     = R
r (Ξ· x) = Ξ· (right x)

𝕄-eq-l : L ＝ l L
𝕄-eq-l = refl

𝕄-eq-r : R ＝ r R
𝕄-eq-r = refl

𝕄-eq-lr : l R ＝ r L
𝕄-eq-lr = refl

open import UF.Subsingletons hiding (center)

𝕄-inductive : (P : 𝕄 β†’ 𝓀 Μ‡ )
             β†’ P L
             β†’ P R
             β†’ ((x : 𝕄) β†’ P x β†’ P (l x))
             β†’ ((x : 𝕄) β†’ P x β†’ P (r x))
             β†’ 𝓀 Μ‡
𝕄-inductive P a b f g = ((x : 𝕄) β†’ is-set (P x))
                       Γ— (a ＝ f L a)
                       Γ— (f R b ＝ g L a)
                       Γ— (b ＝ g R b)


𝕄-induction : (P : 𝕄 β†’ 𝓀 Μ‡ )
            β†’ (a : P L)
            β†’ (b : P R)
            β†’ (f : (x : 𝕄) β†’ P x β†’ P (l x))
            β†’ (g : (x : 𝕄) β†’ P x β†’ P (r 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 ΞΉ (Ξ· center)    = f R b -- or g L a, but then the proofs below change.
𝕄-induction P a b f g ΞΉ (Ξ· (left x))  = f (Ξ· x) (𝕄-induction P a b f g ΞΉ (Ξ· x))
𝕄-induction P a b f g ΞΉ (Ξ· (right x)) = g (Ξ· x) (𝕄-induction P a b f g ΞΉ (Ξ· x))

\end{code}

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

\begin{code}

𝕄-induction-L : (P : 𝕄 β†’ 𝓀 Μ‡ )
                (a : P L)
                (b : P R)
                (f : (x : 𝕄) β†’ P x β†’ P (l x))
                (g : (x : 𝕄) β†’ P x β†’ P (r x))
                (ΞΉ : 𝕄-inductive P a b f g)
              β†’ 𝕄-induction P a b f g ΞΉ L ＝ a

𝕄-induction-L P a b f g _ = refl


𝕄-induction-R : (P : 𝕄 β†’ 𝓀 Μ‡ )
                (a : P L)
                (b : P R)
                (f : (x : 𝕄) β†’ P x β†’ P (l x))
                (g : (x : 𝕄) β†’ P x β†’ P (r x))
                (ΞΉ : 𝕄-inductive P a b f g)
               β†’ 𝕄-induction P a b f g ΞΉ R ＝ b

𝕄-induction-R P a b f g _ = refl

\end{code}

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

\begin{code}

𝕄-induction-l : (P : 𝕄 β†’ 𝓀 Μ‡ )
                (a : P L)
                (b : P R)
                (f : (x : 𝕄) β†’ P x β†’ P (l x))
                (g : (x : 𝕄) β†’ P x β†’ P (r x))
              β†’ (ΞΉ : 𝕄-inductive P a b f g)
              β†’ (x : 𝕄) β†’ 𝕄-induction P a b f g ΞΉ (l x) ＝ f x (𝕄-induction P a b f g ΞΉ x)

𝕄-induction-l P a b f g ΞΉ L     = pr₁ (prβ‚‚ ΞΉ)
𝕄-induction-l P a b f g ΞΉ R     = refl
𝕄-induction-l P a b f g ΞΉ (Ξ· x) = refl

\end{code}

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

\begin{code}

𝕄-induction-r : (P : 𝕄 β†’ 𝓀 Μ‡ )
                (a : P L)
                (b : P R)
                (f : (x : 𝕄) β†’ P x β†’ P (l x))
                (g : (x : 𝕄) β†’ P x β†’ P (r x))
              β†’ (ΞΉ : 𝕄-inductive P a b f g)
              β†’ (x : 𝕄) β†’ 𝕄-induction P a b f g ΞΉ (r x) ＝ g x (𝕄-induction P a b f g ΞΉ x)

𝕄-induction-r P a b f g ΞΉ L     = pr₁ (prβ‚‚ (prβ‚‚ ΞΉ))
𝕄-induction-r P a b f g ΞΉ R     = prβ‚‚ (prβ‚‚ (prβ‚‚ ΞΉ))
𝕄-induction-r P a b f g ΞΉ (Ξ· x) = refl

\end{code}

\begin{code}

left-lc : (x y : 𝔹) β†’ left x ＝ left y β†’ x ＝ y
left-lc x x refl = refl

right-lc : (x y : 𝔹) β†’ right x ＝ right y β†’ x ＝ y
right-lc x x refl = refl

𝔹-is-discrete : (x y : 𝔹) β†’ (x ＝ y) + (x β‰  y)
𝔹-is-discrete center   center     = inl refl
𝔹-is-discrete center   (left y)   = inr (Ξ» ())
𝔹-is-discrete center   (right y)  = inr (Ξ» ())
𝔹-is-discrete (left x) center     = inr (Ξ» ())
𝔹-is-discrete (left x) (left y)   = Cases (𝔹-is-discrete x y)
                                  (Ξ» (p : x ＝ y) β†’ inl (ap left p))
                                  (Ξ» (Ξ½ : x β‰  y) β†’ inr (contrapositive (left-lc x y) Ξ½))
𝔹-is-discrete (left x)  (right y) = inr (Ξ» ())
𝔹-is-discrete (right x) center    = inr (Ξ» ())
𝔹-is-discrete (right x) (left y)  = inr (Ξ» ())
𝔹-is-discrete (right x) (right y) = Cases (𝔹-is-discrete x y)
                                  (Ξ» (p : x ＝ y) β†’ inl (ap right p))
                                  (Ξ» (Ξ½ : x β‰  y) β†’ inr (contrapositive (right-lc x y) Ξ½))

Ξ·-lc : (x y : 𝔹) β†’ Ξ· x ＝ Ξ· y β†’ x ＝ y
Ξ·-lc x x refl = refl

𝕄-is-discrete : (x y : 𝕄) β†’ (x ＝ y) + (x β‰  y)
𝕄-is-discrete L     L     = inl refl
𝕄-is-discrete L     R     = inr (Ξ» ())
𝕄-is-discrete L     (Ξ· x) = inr (Ξ» ())
𝕄-is-discrete R     L     = inr (Ξ» ())
𝕄-is-discrete R     R     = inl refl
𝕄-is-discrete R     (Ξ· x) = inr (Ξ» ())
𝕄-is-discrete (Ξ· x) L     = inr (Ξ» ())
𝕄-is-discrete (Ξ· x) R     = inr (Ξ» ())
𝕄-is-discrete (Ξ· x) (Ξ· y) = Cases (𝔹-is-discrete x y)
                              (Ξ» (p : x ＝ y) β†’ inl (ap Ξ· p))
                              (Ξ» (Ξ½ : x β‰  y) β†’ inr (contrapositive (Ξ·-lc x y) Ξ½))

𝕄-is-set : is-set 𝕄
𝕄-is-set = discrete-types-are-sets 𝕄-is-discrete

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 𝓀₀
π“œ = (𝕄 , (L , R , l , r) , (𝕄-is-set , 𝕄-eq-l , 𝕄-eq-lr , 𝕄-eq-r))

open import UF.SIP
open sip

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}

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 𝓐 L ＝ a
  i = refl

  ii : π“œ-rec 𝓐 R ＝ b
  ii = refl

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

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

\end{code}

Some boiler plate code to name the projections follows:

\begin{code}

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


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


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


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

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


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


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


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


is-hom-r : (𝓐 : BS 𝓀) (𝓑 : BS π“₯) (h : ⟨ 𝓐 ⟩ β†’ ⟨ 𝓑 ⟩)
             β†’ is-hom 𝓐 𝓑 h β†’ h ∘ ⟨ 𝓐 ⟩-r ∼ ⟨ 𝓑 ⟩-r ∘ 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) ,
                                  eql , eqlr , eqr)
 where
  Ξ± = h L      ＝⟨ is-hom-L π“œ 𝓐 h u ⟩
      ⟨ 𝓐 ⟩-L  ＝⟨ (is-hom-L π“œ 𝓐 k v)⁻¹ ⟩
      k L ∎

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

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

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

  eql : Ξ± ＝ Ο• L Ξ±
  eql = ⟨ 𝓐 ⟩-is-set Ξ± (Ο• L Ξ±)

  eqlr : Ο• R Ξ² ＝ Ξ³ L Ξ±
  eqlr = ⟨ 𝓐 ⟩-is-set (Ο• R Ξ²) (Ξ³ L Ξ±)

  eqr : β ＝ γ R β
  eqr = ⟨ 𝓐 ⟩-is-set Ξ² (Ξ³ R Ξ²)


π“œ-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 L ＝ a)
       Γ— (h R ＝ b)
       Γ— ((x : 𝕄) β†’ h (l x) ＝ f x (h x))
       Γ— ((x : 𝕄) β†’ h (r 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 ΞΉ =
   refl ,
   refl ,
   𝕄-induction-l (Ξ» _ β†’ A) a b f g ΞΉ ,
   𝕄-induction-r (Ξ» _ β†’ 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-𝕄 = L

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

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

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

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

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

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

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

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

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

  δ : 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 (l x) ＝ f x (h x))
                  Γ— ((x : 𝕄) β†’ h (r 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 L a' β†’ a' ＝ a)
                               Γ— (βˆ€ b' β†’ b' ＝ g R 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 L       ＝⟨ refl ⟩
        h (l L)   ＝⟨ hl L ⟩
        f L (h L) ∎

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

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


𝕄-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 L     = a
      h R     = b
      h (l x) = f x
      h (r x) = g x

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

  (1) a ＝ f L,
  (2) f R ＝ g L,
  (3) b ＝ g R.

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

      h L     = f L,
      h R     = g R,
      h (l x) = f x,
      h (r x) = g x.

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

     h L = h (l L) = f L,
     h R = h (r R) = g r.

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

      h (l x) = f x,
      h (r 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 = l and g = r. 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 R ＝ g L)

𝕄-caseable-gives-pinductive : (A : 𝓀 Μ‡ )
   (f g : 𝕄 β†’ A)
  β†’ 𝕄-caseable A f g
  β†’ 𝕄-pinductive (f L) (g R) (Ξ» 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 L) (g R) (Ξ» x _ β†’ f x) (Ξ» x _ β†’ g x) (𝕄-caseable-gives-pinductive _ f g ΞΉ)

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

𝕄-cases-redundant-equations : {A : 𝓀 Μ‡ }
    (f g : 𝕄 β†’ A)
  β†’ (p : 𝕄-caseable A f g)
  β†’ (𝕄-cases f g p L   ＝ f L)
  Γ— (𝕄-cases f g p R   ＝ g R)
  Γ— (𝕄-cases f g p ∘ l ∼ f)
  Γ— (𝕄-cases f g p ∘ r ∼ g)

𝕄-cases-redundant-equations f g ΞΉ = 𝕄-primrec-primitive-recursive
                                      (f L) (g R)
                                      (Ξ» 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 L) (g R)
                           (Ξ» 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 L) (g R)
                              (Ξ» x _ β†’ f x) (Ξ» x _ β†’ g x)
                              (𝕄-caseable-gives-pinductive _ f g ΞΉ)
                              (u , v)
  where
   u : βˆ€ a' β†’ a' ＝ f L β†’ a' ＝ f L
   u a' p = p

   v : βˆ€ b' β†’ b' ＝ g R β†’ b' ＝ g R
   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 L ＝ f L

𝕄-cases-L f g p = refl

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

𝕄-cases-R f g p = refl

𝕄-cases-l : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) (p : 𝕄-caseable A f g)
          β†’ 𝕄-cases f g p ∘ l ∼ f

𝕄-cases-l f g p = pr₁ (𝕄-cases-equations f g p)

𝕄-cases-r : {A : 𝓀 Μ‡ } (f g : 𝕄 β†’ A) (p : 𝕄-caseable A f g)
          β†’ 𝕄-cases f g p ∘ r ∼ g

𝕄-cases-r f g p = prβ‚‚ (𝕄-cases-equations f g p)

\end{code}

We now specialize to A = 𝕄 for notational convenience:

\begin{code}

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

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

\end{code}

Here are some examples:

\begin{code}

middle : 𝕄 β†’ 𝕄
middle = 𝕄𝕄-cases (l ∘ r) (r ∘ l) refl

middle-L : middle L ＝ l C
middle-L = refl

middle-R : middle R ＝ r C
middle-R = refl

middle-l : (x : 𝕄) β†’ middle (l x) ＝ l (r x)
middle-l = 𝕄-cases-l _ _ (𝕄-is-set , refl)

middle-r : (x : 𝕄) β†’ middle (r x) ＝ r (l x)
middle-r = 𝕄-cases-r _ _ (𝕄-is-set , refl)

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

r-by-cases : r ∼ 𝕄𝕄-cases (middle ∘ r) (r ∘ r) refl
r-by-cases = 𝕄-cases-uniqueness _ _
              (𝕄-is-set , refl) r ((Ξ» x β†’ (middle-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 (l ∘ f) (middle ∘ f)

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

𝓛 : (f : 𝕄 β†’ 𝕄) β†’ is-𝓛-function f β†’ (𝕄 β†’ 𝕄)
𝓛 f = 𝕄𝕄-cases (l ∘ f) (middle ∘ f)

𝓑 : (f : 𝕄 β†’ 𝕄) β†’ is-𝓑-function f β†’ (𝕄 β†’ 𝕄)
𝓑 f = 𝕄𝕄-cases (middle ∘ f) (r ∘ f)

preservation-𝓛𝓛 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓛-function (𝓛 f 𝓡)
preservation-𝓛𝓛 f 𝓡 𝓻 =
  l (𝓛 f 𝓡 R)      ＝⟨ refl ⟩
  l (middle (f R))  ＝⟨ ap l 𝓻 ⟩
  l (r (f L))       ＝⟨ (middle-l (f L))⁻¹ ⟩
  middle (l (f L))  ＝⟨ refl ⟩
  middle (𝓛 f 𝓡 L) ∎

preservation-𝓛𝓑 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓑-function (𝓛 f 𝓡)
preservation-𝓛𝓑 f 𝓡 𝓻 =
  middle (𝓛 f 𝓡 R)     ＝⟨ refl ⟩
  middle (middle (f R)) ＝⟨ ap middle 𝓻 ⟩
  middle (r (f L))      ＝⟨ middle-r (f L) ⟩
  r (l (f L))           ＝⟨ refl ⟩
  r (𝓛 f 𝓡 L)          ∎

preservation-𝓑𝓛 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓛-function (𝓑 f 𝓻)
preservation-𝓑𝓛 f 𝓡 𝓻 =
  l (𝓑 f 𝓻 R)          ＝⟨ refl ⟩
  l (r (f R))           ＝⟨ (middle-l (f R))⁻¹ ⟩
  middle (l (f R))      ＝⟨ ap middle 𝓡 ⟩
  middle (middle (f L)) ＝⟨ refl ⟩
  middle (𝓑 f 𝓻 L)     ∎

preservation-𝓑𝓑 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f) β†’ is-𝓑-function (𝓑 f 𝓻)
preservation-𝓑𝓑 f 𝓡 𝓻 =
  middle (𝓑 f 𝓻 R)  ＝⟨ refl ⟩
  middle (r (f R))  ＝⟨ 𝕄-cases-r (l ∘ r) (r ∘ l) (𝕄-is-set , refl) (f R) ⟩
  r (l (f R))       ＝⟨ ap r 𝓡 ⟩
  r (middle (f L))  ＝⟨ refl ⟩
  r (𝓑 f 𝓻 L)      ∎

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
 𝐿𝑒𝑓𝑑  = l , refl , refl
 π‘…π‘–π‘”β„Žπ‘‘ = r , refl , refl

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

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


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

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

   iii : 𝕄𝕄-cases (l ∘ r)      (middle ∘ r) refl
       ∼ 𝕄𝕄-cases (middle ∘ l) (r ∘ l)      refl
   iii = 𝕄-cases-uniqueness _ _ (𝕄-is-set , refl) (𝕄𝕄-cases _ _ refl) (i , ii)

   iv : 𝓛 r refl ∼ 𝓑 l refl
   iv = iii

   v : 𝓛 r refl ＝ 𝓑 l refl
   v = dfunext fe iv


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

   Ξ³ : r ＝ 𝓑 r 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 : 𝕄)
            β†’ (l (x βŠ• R) ＝ middle (x βŠ• L))
            Γ— (middle (x βŠ• R) ＝ r  (x βŠ• L))
 βŠ•-property x = prβ‚‚ (mid x)

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

 mid-is-hom-L : mid L ＝ 𝐿𝑒𝑓𝑑
 mid-is-hom-L = refl

 mid-is-hom-L' : (y : 𝕄) β†’ L βŠ• y ＝ l y
 mid-is-hom-L' y = refl

 mid-is-hom-R : mid R ＝ π‘…π‘–π‘”β„Žπ‘‘
 mid-is-hom-R = refl

 mid-is-hom-R' : (y : 𝕄) β†’ R βŠ• y ＝ r y
 mid-is-hom-R' y = refl

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

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

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

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

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

   u = Ξ± L
   v = Ξ± R
   w = Ξ± (l y) βˆ™ 𝕄-cases-l (middle ∘ (x βŠ•_)) (r ∘ (x βŠ•_)) (𝕄-is-set , prβ‚‚ (βŠ•-property x)) y
   t = Ξ± (r y) βˆ™ 𝕄-cases-r (middle ∘ (x βŠ•_)) (r ∘ (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:

     (  l (x βŠ• R) ＝ middle (x βŠ• L)    )
   Γ— (  middle (x βŠ• R) ＝ r  (x βŠ• L)   )

   Γ— (  L   βŠ• y   ＝ l y               )
   Γ— (  R   βŠ• y   ＝ r y               )
   Γ— (  l x βŠ• L   ＝ l (x βŠ• L)         )
   Γ— (  l x βŠ• R   ＝ middle (x βŠ• R)    )
   Γ— (  l x βŠ• l y ＝ l (x βŠ• y)         )
   Γ— (  l x βŠ• r y ＝ middle (x βŠ• y)    )
   Γ— (  r x βŠ• R   ＝ r (x βŠ• R)         )
   Γ— (  r x βŠ• L   ＝ middle (x βŠ• L)    )
   Γ— (  r x βŠ• l y ＝ middle (x βŠ• y)    )
   Γ— (  r x βŠ• r y ＝ r (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 L and R, 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 = l x,
   R βŠ• x = r x.

To be continued.