Timeline for Are infinitary monads monadic?
Current License: CC BY-SA 4.0
35 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 29, 2022 at 15:44 | vote | accept | Ilk | ||
| Jun 12, 2022 at 18:48 | answer | added | Simon Henry | timeline score: 6 | |
| Jun 12, 2022 at 12:21 | comment | added | Ilk | ok i guess i know what you are arguing against is calling that functor a left adjoint to Mnd(C) -> Endo(C), will it better to call it the left adjoint to Mnd(C) -> [ob(C),C]? Maybe i have rephrased the type theoretic property badly into categories. That does not prevent the isomorphism of categories of algebras. Note the paper proves monadicity of that forgetful functor too in the finitary case. | |
| Jun 12, 2022 at 11:31 | comment | added | Zhen Lin | Indeed, this extension construction – at least the one I have in my mind – will have the property that the category of algebras for the original endofunctor embeds in the category of algebras for the extended endofunctor and hence also in the category of algebras for the free monad, because the monad will be algebraically free. But the embedding is not essentially surjective, and it proves nothing about the monadicity of the original category of algebras – how could it, when there are endofunctors that have no free monad? | |
| Jun 12, 2022 at 10:21 | comment | added | Ilk | Its f-algebras are isomorphic to f-algebras of the original endofunctor. I am not claiming that Lan f is isomorphic to the f itself or the standard free monad of that endofunctor exists. I believe proving something about f-algebras of the original endofunctor, is proving something about f, and that it does not allow me to prove arbitrary nonsense about f. I can produce properties of interest, that can not be faked by taking a left kan extension, which talk about the "freer" monad, not only its monad algebras. In my application only the monad algebras really matter. | |
| Jun 12, 2022 at 6:13 | comment | added | Ivan Di Liberti | Related: mathoverflow.net/questions/365947/… | |
| Jun 12, 2022 at 5:33 | comment | added | Zhen Lin | The phrase garbage in garbage out comes to mind. I do not doubt you have a formal proof of something. What I doubt is that you have formalised your claim correctly. From my perspective what you have done is basically a con job: you claim that any endofunctor has a free monad, then you mutter under your breath that what you really mean is that you go up to a larger universe, extend your endofunctor, then get the free monad. I can believe that is doable – I can sketch a proof to my own satisfaction. But it proves nothing about the original endofunctor. | |
| Jun 11, 2022 at 20:16 | comment | added | Ilk | I have proof that it does what i expect, so i would really like to stop discussing this part of assumptions and you can double check universes in the adjoint folds and unfolds, if you can point to an error in there, you are welcome, given i formalized this in agda, the error would have to lie in the application of yoneda lemma there or will be a bug in agda. Unless you can produce a proper proof or a reference rather than just random claims, i do not want to discuss this further. Note that I dont care if it's the already defined one I care that the algebra isomorphism holds. | |
| Jun 11, 2022 at 13:56 | comment | added | Zhen Lin | That's not what I'm referring to. But frankly I cannot make heads or tails of your formulae so I cannot figure out if there is real mathematical argument there or not. What I know for sure is this: you can take Kan extensions of endofunctors from one universe to larger one if you like, but it may not be what you expect. For instance, if you do this procedure with the powerset endofunctor – or $[[-, 2], 2]$ if impredicative $\textrm{Prop}$ makes you unhappy – which is already defined on all universes, you will find that the extension to the larger universe is not the already-defined one. | |
| Jun 11, 2022 at 11:07 | comment | added | Ilk | You actually will not, there is slight issue if you think isomorphic things always have to live in the same universe. But 2 things in distinct universes can still be isomorphic. | |
| Jun 11, 2022 at 6:15 | comment | added | Zhen Lin | It’s not necessary, of course. But it’s the only way we know how to construct free algebras for endofunctors in general. Anyway I don’t really buy your claim that the problem can be solved by introducing universes. I think you will have problems with endofunctors that are polymorphic over universes. | |
| Jun 11, 2022 at 3:37 | history | edited | Ilk |
add type-theory tags
|
|
| Jun 11, 2022 at 3:31 | history | edited | Ilk | CC BY-SA 4.0 |
typo
|
| Jun 11, 2022 at 3:07 | comment | added | Ilk | @ZhenLin yes, i guess i also need to specify that i am being a predicativist here eventually working in some form of predicative HoTT. and again is the accessibility actually necessary and what's the source for that proof? | |
| Jun 11, 2022 at 2:55 | comment | added | Zhen Lin | Not every endofunctor or monad is accessible. The power set endofunctor, for instance. | |
| Jun 11, 2022 at 2:52 | history | edited | Ilk | CC BY-SA 4.0 |
clean up universes
|
| Jun 11, 2022 at 2:09 | history | edited | Ilk | CC BY-SA 4.0 |
awkward sentence
|
| Jun 11, 2022 at 1:50 | history | edited | Ilk | CC BY-SA 4.0 |
added 6 characters in body
|
| Jun 11, 2022 at 1:44 | history | edited | Ilk | CC BY-SA 4.0 |
added 76 characters in body
|
| Jun 11, 2022 at 1:38 | comment | added | Ilk | @SimonHenry hopefully the edit clarifies reasons for existence of a monad which can be thought of as free even though it is not the standard one. | |
| Jun 11, 2022 at 1:36 | history | edited | Ilk | CC BY-SA 4.0 |
clarify a construction
|
| Jun 11, 2022 at 1:27 | history | edited | Ilk | CC BY-SA 4.0 |
added 308 characters in body
|
| Jun 11, 2022 at 0:02 | comment | added | Ilk | Let us continue this discussion in chat. | |
| Jun 11, 2022 at 0:01 | comment | added | Simon Henry | That's not what I meant by algebraic. But i shouldn't have brought this up. let's focus on the existence of free monad. I'm not sure you can solve the problem by invoking universes. In ZFC the power set endofunctor on sets never has a free monad, even if you assume many large cardinals... | |
| Jun 10, 2022 at 23:45 | comment | added | Ilk | @SimonHenry Ok I think we might not be on the same page, I am interested in the forgetful functor being "algebraic" not its left adjoint. Free monads existing with respect to the forgetful functor is something I have a proof of in my setting already. What I am actually interested in is the forgetful functor being monadic. | |
| Jun 10, 2022 at 23:20 | comment | added | Simon Henry | Those conditions are there to ensure the free monads exists and are "algebraic". | |
| Jun 10, 2022 at 23:10 | comment | added | Ilk | @SimonHenry is it that the "easy" case should be with accesssible monad on a locally presentable category? or is there some pathology that the accessibility is preventing? In the type theoretic setting I am ok with local presentability (as the type theory i have in mind really is HoTT + any amount of axioms and/or coherences that allow the monadicity to go through, as long as consistent). I am not sure whether accessibility of an arbitrary monad is reasonable I will have to give that a thought. | |
| Jun 10, 2022 at 22:37 | history | edited | Ilk | CC BY-SA 4.0 |
grammar
|
| Jun 10, 2022 at 22:34 | comment | added | Simon Henry | If you restrict to accessible monad and endofunctors on a locally presentable category, the answer should be yes, but I don't know if there is a proof available in the litterature. | |
| Jun 10, 2022 at 22:30 | comment | added | Ilk | @ZhenLin This is not quaranteed to exist, but it does exist under certain conditions. Normally I operate in an internal language. There the requirements are universes with existentials and internal yoneda. I will update the question to reflect these requirements. | |
| Jun 10, 2022 at 22:21 | comment | added | Zhen Lin | First you would have to produce a free monad from any endofunctor. This is not guaranteed to exist. | |
| Jun 10, 2022 at 21:31 | history | edited | Ilk | CC BY-SA 4.0 |
point out finitarity restrictions
|
| Jun 10, 2022 at 21:17 | history | undeleted | Ilk | ||
| Jun 10, 2022 at 21:17 | history | deleted | Ilk | via Vote | |
| Jun 10, 2022 at 20:40 | history | asked | Ilk | CC BY-SA 4.0 |