## Kleisli Monad bijection

### Remember to vote up questions/answers you find interesting or helpful (requires 15 reputation points)

For a monad $(T,\mu,\eta)$ if $T(A) = T(B)$, does this imply that $\mu_A = \mu_B$? I want to know because in the bijection between Kleisli triples and monads, given a monad, we define $f^* := T(f) ; \mu_B$ if $f : A\to T(B)$ (c.f. Prop 1.6), but this needs to be well defined even when $T$ is not an embedding.

Clarification (more formal): Given a monad $(T,\mu,\eta)$, I need to define ${}^*$ on the class $\{f \;|\; \exists A,B \in |\mathbf{C}| . f : A \to T B \}$. If $T$ were an embedding then I could just take $B := T^{-1}(\mathrm{cod}(f))$. What do I do though when $T$ is not an embedding? All I know about the codomain of an element of this class is that it is in the image of $T$. There may be many $B$'s and the $\mu_B$'s may be different!

-

2
The objects of the Kleisli category are the objects of the underlying category, not T of them, so the reconstruction of the monad from the Kleisli category is always perfectly well-defined, even though the answer to your first question is probably "no." – Mike Shulman May 26 2010 at 0:56
Maybe I did not make myself clear enough. It is a subtle point (maybe trivial?), and one that I missed until I tried to formally write down a definition in Isabelle. Given a monad $(T,\mu,\eta)$, I need to define $*$ on the class $\{f|\exists A,B \in |\mathbf{C}| . f : A \to T B \}$. If $T$ were an embedding then I could just take $B := T^{-1}(\mathrm{cod}(f))$. What do I do though when $T$ is not an embedding? All I know about the codomain of an element of this class is that it is in the image of $T$. There may be many $B$'s and the $\mu_B$'s may be different! – apk May 26 2010 at 10:08
You could just define the morphisms to be triples $(A, B, f : A \to TB)$. Then you would know which $B$ to choose. – Neel Krishnaswami May 26 2010 at 11:27
I was thinking about this, but that's a different category, isn't it? – apk May 26 2010 at 11:32

1
I should add that your difficulty is partly a function of the fact that you are trying to define $*$ on the universal collection of all the morphisms, rather than by considering families of hom-sets indexed by domain and codomain. In a dependent type theory, I would usually try to define Hom to be a type operator dependent upon domain and codomain. Isabelle must have some standard techniques to work around the lack of dependency -- I would look at those. (My previous comment is one way of doing it, but if there's an idiomatic thing you should do that.) – Neel Krishnaswami May 26 2010 at 11:33
show 1 more comment

## 3 Answers

This didn't fit in the comments, so I'm posting it as an answer.

Ignoring size issues, we can define a category as a set of objects, together with a family of sets of morphisms, with one set for each domain and codomain -- ie, as a dependent record:

$$\mathrm{Cat} = \sum \mathrm{Obj}:\mathrm{Set}.\;\sum \mathrm{Mor} : \mathrm{Obj} \times \mathrm{Obj} \to \mathrm{Set}.\; \ldots \mathit{category\; axioms} \ldots$$

So if you have a category $C \equiv (\mathrm{Obj}, \mathrm{Mor}, \ldots)$ and a monad $(T, \mu, \eta)$, the Kleisli category will be of the form $(\mathrm{Obj}, (\lambda AB.\;\mathrm{Mor}(A, TB)), \ldots)$.

Then, the extension operator will be an operation whose type is $\prod A,B:O.\;\mathrm{Mor}(A, TB) \to \mathrm{Mor}(TA, TB)$, which can be defined in the obvious way, as $\lambda A\;B\;f.\;T(f);\mu_B$. Note that the objects for the domain and codomain come in as arguments, so there's no need to reconstruct them from the data of the function $f$.

(In fact, if you spell out the definition of functor for this setup, you'll see that even $T$ will be indexed, so its action on morphisms really ought to be written $T_{A,B}(f)$. I just left them out since these arguments are obvious from context.)

-

Thanks for this.  But I'm not talking about the Kleisli Category $C_T$, I am talking about the Kleisli triple over $C$ (sorry, this was my mistake; I'll edit the question).  In every place where I have seen the Kleisli triple defined from a Monad, the underlying Category is the same with no indexing of objects.  When you index the objects, surely it is a different category, however you present the theory. – apk May 26 2010 at 12:56

### You can accept an answer to one of your own questions by clicking the check mark next to it. This awards 15 reputation points to the person who answered and 2 reputation points to you.

I agree with Mike that you shouldn't NEED this, BUT the answer is yes. The monad $T$ arises as coming from the adjunction $U:C^T \to C:F$, where $C^T$ is its category of Eilenberg-Moore algebras. Since this adjunction is monadic, it reflects isos. Hence, if $TX=U(FX)$ is iso to $TY=U(FY)$, then $FX$ and $FY$ are iso. Now, consider $id_{UFX}$, then, since here is a bijection DEPENDING NATURALLY ON A=UFX and B=FX between $Hom(FA,B)$ and $Hom(A,UB)$, we have that $\epsilon_{FX}$ and $\epsilon_{FY}$ are the same (up to identification via isomorphisms), where $\epsilon$ represents the counit of the adjunction. Now, multiplication $\mu$ of the monad $T$ has $\mu_X=G(\epsilon_{FX})$. This completes the proof.

-

In fact, the Kleisli star is a partial map ${}^* : \mathrm{Mor}(\mathbf{C}) \times \mathrm{Obj}(\mathbf{C}) \times \mathrm{Obj}(\mathbf{C}) \to \mathrm{Mor}(\mathbf{C})$. So there is no problem!

-
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 54, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": false, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9546073079109192, "perplexity_flag": "head"}