Updated the references.

]]>Added Michał Przybyłek’s thesis.

]]>Just to say thanks for again taking the time to reply.

I am now distracted with something else, but I’ll come back to this.

]]>I picked that example at random, just feeling that in a given situation it might well be easier to directly check some kind of solution set condition than to first come up with and check the existence of no less than two idempotent pseudomonads, just to start with. But I am just speaking superficially here and may be way off, just sharing my user-experience.

If one is interested in ordinary adjointness, as opposed to something like multiadjointness, then it suffices only to have one lax idempotent pseudomonad $P$ around, which would typically be the appropriate notion of free small cocompletion in that context. The adjoint functor theorem in this context says that a 1-cell is left adjoint if and only if it preserves $P$-colimits, and is “$P$-admissible”, i.e. admits a nerve with respect to $P$, which is the formal analogue of the solution set condition.

With a formal theory of relative monads in hand, do we get a nice relative analog of the classical fact that for a monad on a symmetric closed category to lift to an enriched/internal monad is equivalent to it having symmetric monoidal monad structure?

I believe this should follow from formal considerations. I imagine the correspondence between strong and enriched monads follows from an equivalence between the equipment of actions of a monoidal category, and the equipment of enriched categories, under suitable assumptions on the monoidal category $V$ (along the lines of Enrichment through variation): this equivalence would then preserve relative monads. However, I’ve not yet checked the details.

]]>I see, thanks.

I picked that example at random, just feeling that in a given situation it might well be easier to directly check some kind of solution set condition than to first come up with and check the existence of no less than two idempotent pseudomonads, just to start with. But I am just speaking superficially here and may be way off, just sharing my user-experience.

But here is a question I actually care about (which may be comparatively trivial, please bear with me):

With a formal theory of relative monads in hand, do we get a nice relative analog of the classical fact that for a monad on a symmetric closed category to lift to an enriched/internal monad is equivalent to it having symmetric monoidal monad structure?

I see vague allusion to this on p. 3 of Arkor & McDermott 2023a, but I am not sure if the question can be extracted from the discussion there.

]]>Re. #36:

What I was after are theorems recognizable outside the area of formal category theory itself. Imagine somebody who is into category theory but without background in formal category theory, what can the latter offer them?

Many of these references play a similar role, say, to Kelly’s *Basic Concepts of Enriched Category Theory*. That is, they are useful when someone is working in a context whose category theory has not been well developed (such as enriched category theory without symmetry/cocompleteness) and they want to know that the fundamental theorems of category theory hold in this setting, rather than having to derive the results from scratch in their particular setting. For example, Gordon and Power have a series of papers in which they develop enough bicategory-enriched category theory to be sufficient for their applications in computer science (e.g. Algebraic structure for bicategory enriched categories), because a general theory was not available. However, now many of these results may be derived from analogous results in formal category theory. Another example is Shulman’s Enriched indexed categories, in which he develops much basic category theory in this new setting, but whose results follow from analogous results in formal category theory (as he notes this in that paper), though at that time many of the requisite results had not been established.

Formal category theory has also been established with specific applications in mind, e.g. in Wood et al’s work on constructive complete distributivity, but I think the main motivation is to provide a general framework for doing “category-like theory”, so as to be of use to category theorists generally.

Formal category theory is more useful the earlier it is developed, since it prevents a proliferation of references on different flavours of category theory with essentially the same definitions and proofs. (Take, for example, the recent introduction of categories enriched in a skew-monoidal category, whose theory may now be derived from formal category theory, rather than needing to carry out a Kelly-like programme in slight additional generality.)

This sounds like a great statement, but it may require serious work to unwind what it is saying for a concrete situation.

That paper in particular includes a number of concrete examples that show how to unwind it for specific situations, though I imagine it is probably easier for the reader to look at the paper directly for that. The purpose of the paper was less to prove some conjecture, and rather to show that a number of isolated adjoint functor theorems in the literature were instances of a more general theorem, making it easier to come up with new variants as applications demand, without needing to reprove each variant individually. However, the theorems in question, that were previously in the literature, are all in the setting of ordinary categories; whereas the general theorem in that paper can immediately be specialised to enriched categories, etc.

]]>Add a sentence about one motivation for the development of formal category theory.

]]>Thanks for adding the long list of theorems.

