You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Elisha Goldman (Jan 15 2026 at 14:43):Adjunction can be described with hom-sets and orthogonality, but they can also be described explicitly with some functors with finitely many coherences. Which universal constructions are finitely presentable like this, specifically which ones can I use homotopy.io to reason about?
Limits are adjoints, but they're adjoints from functor categories, which seem equally problematic to define if we can't reference products. Limits in Abelian categories are uniquely characterized by their computational properties, maybe something similar could be applied to ordinary categories somehow. Universals are the same as representables, but that requires a notion of representation homotopy.io doesn't provide (and you'd need a Yoneda structure in your category-of-categories anyway)
Elisha Goldman (Jan 15 2026 at 15:55):Finite limits (into preorders) are finitely presentable (in an unsatisfying way): just write out the schema category with the terminal object explicitly and create an adjunction into your target category. This works since functors into preorders preserve limits iff they're adjoints