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!

-
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 '10 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! –  user6082 May 26 '10 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 '10 at 11:27
I was thinking about this, but that's a different category, isn't it? –  user6082 May 26 '10 at 11:32
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 '10 at 11:33
show 1 more comment

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. –  user6082 May 26 '10 at 12:56
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!