What I was after are theorems recognizable outside the area of formal category theory itself. Imagine somebody who is into category theory but without background in formal category theory, what can the latter offer them?

Such people might well be in need of an adjoint functor, say, in a given situation. So they follow your link to Arkor et al 23, Theorem 2.16…

This sounds like a great statement, but it may require serious work to unwind what it is saying for a concrete situation.

Can we extract from this a tangible corollary, of the kind:

“For example in the case that the lax-idempotent pseudomonads $R$ and $I$ are taken to be such-and-such, this theorem positively answers the question of existence of adjoints which was previously left-open in …”

?

]]>Added further references. These references are of a different nature, in that they develop the theory of proarrow equipments (or other formalisms for formal category theory), rather than developing category theory inside such a formalism. However, they still fall very much within the purview of formal category theory, as their motivation is to study the structure of categories. To explain this distinction, I’ve introduced two terms: “intramural” (to refer to doing category theory inside a 2-dimensional structure) and “extramural” (to refer to studying the theory of such 2-dimensional structures). There may be good existing terms for this distinction, or better alternatives. Feel free to offer suggestions. Even in the 1-dimensional case, I’m not sure I’ve seen this distinction being drawn explicitly, but I think it can be helpful.

]]>Add some mention of theorems. This is a rather biased selection at the moment; I will try to add more later. (The references on codiscrete cofibration are relevant, for instance, as are the many papers on the monads-and-bimodules construction.)

]]>Added reference to Trimble’s epistemologies.

]]>Moved content on formal (infinity, 1)-category theory to a standalone page.

]]>Thanks, looks good.

Maybe some of the original Idea-section was not completely useless? :-)

Such as the comparison to “formal set theory” one dimension down?

]]>Re. #28: I will bring the (infinity, 1)-categorical page into line with this one, and also give some references to theorems that have been proven in formal category theory. (I will continue editing in a couple of hours.)

]]>Rewrote the introduction and approaches section. (More to follow.)

]]>You wanna take care of that, or shall I?

By the way, while we have the momentum:

What the entry badly needs after presenting the heavy machinery is to show some output:

What are useful theorems in formal category theory which make the machinery worthwhile?

]]>Perhaps the references to formal (infinity, 1)-category theory should be moved to synthetic (infinity,1)-category theory. “Formal” and “synthetic” appear to be being used in the same context, which is unfortunate. It would be better to have a single name.

]]>Formal category theory is intended to capture all flavours of (one-dimensional) category theory, e.g. ordinary category theory, internal category theory, enriched category theory, fibred category theory, internal category theory, etc. Enriched category theory is notable only because it is a useful and widely used flavour, and because there are subtleties in the enriched setting that are not visible in ordinary or internal category theory (e.g. not every weighted colimit may be expressed as a conical colimit). I shall try to expand upon this in the introduction.

]]>Would it make sense to speak of *formal enriched category theory*, for definiteness?

Thanks.

I have just swapped your paragraph withe the previous one, so that its lead-in via “This is analogous to…” still makes sense.

]]>I will try to clean this up a little more this evening.

]]>Rephrase the introduction so that it no longer talks about the 2-category Cat, and instead highlights that more structure is needed than simply a 2-category.

]]>Looks good.

What is maybe still missing is an indication that all these tools are needed to do something more ambitious than what the Idea-section currently advertises:

The idea section currently just speaks about using a plain old 2-category $Cat$ in order to do formal theory of plain categories.

Somewhere there should be a line saying that one can also consider more ambitious projects like “formal enriched category theory” which then require an ambient context richer than a plain 2-category. Or something like this.

]]>I’ve edited the text regarding the approaches slightly. It needs a bigger rework, but this is in a slightly more appropriate form for the nLab.

]]>