Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
David. Have you seen this?
Mention KZ doctrines and remove duplicate link.
I have edited this entry a fair bit:
Have touched the original text to make it flow better (I hope) and added some crucial cross-links, such as with ETCC and with 2-topos.
Then I added paragraphs on how:
in one direction, this “formal category theory” is the categorification of the discussion of set theory via the topos of sets,
while, in the other direction, it further categorifies to the untrodden territory of formal -category theory seen in the full -topos
which however is already interesting in Verity & Riehl’s “formal -category theory” seen in “just” ,
(which, at least for the case of presentable -categories, is accessible already as 2Ho(ComModCat).)
As one source I found for exactly this terminology, I added pointer to:
added publication data and hyperlinks to:
Formal category theory should be taken to be an axiomatisation of the properties of VCat, not Cat. This is an important distinction, because Cat has some unusual structure that is not enjoyed more generally by 2-categories of enriched categories. In particular, it has a “nice” Yoneda structure (i.e. it satisfies Axiom 3* of Street and Walters). Therefore, I don’t think it’s accurate to say that formal category theory is directly related to 2-topos theory, because the evidence suggests that only nice Yoneda structures form 2-toposes (as studied by Weber). I haven’t made any changes accordingly yet, because I want to leave this open for discussion, but I think it’s a subtle but important point.
Why not consider adding demand for nice Yoneda structure to the axioms of formal category theory?
Because then you don’t capture 2-categories of enriched categories for most bases of enrichment, which is a motivating class of examples. Nice Yoneda structures are generally those arising from internal categories, which tend to be “better behaved” than enriched categories.
Maybe what you really want to do is add to the entry a line saying that there is an extra axiom which one may add to reduce formal category theory of general enriched categories to that of -enriched categories.
I’ll try to figure out a clear way to put it and update the page accordingly.
Added a reference
Thanks for the reference.
It’s not clear to me what the line between formal category theory and synthetic category theory is (if there even is one). Dan and I were calling our proofs “synthetic” until recently when we changed the name to emphasize the continuity with prior work.
I don’t feel the message in the Category Theory Zulip server was entirely suited to placing wholesale on the nLab, as it was intended specifically as a response to someone who wanted a starting point for learning about formal category theory. In particular, there is often a trade-off between the simplicity of an approach, and its expressivity. For instance, (augmented) virtual equipments are more complicated structures than proarrow equipments, but are also much more expressive (for instance, in capturing enriched category theory without assumptions on the base of enrichment). So if one wishes to work very generally, it is better to work in the (augmented) virtual setting, and it seems reasonable to suggest these approaches to someone learning formal category theory.
However, the trade-off between virtual equipments and augmented virtual equipments is a little more subtle since, from what I have understood, many of the natural examples of augmented virtual equipments naturally reside inside a larger (non-augmented) virtual equipment (e.g. for instance, (Set, Set’)-Prof resides within Set’-Prof). So here the trade-off has a different flavour, less about examples, and more about simplicity of definitions and proofs: a prime example being the additional complexity of an augmented virtual double category, versus the simplicity of admissibility in that setting (an analogous development in a virtual equipment necessitating specifying some class of admissible proarrows).
Really it would be helpful to rework this nLab page entirely and give a more detailed introduction to these ideas and their trade-offs. Perhaps I shall find the time to do so. Part of the difficulty is that any such discussion is necessarily somewhat hand-wavy, because there are many aspects of formal category theory that have not yet been established in any one setting, making it impossible to give a precise comparison by reference to the literature (though this situation has been steadily improving, in no small part due to Roald’s work).
(I should finally mention that there were some misspellings of people’s names on Zulip and consequently in the nLab page. These have now been fixed.)
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 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.
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.
I will try to clean this up a little more this evening.
Would it make sense to speak of formal enriched category theory, for definiteness?
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.
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.
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?
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.)
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?
Added reference to Trimble’s epistemologies.
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 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.
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 and are taken to be such-and-such, this theorem positively answers the question of existence of adjoints which was previously left-open in …”
?
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.
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.
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 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 -colimits, and is “-admissible”, i.e. admits a nerve with respect to , 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 (along the lines of Enrichment through variation): this equivalence would then preserve relative monads. However, I’ve not yet checked the details.
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.
1 to 43 of 43