Martin Escardo and Paulo Oliva, April 2024

The free discrete graphic monoid is given by the monoid of lists
without repetitions.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.DiscreteAndSeparated

module DiscreteGraphicMonoids.Free
        (fe : Fun-Ext)
       where

open import MLTT.List
            renaming (_∷_ to _•_ ;          -- typed as \bub
                      _++_ to _◦_ ;         -- typed as \buw
                      ++-assoc to ◦-assoc)
open import Naturals.Order
open import Notation.CanonicalMap
open import Notation.Order
open import UF.Base
open import DiscreteGraphicMonoids.Type
open import DiscreteGraphicMonoids.ListsWithoutRepetitions fe
open import DiscreteGraphicMonoids.LWRDGM fe

\end{code}

List⁻ X is the graphic monoid freely generated by X, with
η⁻ : X → List⁻ X as the universal map, or insertion of generators.

That is,

 1. List⁻ X is a graphic monoid.

 2. There is a map η⁻ : X → List⁻ X, such that for any graphic monoid
    M and any function f : X → M, there is a unique monoid
    homomorphism f' : List⁻ → M.

       η⁻
    X ---> List⁻ X
     \       .
      \      .
       \     .
     f  \    . f⁻
         \   .
          \  .
           \ .
            v
            M


The following is an auxiliary module to prove that.

\begin{code}

module free-discrete-graphic-monoid-development
        {𝓤 𝓥 : Universe}
        (M : 𝓥 ̇ )
        {{M-is-discrete' : is-discrete' M}}
        (e : M)
        (_●_ : M → M → M)
        (●-left-unit : (x : M) → e ● x ＝ x)
        (●-right-unit : (x : M) → x ● e ＝ x)
        (●-assoc : (x y z : M) → x ● (y ● z) ＝ (x ● y) ● z)
        (M-is-graphic : (x y : M) → (x ● y) ● x ＝ x ● y)
        (X : 𝓤 ̇ )
        {{X-is-discrete' : is-discrete' X}}
        (f : X → M)
       where

 M-is-discrete : is-discrete M
 M-is-discrete = discrete'-gives-discrete

 f' : List X → M
 f' []       = e
 f' (x • xs) = f x ● f' xs

\end{code}

Notice that f' preserves the unit my construction.

