Return to 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)

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.

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 l2 -> Set l3) (A : Set l1) : Set (lsuc l2 ⊔ l3 ⊔ l1) where
    FMap : {X : Set l2} -> G X  -> (X -> A) -> Lan G A

data Freer {l1 l2 l3} (F : Set l1 -> Set l2) (A : Set l3) : Set (l3 ⊔ (lsuc l1 ⊔ l2)) 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)

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)