Timeline for Are infinitary monads monadic?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 29, 2022 at 15:44 | vote | accept | Ilk | ||
| Jun 12, 2022 at 19:41 | comment | added | Simon Henry | If you can use this to give an example of a non-trivial category $C$ such that every endofunctor on $C$ admit a free monad, i'd be interested to see it. | |
| Jun 12, 2022 at 19:31 | comment | added | Ilk | i know that the parametricity assumption contradict certain other impredicative assumptions, i will have to think how to port those to my setting to show this counterexample cannot actually go through. but this also explains why i couldnt find a generalization in the literature. | |
| Jun 12, 2022 at 19:30 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 16 characters in body
|
| Jun 12, 2022 at 19:29 | comment | added | Simon Henry | I know. But you are still missing the point I'm making : rejecting the existence of power set isn't enough to avoid the argument - you would have to work in a system that is inconsistent with the existence of power set. | |
| Jun 12, 2022 at 19:26 | comment | added | Ilk | note izf has powerset and i am working predicatively, so i think the distinction lies in predicativity of the setting | |
| Jun 12, 2022 at 19:24 | comment | added | Simon Henry | Though I should say being inconsistant with excluded middle wouldn't even be enough, the argument I gave doesn't use excluded middle, so it is already inconsitant with IZF. You basically have to be inconsistent with the existence of power set. I don't know any foundation that does this. | |
| Jun 12, 2022 at 19:21 | comment | added | Simon Henry | I don't know what this is. In any case, if you are indeed convince you have free monad, then I have answered your question. I just have no idea what category you are talking about - I don't know any category where every endofunctor admits a free monad - but maybe they exists | |
| Jun 12, 2022 at 19:19 | comment | added | Ilk | I think that's the internal yoneda lemma that comes from parametricity as parametricity contradicts excluded middle. | |
| Jun 12, 2022 at 19:17 | comment | added | Simon Henry | Predicative doesn't mean inconsitent with ZFC. It means you are rejecting some axiom of ZFC. As long as ZFC (or a stronger theory, like ZFC + some large cardinals) proves the category of sets is a model of your theory, you can't prove theorem inconsistant with ZFC. So unless you include axioms that are inconsitent with ZFC, you won't be able to prove this. | |
| Jun 12, 2022 at 19:13 | comment | added | Ilk | I mean it is inconsistent with zfc as i am working predicatively and with internal yoneda, where the only techniques i know of exclude excluded middle, so power set functor examples are quite explicitly what fails. | |
| Jun 12, 2022 at 19:00 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 9 characters in body
|
| Jun 12, 2022 at 18:48 | history | answered | Simon Henry | CC BY-SA 4.0 |