Timeline for Kleisli Monad bijection
Current License: CC BY-SA 2.5
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 3, 2010 at 13:21 | vote | accept | user6082 | ||
| Jun 3, 2010 at 13:21 | answer | added | user6082 | timeline score: 0 | |
| May 26, 2010 at 17:30 | answer | added | David Carchedi | timeline score: 1 | |
| May 26, 2010 at 12:59 | history | edited | user6082 | CC BY-SA 2.5 |
added 214 characters in body
|
| May 26, 2010 at 12:33 | answer | added | Neel Krishnaswami | timeline score: 2 | |
| May 26, 2010 at 11:43 | comment | added | user6082 | I thought that * has to be defined on the whole class of morphisms. Even if you restricted it to Hom(A,TB), the initial problem is still there because I might define it differently on Hom(A,TC) but TB=TC. Could you give a precise mathematical definition that makes sense (forget Isabelle for the moment)? | |
| May 26, 2010 at 11:33 | comment | added | Neel Krishnaswami | 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.) | |
| May 26, 2010 at 11:32 | comment | added | user6082 | I was thinking about this, but that's a different category, isn't it? | |
| May 26, 2010 at 11:27 | comment | added | Neel Krishnaswami | You could just define the morphisms to be triples $(A, B, f : A \to TB)$. Then you would know which $B$ to choose. | |
| May 26, 2010 at 11:25 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
fixed curly braces for sets
|
| May 26, 2010 at 10:23 | history | edited | user6082 | CC BY-SA 2.5 |
added 99 characters in body
|
| May 26, 2010 at 10:13 | history | edited | user6082 | CC BY-SA 2.5 |
added 442 characters in body
|
| May 26, 2010 at 10:08 | comment | added | user6082 | 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! | |
| May 26, 2010 at 0:56 | comment | added | Mike Shulman | 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." | |
| May 25, 2010 at 21:01 | history | asked | user6082 | CC BY-SA 2.5 |