Martin Escardo, 7th August 2020.

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

Modified 2nd May 2025 to remove the requirement that the underlying
types of binary systems are sets, and also to removed some unused
hypotheses. But it is still the case that the initial binary system is
a set.

\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 : 𝕄
 Ξ· : 𝔹 β†’ 𝕄

pattern 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

\end{code}

We now show that 𝕄 is a set.

\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

\end{code}

It turns out that we don't need to know that 𝕄 is a set. But it is
interesting to know that the initial binary system is a set, even
though we don't require the underlying types of binary systems to be
sets.

We now prove a general induction principle for 𝕄 and a particular case
of interest.

\begin{code}

open import UF.Subsingletons hiding (center)

𝕄-induction : (P : 𝕄 β†’ 𝓀 Μ‡ )
            β†’ (a : P L)
            β†’ (b : P R)
            β†’ (f : (x : 𝕄) β†’ P x β†’ P (l x))
            β†’ (g : (x : 𝕄) β†’ P x β†’ P (r x))
            β†’ (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 C             = f R b -- (*)
𝕄-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}

(*) Alternatively, here we can take g L a, but then the proofs below
change.

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

\begin{code}

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

𝕄-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₁ ΞΉ
𝕄-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β‚‚ ΞΉ)
𝕄-induction-r P a b f g ΞΉ R     = prβ‚‚ (prβ‚‚ ΞΉ)
𝕄-induction-r P a b f g ΞΉ (Ξ· x) = refl

\end{code}

We now give 𝕄 the structure of a 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) = (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) , (𝕄-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) ΞΉ

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

\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-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) Ξ± Ξ² Ο• Ξ³
 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)       ∎

π“œ-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}

TODO. Now that we have removed the sethood requirement for the
underlying type of a binary system we need to prove unique existence
as contractibility (as done for nno's in the MGS'2019 lecture notes).

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

\begin{code}

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

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

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

𝕄-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
  α = 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)   ∎

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

𝕄-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 (3) hold, we are left
with condition (2) 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 (2)
and work with the equations

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

Hence the function 𝕄-cases defined belowgives 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 following constructions and facts are all particular cases of
those for 𝕄-primrec.

\begin{code}

𝕄-caseable : (A : 𝓀 Μ‡ ) β†’ (𝕄 β†’ A) β†’ (𝕄 β†’ A) β†’ 𝓀 Μ‡
𝕄-caseable A f g = (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 p
 = 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)

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}

Here are some examples:

\begin{code}

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

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

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

m-l : (x : 𝕄) β†’ m (l x) ＝ l (r x)
m-l = 𝕄-cases-l _ _ refl

m-r : (x : 𝕄) β†’ m (r x) ＝ r (l x)
m-r = 𝕄-cases-r _ _ refl

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

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

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

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

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

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

preservation-𝓛𝓑 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f)
                β†’ is-𝓑-function (𝓛 f 𝓡)
preservation-𝓛𝓑 f 𝓡 𝓻 =
  m (𝓛 f 𝓡 R) ＝⟨ refl ⟩
  m (m (f R)) ＝⟨ ap m 𝓻 ⟩
  m (r (f L)) ＝⟨ m-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))      ＝⟨ (m-l (f R))⁻¹ ⟩
  m (l (f R))      ＝⟨ ap m 𝓡 ⟩
  m (m (f L))      ＝⟨ refl ⟩
  m (𝓑 f 𝓻 L)      ∎

preservation-𝓑𝓑 : (f : 𝕄 β†’ 𝕄) (𝓡 : is-𝓛-function f) (𝓻 : is-𝓑-function f)
                β†’ is-𝓑-function (𝓑 f 𝓻)
preservation-𝓑𝓑 f 𝓡 𝓻 =
  m (𝓑 f 𝓻 R)  ＝⟨ refl ⟩
  m (r (f R))  ＝⟨ 𝕄-cases-r (l ∘ r) (r ∘ l) refl (f R) ⟩
  r (l (f R))  ＝⟨ ap r 𝓡 ⟩
  r (m (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.

(NB. We no longer need to know that F is a set, but we keep the
original proof.)

\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) (m ∘ r) refl (l x) ＝⟨ 𝕄-cases-l _ _ refl x ⟩
    l (r x)                            ＝⟨ (m-l x)⁻¹ ⟩
    m (l x)                            ∎

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

   iii : 𝕄-cases (l ∘ r) (m ∘ r) refl
       ∼ 𝕄-cases (m ∘ l) (r ∘ l) refl
   iii = 𝕄-cases-uniqueness _ _ 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-eq-l , F-eq-lr , F-eq-r))

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

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

 βŠ•-property : (x : 𝕄)
            β†’ (l (x βŠ• R) ＝ m (x βŠ• L))
            Γ— (m (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   ＝ m (x βŠ• R))
               Γ— (l x βŠ• l y ＝ l (x βŠ• y))
               Γ— (l x βŠ• r y ＝ m (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 βŠ•_)) (m ∘ (x βŠ•_)) (pr₁ (βŠ•-property x)) y ∎

   u = Ξ± L
   v = Ξ± R
   w = Ξ± (l y) βˆ™ 𝕄-cases-l
                  (l ∘ (x βŠ•_))
                  (m ∘ (x βŠ•_))
                  (pr₁ (βŠ•-property x))
                  y
   t = Ξ± (r y) βˆ™ 𝕄-cases-r
                  (l ∘ (x βŠ•_))
                  (m ∘ (x βŠ•_))
                  (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   ＝ m (x βŠ• L))
               Γ— (r x βŠ• R   ＝ r (x βŠ• R))
               Γ— (r x βŠ• l y ＝ m (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 (m ∘ (x βŠ•_)) (r ∘ (x βŠ•_)) (prβ‚‚ (βŠ•-property x)) y ∎

   u = Ξ± L
   v = Ξ± R
   w = Ξ± (l y) βˆ™ 𝕄-cases-l
                  (m ∘ (x βŠ•_))
                  (r ∘ (x βŠ•_))
                  (prβ‚‚ (βŠ•-property x))
                  y
   t = Ξ± (r y) βˆ™ 𝕄-cases-r
                  (m ∘ (x βŠ•_))
                  (r ∘ (x βŠ•_))
                  (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) ＝ m (x βŠ• L)    )
   Γ— (  m (x βŠ• R) ＝ r (x βŠ• L)    )
   Γ— (  L   βŠ• y   ＝ l y          )
   Γ— (  R   βŠ• y   ＝ r y          )
   Γ— (  l x βŠ• L   ＝ l (x βŠ• L)    )
   Γ— (  l x βŠ• R   ＝ m (x βŠ• R)    )
   Γ— (  l x βŠ• l y ＝ l (x βŠ• y)    )
   Γ— (  l x βŠ• r y ＝ m (x βŠ• y)    )
   Γ— (  r x βŠ• R   ＝ r (x βŠ• R)    )
   Γ— (  r x βŠ• L   ＝ m (x βŠ• L)    )
   Γ— (  r x βŠ• l y ＝ m (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 case analysis.

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