# orderedItems[].object.content
@jonmsterling @ltchen My impression is that the more set-theoretic aspects of locally presentable categories arise, at least primarily, when one does not fix the cardinality of presentability. In contrast, much of the theory of locally \(\lambda\)-presentable categories, for a fixed \(\lambda\), can be derived 2-category theoretically without set-theoretic assumptions. In my experience, many of the applications of locally presentable categories do not require a change of cardinal (particularly in computer science). So perhaps the obstructions to constructivity are not as severe as might be feared at first. (On the other hand, the theory of accessible categories seems much more reliant on freely changing cardinality.)

# orderedItems[].object.contentMap.en
@jonmsterling @ltchen My impression is that the more set-theoretic aspects of locally presentable categories arise, at least primarily, when one does not fix the cardinality of presentability. In contrast, much of the theory of locally \(\lambda\)-presentable categories, for a fixed \(\lambda\), can be derived 2-category theoretically without set-theoretic assumptions. In my experience, many of the applications of locally presentable categories do not require a change of cardinal (particularly in computer science). So perhaps the obstructions to constructivity are not as severe as might be feared at first. (On the other hand, the theory of accessible categories seems much more reliant on freely changing cardinality.)

# orderedItems[].object.content
@ltchen Which aspects of the theory of locally presentable categories do not work well constructively?

# orderedItems[].object.contentMap.en
@ltchen Which aspects of the theory of locally presentable categories do not work well constructively?

# orderedItems[].object.content
@stringdiagram Another nice observation is that the same characterisation works for relative monads: a functor is (up to isomorphism) the Kleisli inclusion for a \(j\)-relative monad if and only if it is bijective-on-objects and has a right \(j\)-relative adjoint.

# orderedItems[].object.contentMap.en
@stringdiagram Another nice observation is that the same characterisation works for relative monads: a functor is (up to isomorphism) the Kleisli inclusion for a \(j\)-relative monad if and only if it is bijective-on-objects and has a right \(j\)-relative adjoint.

# orderedItems[].object.content
@zyang In case you didn't see, Dima Szamozvancev responded to the question on the Category Theory Zulip (https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category-theory/topic/Comonadicity.20of.20Presheaf.20Categories) :)

# orderedItems[].object.contentMap.en
@zyang In case you didn't see, Dima Szamozvancev responded to the question on the Category Theory Zulip (https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category-theory/topic/Comonadicity.20of.20Presheaf.20Categories) :)

# orderedItems[].object.content
@MartinEscardo Another relevant reference is Marmolejo–Wood's "Monads as Extension Systems - No Iteration is Necessary" (http://www. tac.mta.ca/tac/volumes/24/4/24-04abs.html). However, they work in the setting of an arbitrary 2-category, so the definition there still requires some specialisation.

# orderedItems[].object.contentMap.en
@MartinEscardo Another relevant reference is Marmolejo–Wood's "Monads as Extension Systems - No Iteration is Necessary" (http://www. tac.mta.ca/tac/volumes/24/4/24-04abs.html). However, they work in the setting of an arbitrary 2-category, so the definition there still requires some specialisation.

# orderedItems[].object.content
@MartinEscardo @jaklt Walters's thesis is freely available (https://openresearch-repository.anu.ed u.au/handle/1885/133321). He defines algebras in extension form. However, he also considers a generalisation of monads to relative monads (there called "devices").

# orderedItems[].object.contentMap.en
@MartinEscardo @jaklt Walters's thesis is freely available (https://openresearch-repository.anu.ed u.au/handle/1885/133321). He defines algebras in extension form. However, he also considers a generalisation of monads to relative monads (there called "devices").

# orderedItems[].object.content
@jaklt @MartinEscardo The notion essentially first appeared in Walters's "An alternative approach to universal algebra" (https://link.springer.com/chapter/10.1 007/BFb0059142), and was expanded upon in his thesis. However, Walters's notation can be a little difficult to read compared to more modern papers.

# orderedItems[].object.contentMap.en
@jaklt @MartinEscardo The notion essentially first appeared in Walters's "An alternative approach to universal algebra" (https://link.springer.com/chapter/10.1 007/BFb0059142), and was expanded upon in his thesis. However, Walters's notation can be a little difficult to read compared to more modern papers.