\begin{code}

 f'-preserves-mul : (xs ys : List X) → f' (xs ◦ ys) ＝ f' xs ● f' ys
 f'-preserves-mul [] ys =
  f' ([] ◦ ys)  ＝⟨ refl ⟩
  f' ys         ＝⟨ (●-left-unit (f' ys))⁻¹ ⟩
  e ● f' ys     ＝⟨ refl ⟩
  f' [] ● f' ys ∎
 f'-preserves-mul (x • xs) ys =
  f' (x • xs ◦ ys)      ＝⟨ refl ⟩
  f x ● f' (xs ◦ ys)    ＝⟨ ap (f x ●_) (f'-preserves-mul xs ys) ⟩
  f x ● (f' xs ● f' ys) ＝⟨ ●-assoc (f x) (f' xs) (f' ys) ⟩
  (f x ● f' xs) ● f' ys ＝⟨ refl ⟩
  f' (x • xs) ● f' ys   ∎

 f⁻ : List⁻ X → M
 f⁻ = f' ∘ underlying-list

 f⁻-triangle : f⁻ ∘ η⁻ ∼ f
 f⁻-triangle x = (f⁻ ∘ η⁻) x ＝⟨ refl ⟩
                 f x ● e     ＝⟨ ●-right-unit (f x) ⟩
                 f x         ∎

 underlying-list-preserves-unit : ι ([]⁻ {𝓤} {X}) ＝ []
 underlying-list-preserves-unit = refl

\end{code}

The function ι : List⁻ X → List X doesn't preserve multiplication, as
this would mean that ρ (xs ◦ ys) ＝ xs ◦ ys for any two lists with
ρ xs ＝ xs and ρ ys = ys. However, it's composition f⁻ with f'
does. We need to use the graphic law, as this is not true in general.

\begin{code}

 ϕ : List M → M
 ϕ []       = e
 ϕ (u • us) = u ● ϕ us

\end{code}

Notice that ϕ preserves the unit by construction. It also preserves
multiplication, but we don't use this fact, although we record it.

\begin{code}

 ϕ-preserves-mul : (us vs : List M)
                 → ϕ (us ◦ vs) ＝ ϕ us ● ϕ vs
 ϕ-preserves-mul [] vs =
  ϕ ([] ◦ vs)   ＝⟨ refl ⟩
  ϕ vs          ＝⟨ (●-left-unit (ϕ vs))⁻¹ ⟩
  (e ● ϕ vs)    ＝⟨ refl ⟩
  (ϕ [] ● ϕ vs) ∎
 ϕ-preserves-mul (x • us) vs =
  ϕ (x • us ◦ vs)   ＝⟨ refl ⟩
  x ● ϕ (us ◦ vs)   ＝⟨ ap (x ●_) (ϕ-preserves-mul us vs) ⟩
  x ● (ϕ us ● ϕ vs) ＝⟨ ●-assoc x (ϕ us) (ϕ vs) ⟩
  (x ● ϕ us) ● ϕ vs ＝⟨ refl ⟩
  ϕ (x • us) ● ϕ vs ∎

 ϕ-map-lemma : (xs : List X) → f' xs ＝ ϕ (map f xs)
 ϕ-map-lemma []       = refl
 ϕ-map-lemma (x • xs) = ap (f x ●_) (ϕ-map-lemma xs)

\end{code}

The following is the only, but crucial, place the graphic property of
M is used directly.

\begin{code}

 ϕ-δ-lemma' : (u v : M) (ws : List M)
            → u ● (v ● ϕ (δ u ws)) ＝ u ● (v ● ϕ ws)
 ϕ-δ-lemma' u v []       = refl
 ϕ-δ-lemma' u v (w • ws) = h (M-is-discrete u w)
  where
   h : is-decidable (u ＝ w)
     → u ● (v ● ϕ (δ u (w • ws))) ＝ u ● (v ● ϕ (w • ws))
   h (inl refl) =
    u ● (v ● ϕ (δ u (u • ws))) ＝⟨ ap (λ - → u ● (v ● ϕ -)) (δ-same u ws) ⟩
    u ● (v ● ϕ (δ u ws))       ＝⟨ ϕ-δ-lemma' u v ws ⟩
    u ● (v ● ϕ ws)             ＝⟨ ●-assoc u v (ϕ ws) ⟩
    (u ● v) ● ϕ ws             ＝⟨ ap (_● ϕ ws) ((M-is-graphic u v)⁻¹) ⟩
    ((u ● v) ● u) ● ϕ ws       ＝⟨ (●-assoc (u ● v) u (ϕ ws))⁻¹ ⟩
    (u ● v) ● (u ● ϕ ws)       ＝⟨ (●-assoc u v (u ● ϕ ws))⁻¹ ⟩
    u ● (v ● (u ● ϕ ws))       ＝⟨ refl ⟩
    u ● (v ● ϕ (u • ws))       ∎
   h (inr ν) =
    u ● (v ● ϕ (δ u (w • ws))) ＝⟨ ap (λ - → u ● (v ● ϕ -)) (δ-≠ u w ws ν) ⟩
    u ● (v ● ϕ (w • δ u ws))   ＝⟨ refl ⟩
    u ● (v ● (w ● ϕ (δ u ws))) ＝⟨ ap (u ●_) (●-assoc v w (ϕ (δ u ws))) ⟩
    u ● ((v ● w) ● ϕ (δ u ws)) ＝⟨ ϕ-δ-lemma' u (v ● w) ws ⟩
    u ● ((v ● w) ● ϕ ws)       ＝⟨ ap (u ●_) ((●-assoc v w (ϕ ws))⁻¹) ⟩
    u ● (v ● (w ● ϕ ws))       ＝⟨ refl ⟩
    u ● (v ● ϕ (w • ws))       ∎

\end{code}

We need the following particular case of the above lemma.

\begin{code}

 ϕ-δ-lemma : (u : M) (ws : List M)
           → u ● ϕ (δ u ws) ＝ u ● ϕ ws
 ϕ-δ-lemma u ws =
  u ● ϕ (δ u ws)       ＝⟨ ap (u ●_) ((●-left-unit (ϕ (δ u ws)))⁻¹) ⟩
  u ● (e ● ϕ (δ u ws)) ＝⟨ ϕ-δ-lemma' u e ws ⟩
  u ● (e ● ϕ ws)       ＝⟨ ap (u ●_) (●-left-unit (ϕ ws)) ⟩
  u ● ϕ ws             ∎

 ϕ-ρ-lemma : (us vs : List M)
           → ρ us ＝ ρ vs
           → ϕ us ＝ ϕ vs
 ϕ-ρ-lemma = course-of-values-induction-on-length _ h
  where
   h : (us : List M)
     → ((us' : List M)
             → length us' < length us
             → (vs : List M) → ρ us' ＝ ρ vs → ϕ us' ＝ ϕ vs)
     → (vs : List M) → ρ us ＝ ρ vs → ϕ us ＝ ϕ vs
   h [] IH [] e = refl
   h (u • us) IH (v • vs) e =
    ϕ (u • us)     ＝⟨ refl ⟩
    u ● ϕ us       ＝⟨ (ϕ-δ-lemma u us)⁻¹ ⟩
    u ● ϕ (δ u us) ＝⟨ ap (u ●_) (IH (δ u us) (δ-length u us) (δ v vs) I) ⟩
    u ● ϕ (δ v vs) ＝⟨ ap (_● ϕ (δ v vs)) (equal-heads e) ⟩
    v ● ϕ (δ v vs) ＝⟨ ϕ-δ-lemma v vs ⟩
    v ● ϕ vs       ＝⟨ refl ⟩
    ϕ (v • vs)     ∎
     where
      have-e : u • δ u (ρ us) ＝ v • δ v (ρ vs)
      have-e = e

      I =  ρ (δ u us) ＝⟨ (δ-ρ-swap u us)⁻¹ ⟩
           δ u (ρ us) ＝⟨ equal-tails e ⟩
           δ v (ρ vs) ＝⟨ δ-ρ-swap v vs ⟩
           ρ (δ v vs) ∎

 ϕ-ρ : (us : List M) → ϕ us ＝ ϕ (ρ us)
 ϕ-ρ us = ϕ-ρ-lemma us (ρ us) ((ρ-idemp us)⁻¹)

 f'-ρ-lemma : (xs : List X)
            → f' (ρ xs) ＝ f' xs
 f'-ρ-lemma xs =
  f' (ρ xs)            ＝⟨ ϕ-map-lemma (ρ xs) ⟩
  ϕ (map f (ρ xs))     ＝⟨ ϕ-ρ (map f (ρ xs)) ⟩
  ϕ (ρ (map f (ρ xs))) ＝⟨ ap (ϕ) (ρ-map f xs) ⟩
  ϕ (ρ (map f xs))     ＝⟨ (ϕ-ρ (map f xs))⁻¹ ⟩
  ϕ (map f xs)         ＝⟨ (ϕ-map-lemma xs)⁻¹ ⟩
  f' xs                ∎

 f'-ρ-lemma' : (xs ys : List X)
             → ρ xs ＝ ρ ys
             → f' xs ＝ f' ys
 f'-ρ-lemma' xs ys e =
  f' xs     ＝⟨ (f'-ρ-lemma xs)⁻¹ ⟩
  f' (ρ xs) ＝⟨ ap f' e ⟩
  f' (ρ ys) ＝⟨ f'-ρ-lemma ys ⟩
  f' ys     ∎

 f⁻-preserves-mul : (𝔁𝓼 𝔂𝓼 : List⁻ X)
                  → f⁻ (𝔁𝓼 · 𝔂𝓼) ＝ f⁻ 𝔁𝓼 ● f⁻ 𝔂𝓼
 f⁻-preserves-mul 𝔁𝓼@(xs , a) 𝔂𝓼@(ys , b) =
  f⁻ (𝔁𝓼 · 𝔂𝓼)      ＝⟨ refl ⟩
  f' (ρ (xs ◦ ys)) ＝⟨ f'-ρ-lemma (xs ◦ ys) ⟩
  f' (xs ◦ ys)     ＝⟨ f'-preserves-mul xs ys ⟩
  f' xs ● f' ys    ＝⟨ refl ⟩
  f⁻ 𝔁𝓼 ● f⁻ 𝔂𝓼      ∎

 f⁻-uniqueness : (h : List⁻ X → M)
               → h []⁻ ＝ e
               → ((xs ys : List⁻ X) → h (xs · ys) ＝ h xs ● h ys)
               → h ∘ η⁻ ∼ f
               → h ∼ f⁻
 f⁻-uniqueness h unit-h comp-h triangle-h (xs , a) = I xs a
  where
   I : (xs : List X) (a : ρ xs ＝ xs)
     → h (xs , a) ＝ f⁻ (xs , a)
   I [] a =
    h ([] , a) ＝⟨ ap h (to-List⁻-＝ refl) ⟩
    h []⁻      ＝⟨ unit-h ⟩
    e          ＝⟨ refl ⟩
    f⁻ ([] , a) ∎
   I (x • xs) a =
    h ((x • xs) , a) ＝⟨ ap h (·-lemma x xs a) ⟩
    h (η⁻ x · 𝔁𝓼)    ＝⟨ comp-h (η⁻ x) 𝔁𝓼 ⟩
    h (η⁻ x) ● h 𝔁𝓼  ＝⟨ ap₂ _●_ (triangle-h x) (I xs b) ⟩
    f x ● f⁻ 𝔁𝓼      ＝⟨ refl ⟩
    f x ● f' xs      ＝⟨ refl ⟩
    f⁻ ((x • xs) , a) ∎
     where
      b : ρ xs ＝ xs
      b = ρ-tail x xs a

      𝔁𝓼 : List⁻ X
      𝔁𝓼 = xs , b

\end{code}

We now package the above development as follows, to conclude that, as
claimed, lists without repetitions over a discrete type form the free
discrete graphic monoid.

\begin{code}

module _
        (𝓜 : DGM 𝓥)
        {X : 𝓤 ̇ }
        {{X-is-discrete' : is-discrete' X}}
       where

 open free-discrete-graphic-monoid-development
       ⟨ 𝓜 ⟩
       {{discrete-gives-discrete' (discreteness 𝓜)}}
       (unit 𝓜)
       (multiplication 𝓜)
       (left-neutrality 𝓜)
       (right-neutrality 𝓜)
       (associativity 𝓜)
       (graphicality 𝓜)
       X
       {{X-is-discrete'}}

 extension : (X → ⟨ 𝓜 ⟩) → List⁻ X → ⟨ 𝓜 ⟩
 extension = f⁻

 extension-is-hom : (f : X → ⟨ 𝓜 ⟩)
                  → is-hom (List⁻-DGM X) 𝓜 (extension f)
 extension-is-hom f = refl , f⁻-preserves-mul f

 triangle : (f : X → ⟨ 𝓜 ⟩)
          → extension f ∘ η⁻ ∼ f
 triangle = f⁻-triangle

 uniqueness : (f : X → ⟨ 𝓜 ⟩)
              (g : List⁻ X → ⟨ 𝓜 ⟩)
            → is-hom (List⁻-DGM X) 𝓜 g
            → g ∘ η⁻ ∼ f
            → extension f ∼ g
 uniqueness f g (g-unit , g-comp) h = ∼-sym (f⁻-uniqueness f g g-unit g-comp h)

\end{code}