Are infinitary monads monadic?

Question

As discussed here, Are monads monadic?, in "On the monadicity of finitary monads" by Steve Lack, the following is shown, the forgetful functor from $Mnd_f(C) \rightarrow Endo_f(C)$ is monadic, note the finitarity restrictions on both domain and codomain. In the same paper, Steve Lack, also shows a generalization for operads, but those recover only cartesian monads as discussed here Monad arising from operad. Are there any results known, which generalize this to the forgetful functor $Mnd(C) \rightarrow Endo(C)$? Note the lack of finitarity restrictions.

Edit: Assume that C supports enough constructions to have internal left Kan extensions up to universes, thus guaranteeing some form of free monads. Note that for example on the universe in type theory we can take a left kan extension and then take its free monad to obtain a free monad, which exists in a higher universe. This ensures existence of arbitrary free monads at the cost of having to think about a universe.

Edit 2: To explain existence of free monad under those conditions and stop derailing the discussion away from the issue of infinitary monads, I would like to point out the construction and then write a quick argument.

data Lan {l1 l2 l3 : _} (G : Set l1 -> Set l2) (A : Set l3) : Set (lsuc l1 ⊔ l2 ⊔ l3) where
    FMap : {X : Set l1} -> G X  -> (X -> A) -> Lan G A

data Freer {l1 l2 l3 : _} (F : Set l1 -> Set l2) (A : Set l3) : Set (lsuc l1 ⊔ l2 ⊔ l3) where
    Pure : A -> Freer F A
    Impure : Lan F (Freer F A) → Freer F A

Here Lan means left kan extension of F along identity. Note that this always exists even when the naive free monad of F does not.

Further more by algebraic-freeness of existing free monads in type theory we obtain $Talg (Freer \: F) \cong Falg (Lan \: F)$. Further by dualizing a result of Hinze we can obtain $Falg (Lan \: F) \cong Falg \: F$, for all $F$. We can actually obtain this result even when $F$ is not a strong endofunctor. (see page 2133 (26 of 52) in Adjoint folds and unfolds—An extended study)

Edit 3: for proofs feel free to assume any background that would be compatible with predicative HoTT or MLTT/MLTT+K and would make this property hold if it's known to turn out consistent.

Answer 1

These question of existence of free monad are not "derailling" the discusion. They are the whole point of the discusion. Let me clarify :

If I'm not mistaken, we have the following:

Theorem: Let $V$ be a monoidal category. Let $A$ be the category of monoids in $V$, then the forgetfull functor $U: A \to V$ is monadic if and only if it admits a left adjoint.

Sketch of the Proof: Just check the other two conditions of Beck criterion. The forgetfull functor is conservative. So we need to check that it create U-split coequalizer. Given a U-split coequalizer diagram $ X \rightrightarrows Y$ in $A$, and let $Z$ be its colimit in $V$ ( which exists by assumption). Then $Z$ comes with a monoid structure because the colimit defining it is split, so preserved by any functor, in particular the tensor product, so that $Z \otimes Z $ is the coequalizer of $X \otimes X$ and $ Y \otimes Y$ which you can use to construct an operaion $ Z \otimes Z \to Z$ making the relevant maps morphism of monoids.

With a little bit of additional work, you can conclude that this makes $Z$ a colimit in the category of monoids. $\square$

It follows that :

Corollary: Given $C$ any category, and $S \subset End(C)$ a full subcategory of endofunctors such that, $S$ contains the identity, is closed under composition, and every element of $S$ generates a free monads which is also in $S$, then the category of monads that are in $S$ is monadic over $S$.

Proof: Apply the previous result to the monoidal category $S$ (for the composition of endofunctors). $\square$

So the all point of the question is to find nice class of endofunctor for which free monads construction are available. For example :

Proposition : If $C$ is a locally presentable then the category of accessible monads on $C$ is monadic over the category of accessible endofunctor on $C$.

Though I have to insist that I do not know any exemple of category for which free monad construction on $C$ exists unconditionally. In fact, I'm relatively convinced this is impossible. To give an example :

Proposition: It is inconsistent with ZF (even with IZF) that every endofunctor of the category of sets admit a free monads.

proof: Consider the power-set endofunctor $X \mapsto \mathcal{P}(X)$, if the free monad on $\mathcal{P}$ existed, then as endomorphism monad exists in Set, the category of algebras for this monad would be the algebras for the endofunctor $\mathcal{P}$. In partiular the category of $\mathcal{P}-algebra$ would have an initial object, but by a well known theorem of Lambek, an initial algebra for an endofunctor $\mathcal{P}$ is always such that $\mathcal{P}(X) \simeq X$, but this is impossible by the diagonal argument. $\square$

So, unless the type theory you are using is inconsistent with ZFC, or you are using a notion of "endofunctor of sets" that does not corresponds to the usual notion, you won't be able to show that any endofunctor of the category of sets admit a free monad.

I don't quite understand what you are trying to explain with universes, but I think the problem you'll run into is that if you start form an endomorphism of the category of U-sets, then you might be able to construct something that look like a free monad on the category of V-sets for V a larger universe, but that's no longer a monad on U-set, so the forgetfull functor don't take you back to an endofunctor on U-set, but on V-set, but if you start with an endofunctor on $V$-set, then you need to go to an even larger universe W to get your free monad, but for endofunctors on W you'll need to get to a larger one and so one... And if your theory is consistent with ZFC, you can never find this way a setting where both the free monad and the forgetfull functor are simultenously defined, so that you can have a well defined "free monad monad" that acts on a category.

What will work (and maybe this is essentially what you are doing) is that if $\kappa$ is an innaccesible cardinal ( any regular cardinal actually), then any endofunctor of the category of $\kappa$-small sets can be extended into a $\kappa$-accessible endofunctor of the category of all sets, and then amongst $\kappa$-accessible endofunctors free monad constructions are available, and you can get a monadicity result by working with $\kappa$-accessible endofunctor.