# orderedItems[].object.content
@MartinEscardo "Monads need not be endofunctors" (https://arxiv.org/abs/1412.7148) is a good reference. (The definitions are presented in the additional generality of relative monads, but specialising to monads relative to the identity functor will give you what you are looking for.)

# orderedItems[].object.contentMap.en
@MartinEscardo "Monads need not be endofunctors" (https://arxiv.org/abs/1412.7148) is a good reference. (The definitions are presented in the additional generality of relative monads, but specialising to monads relative to the identity functor will give you what you are looking for.)

# orderedItems[].object.content
@maxsnew Zhen Lin has a nice characterisation of the finitary algebraic theories whose categories of algebras have finite biproducts (https://math.stackexchange.com/a/11027 62), which shows that commutativity is not necessary.

# orderedItems[].object.contentMap.en
@maxsnew Zhen Lin has a nice characterisation of the finitary algebraic theories whose categories of algebras have finite biproducts (https://math.stackexchange.com/a/11027 62), which shows that commutativity is not necessary.

# orderedItems[].object.content
@ltchen Garner's "Combinatorial structure of type dependency" (https://arxiv.org/abs/1402.6799) may be relevant.

# orderedItems[].object.contentMap.en
@ltchen Garner's "Combinatorial structure of type dependency" (https://arxiv.org/abs/1402.6799) may be relevant.

# orderedItems[].object.content
@stringdiagram Perhaps it's worth mentioning that, while actions/modules are less familiar than algebras from the perspective of ordinary category theory, they are the appropriate notion of algebra for monads in a 2-category (which is where much of their theory originates).

# orderedItems[].object.contentMap.en
@stringdiagram Perhaps it's worth mentioning that, while actions/modules are less familiar than algebras from the perspective of ordinary category theory, they are the appropriate notion of algebra for monads in a 2-category (which is where much of their theory originates).

# orderedItems[].object.content
@maxsnew @stringdiagram @jer_gib Yes, this is precisely the universal property for an Eilenberg–Moore object in a 2-category.

# orderedItems[].object.contentMap.en
@maxsnew @stringdiagram @jer_gib Yes, this is precisely the universal property for an Eilenberg–Moore object in a 2-category.

# orderedItems[].object.content
@maxsnew If you're assuming that \(C\) is a small category with finite coproducts, then the category of finite product-preserving presheaves on \(C\) is equivalent to the cocompetion of \(C\) under sifted colimits, hence a locally strongly finitely presentable category. Such categories can be characterised as those reflective subcategories of presheaf categories for which the right adjoint preserves sifted colimits. However, if you do care about small products, rather than finite products, the situation is more subtle.

# orderedItems[].object.contentMap.en
@maxsnew If you're assuming that \(C\) is a small category with finite coproducts, then the category of finite product-preserving presheaves on \(C\) is equivalent to the cocompetion of \(C\) under sifted colimits, hence a locally strongly finitely presentable category. Such categories can be characterised as those reflective subcategories of presheaf categories for which the right adjoint preserves sifted colimits. However, if you do care about small products, rather than finite products, the situation is more subtle.

# orderedItems[].object.content
@maxsnew What exactly would you like to be able to do?

# orderedItems[].object.contentMap.en
@maxsnew What exactly would you like to be able to do?

# orderedItems[].object.content
@Bryce The favicon was updated just under two weeks ago.

# orderedItems[].object.contentMap.en
@Bryce The favicon was updated just under two weeks ago.

# orderedItems[].object.content
@ohad Hermida constructs this Yoneda structure on Multicat in the (unpublished) "Fibrations and Yoneda structure for multicategories".

# orderedItems[].object.contentMap.en
@ohad Hermida constructs this Yoneda structure on Multicat in the (unpublished) "Fibrations and Yoneda structure for multicategories".

# orderedItems[].object.content
@maxsnew I'm sure you've already come across it, but my impression was that Frey's "A 2-Categorical Analysis of the Tripos-to-Topos Construction" (https://arxiv.org/abs/1104.2776) was motivated by this question (though I've not yet had a chance to read it).

# orderedItems[].object.contentMap.en
@maxsnew I'm sure you've already come across it, but my impression was that Frey's "A 2-Categorical Analysis of the Tripos-to-Topos Construction" (https://arxiv.org/abs/1104.2776) was motivated by this question (though I've not yet had a chance to read it).

# orderedItems[].object.content
@OscarCunningham Yes, when a 2-category admits Eilenberg–Moore objects, this assignment forms an algebra for Mnd.

# orderedItems[].object.contentMap.en
@OscarCunningham Yes, when a 2-category admits Eilenberg–Moore objects, this assignment forms an algebra for Mnd.

# orderedItems[].object.content
@maxsnew They are called "pseudo-operads in Cat" in Day–Street's "Lax monoids, pseudo-operads, and convolution" (http://maths.mq.edu.au/~street/Multic ats.pdf).

# orderedItems[].object.contentMap.en
@maxsnew They are called "pseudo-operads in Cat" in Day–Street's "Lax monoids, pseudo-operads, and convolution" (http://maths.mq.edu.au/~street/Multic ats.pdf).

# orderedItems[].object.content
@ltchen While there is a standard definition of "category", there is no standard definition of "type theory"/"deductive system" (though there are many candidates). However, if you pick a specific framework (e.g. generalised algebraic theories), then one can give a general type theoretic definition of product just as easily as one gives the category theoretic definition of product.

Historically, studying "type theories" in general has not been popular, though it is becoming more fashionable now.

# orderedItems[].object.contentMap.en
@ltchen While there is a standard definition of "category", there is no standard definition of "type theory"/"deductive system" (though there are many candidates). However, if you pick a specific framework (e.g. generalised algebraic theories), then one can give a general type theoretic definition of product just as easily as one gives the category theoretic definition of product.

Historically, studying "type theories" in general has not been popular, though it is becoming more fashionable now.