Why my μ can not be composed in the T-program (Kleisili) category when define Lawvere theory?

Question

Recently I am learning Lawvere Theories.

I watched a video of Dr. Emily Riehl on youtube (https://youtu.be/6t6bsWVOIzs).

She said that "If we cut down the T-program between finite sets and formally turn around arrows, that is a Lawvere theory".

It's great, so I do some experiments about this.

1. I want to use a lawvere theory to describe Mon.
2. I choice the Kleisili category for the List monad.
3. I choice 3 morphisms named $μ_k$, $1+μ_k$, $μ_k+1$ in this category to verify following diagram commute.

μ_k : {x1} -> {x1,x2}
μ   : {x1} -> List {x1,x2}
μ   = λx.[x1,x2]

1+μ_k : {x1,x2} -> {x1,x2,x3} 
1+μ   : {x1,x2} -> List {x1,x2,x3}
1+μ   = (λx.[x1], λx.[x2,x3])

μ_k+1 : {x1,x2} -> {x1,x2,x3}
μ+1   : {x1,x2} -> List {x1,x2,x3}
μ+1   = (λx.[x1,x2], λx.[x3])

Note that $μ_k$, $1+μ_k$, $μ_k+1$ are morphisms in KLeisili category and I use dot line to describe them. μ, 1+μ, μ+1 are corresponding morphisms in the underlying category Set. The implement of 1+μ and μ+1 are pair of functions which means that when case analyze x1, apply first component, when case analyze x2, apply second component.

If we compose the morphisms above (e.g. use bind operator if you know Haskell), the diagram must be commute.

My question is:

Why μ can not be inserted into the implement of 1+μ and μ+1?

If you look into 1+μ, the name of it seems like "id+μ" or "(id, μ)" , why we can't use μ and id to replace the implementation of 1+μ?

For example:

1+μ = (id, μ) -- where id = λx.[x]

This seems to be a more natural to impelement 1+μ, but we can not do that, because λx.[x2,x3] ≠ λx.[x1,x2]

Unless we define μ like this

μ = λx. case x1 [x1,x2]
        case x2 [x2,x3]
        case x3 [x3,x4]
        ....

But since μ : {x1} -> List {x1,x2}, we can't do that...

This is very weird, because if we turn around the arrows, in the oppsite category, all $μ^{op}_k$ are the same arrow.

Very thanks.

Answer 1

It does not make sense to insert $\mu$ inside the implementation of $1+\mu$ or of $\mu+1$, because it does not type check, but the implementations of the different functions that you have provided is however correct. There is one very important thing that you should understand, in category theory one usually does not distinguish between isomorphic objects - that is people will tend to write that $\left\{x_1,x_2\right\} = \left\{x_2,x_3\right\}$, even though strictly speaking from a set-theoretic point of view, these sets are different. This is what Riehl does in the conference you shared, when she defines $\underline{n}$ as "the" set with $n$ elements, when there are really many sets with $n$ elements.

Now you have to realise that when you write $$ 1+\mu : \left\{x_1,x_2\right\} \to list(\left\{ x_1,x_2,x_3 \right\})$$ You are implicitly taking a way to decompose the set on the left into a disjoint union. More explicitly you are assuming that you are writing $$\left\{ x_1,x_2\right\} = \left\{ x_1 \right\} + \left\{ x_1 \right\}$$ and then you are considering that the part $1$ acts on the right side, and the part $\mu$ acts on the left side. Since $1$ (the unit of the monad) sends $\{ x_1\}$ on $list(\{ x_1 \})$, and there is a function $\{ x_1\} \to \{ x_1,x_2,x_3\}$ (sending $x_1$ onto $x_1$), you can see $1$ as a function $\{ x_1\} \to list(\{ x_1,x_2,x_3\})$. Similarly, $\mu$ sends $\{ x_1\}$ on $list(\{ x_1,x_2\})$ and there is a function $\{ x_1,x_2\} \to \{ x_1,_x2,x_3\}$ (sending $x_1$ to $x_2$ and $x_2$ to $x_3$), so you can see $\mu$ as a function $\{ x_1,x_2\}\to list(\{ x_1,x_2,x_3\})$ what you have really defined is a function $$ \{ x_1\} + \{ x_1\} \to list(\{x_1,x_2,x_3\}) $$ by unversal property of the disjoint union.

So you see what is really going on when you write $1+\mu$, is that there are lots of ways to keep track of the elements that are implied by the notation, and that are swept under the rug.

Now, when you are working in a programming language, you are more in a set-theoretic setting, meaning that you actually distinguish between the names. So you have two ways to work around this : one very impractical - define the disjoint union operation of the types, and use $\mu$ explicitly. But then you will land inside $list(\{x1\} + \{x_1+x_2\})$ on one side, and in $list(\{ x_1,x_2\} + \{ x_1 \})$ on the other side. You have to encode explitly a function from one to the other. The other solution is much better, it is what you have done : define manually the functions so that it all makes sense properly. Here is how I would write it (in a syntax vaguely inspired from programming languages)

Type T1 :
  x0 : T1
Type T2 :
  x0 x1 : T2
Type T3 : 
  x0 x1 x2 : T3
Type list (T : Type) : 
  [] : list T
  _::_ : T -> list T -> list T

mu : T1 -> list T2
mu (x0) = [x0::x1]

1+mu : T2 -> list T3
1+mu (x0) = [x0]
1+mu (x1) = [x1::x2]

mu+1 : T2 -> list T3
mu+1 (x0) = [x0::x1]
mu+1 (x1) = x2

This is basically what you defined, with a distinction : I named the types. As you can see, mu lands in list T2 and 1+mu lands in list T3. This shows why you cannot use mu in the body of the definition of 1+mu, unless you provide some specific function i1 : T2 -> T3. Be careful though as you would also need to provide a function i2 : T2 -> T3 in order to use mu in the body of the definition of mu+1, and the two functions i1 and i2 are different !