Unless I'm mistaken the "Free completion under finite limits monad" $C \mapsto C^{lex}$ and the "free co-completion monad" $C \mapsto \widehat{C}$ (the categories of small presheaves) satisfies a distributivity law, and the algebra for the composed monad $C \mapsto \widehat{C^{lex}}$ are the infinitary pretopos.


Has this been written out somewhere ? I have a vague memories of seeing something like that some time ago (or maybe it was for completion under co-products and extensive categories), but I have not been able to find it anywhere...


Is there a similar statement for finitary pretoposes ?


I assume $C \mapsto \widehat{C}$ has to be replaced by completion under finite co-products and some co-equalizer, but that seems to be a little bit more tricky. I guess in technical terms what I want to know is: "is it possible to write the free pre-topos monad as the composite of a co-KZ-monad and a KZ-monad satisfying a distributivity law ?"



References requestion : Pretopos are algebras for a composed monad?
I think Mike is right: in Garner and Lack, [Lex colimits](https://arxiv.org/abs/1107.0778), Proposition 2.3 and the discussion following it show that the free cocompletion 2-monad lifts to the 2-category of finitely complete categories, which is equivalent to the existence of a distributive law between these two 2-monads. Since the 2-monad for finite limits is colax-idempotent and the 2-monad for small colimits is lax-idempotent, one doesn't need to appeal to the theory of fully weak distributive laws between 2-monads for this -- the KZ theory will suffice.


Then Proposition 2.5 shows that the algebras for the composite 2-monad are precisely the infinitary pretoposes.


