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.
Jacques Carette (Nov 25 2021 at 13:38):What's the position of (the various flavours of) sketches in the category theory pantheon? At one point in time, there was a lot of work on these, but they seemed to have largely fallen out of use. [This was brought to mind by the exception that is the paper that just appeared today on the arxiv, naturally.]
Perhaps the better question to ask is: what is the replacement? What is the method of use today for what sketches were used 'then'?
Morgan Rogers (he/him) (Nov 25 2021 at 13:44):There's no replacement; they are just as useful as they have ever been, I think, but there hasn't been much recent effort dedicated to them in their own right. In Johnstone's Sketches of an Elephant there is a nice comparison with other logical frameworks.
Jacques Carette (Nov 25 2021 at 13:59):What surprises me is that I don't see them used much. They really do seem to be a nice specification mechanism. And seem to mesh well with the ideas of doctrines, for example. Though I have yet to see a good explanation of that - or of the relation with operads, for that matter, both of which seem to me to be rather obvious questions.
Nathanael Arkor (Nov 25 2021 at 20:51):@Mike Shulman's recent work LNL polycategories and doctrines of linear logic makes use of a (new) kind of sketch. That could be a good place to look if you're interested in relations between operadic and sketch-like notions.
Nathanael Arkor (Nov 25 2021 at 20:57):I'm not sure this is quite what you're looking for, but Kinoshita–Power–Takeyama in Sketches describe sketches corresponding to finitary (2-)monads. If by "doctrine" you mean something like a 2-monad, then perhaps this is relevant.
Jacques Carette (Nov 26 2021 at 12:45):Indeed, thanks for the pointers.
Evan Patterson (Nov 28 2021 at 02:22):While sketches have an appealing diagrammatic flavor, my guess is that they are not much used because they are extremely verbose compared to equivalent formalisms. Try writing down the theory of categories, or even just the theory of monoids, as a finite limit or finite product sketch, including all the axioms, and compare with the equivalent (generalized) algebraic theories.
Jacques Carette (Nov 28 2021 at 15:06):I'm a big fan of generalized algebraic theories. Thanks for giving me an incentive to just stick with them!
Jon Sterling (Nov 29 2021 at 11:23):I feel that sketches become very useful when it is too complex to carefully present things syntactically. GATs are near the upper limit of feasible complexity for working in a precise way, but they are still within possibility --- which is why they have been so successful.
I like to take the "best of both worlds": writing things down syntactically in nice notations, and claim that it can be sketched. This way I am at least using a "loose notation to make a precise mathematical statement" --- whereas, I find attempts to work entirely "type theoretically" from top to bottom to be more of "using a loose notation to make an imprecise mathematical statement", unless things are done with a level of care that is usually prohibitive.
Jacques Carette (Nov 29 2021 at 14:33):So, when I do 'real' work, these days I pretty much always use Agda. Is that a sufficient level of care?
@Jonathan Sterling can you give me concrete examples of when things are too complex to present syntactically? If I were to guess, maybe you mean when something is given by a construction, and it's easier to 'output' a sketch than a proper definition in type theory? Or is that not it at all?
Reid Barton (Nov 29 2021 at 14:39):If you want to prove that the category of models of an algebraic theory is cocomplete (or better yet, locally presentable) then writing it as the category of models of a limit sketch is a useful "intermediate representation".
Alexander Campbell (Nov 30 2021 at 03:18):Morgan Rogers (he/him) said:
In Johnstone's Sketches of an Elephant there is a nice comparison with other logical frameworks.
As one might expect from the book’s title ;-)
Jon Sterling (Nov 30 2021 at 08:15):@Jacques Carette The difficulty is usually not "presenting it in type theory" vs. "sketching" --- this is usually just a matter of taste. The difficulty lies rather in the choice between "constructing a finitary 2-monad for some new kind of structure" vs. "constructing the type theory / logical framework for this structure and showing that it is sound and complete for the desired category of models". The former can often be done very easily by virtue of some nice math and general results, whereas the latter is even in the "easy" cases almost beyond what we can rigorously do by hand --- see Streicher's syntactical initiality argument, for instance, a variant of which was recently formalized in Agda.
Morgan Rogers (he/him) (Nov 30 2021 at 09:17):Alexander Campbell said:
Morgan Rogers (he/him) said:
In Johnstone's Sketches of an Elephant there is a nice comparison with other logical frameworks.
As one might expect from the book’s title ;-)
Disappointingly, a sketch for the theory of Elephants is not provided...
Jacques Carette (Nov 30 2021 at 11:48):@Jonathan Sterling Just so that I understand fully, let me rephrase: the difficulty is not in defining and using particular theories via a presentation (in either setting), but rather in doing the meta-theory of that newly defined item.
Jon Sterling (Nov 30 2021 at 11:51):@Jacques Carette That's right! So what I do in practice is write down "type theoretic" presentations of theories, and then point out that they correspond to sketches for a certain 2-monad. This way I avoid needing to develop the metatheory of the logical framework.
Jon Sterling (Nov 30 2021 at 15:03):Btw. It is perhaps worth explaining why this doesn't "beg the question" of syntactic initiality --- one only has to interpret finitely many "type theoretically defined" constants into the abstract internal language determined by the doctrine, which can be thought of as a "read-time" procedure to be executed by the mathematical reader. One is not relying on the (true, but harder to establish rigorously) fact that some formal syntax that is notated with turnstiles is sound and complete.
Jon Sterling (Nov 30 2021 at 15:04):(It is much like how one can work with groups without developing the formal syntax of groups.)
Jacques Carette (Nov 30 2021 at 15:32):To flesh out the analogy: you only need the axiomatic description of groups, not reason over actual presentations in terms of generators and relations.
Note that although I am familiar with the idea of 'doctrine' (and some generalizations), I have yet to see a definition that is formal enough that I can "write it down in Agda". Do you know if it is indeed a fuzzy idea, or something that can be properly formalized?
Nathanael Arkor (Nov 30 2021 at 15:59):Do you know if it is indeed a fuzzy idea, or something that can be properly formalized?
It is a fuzzy idea (see [[doctrine]] for some suggestions as to what it could mean, none of which are particularly satisfactory).
Jon Sterling (Nov 30 2021 at 16:43):Jacques Carette said:
To flesh out the analogy: you only need the axiomatic description of groups, not reason over actual presentations in terms of generators and relations.
Note that although I am familiar with the idea of 'doctrine' (and some generalizations), I have yet to see a definition that is formal enough that I can "write it down in Agda". Do you know if it is indeed a fuzzy idea, or something that can be properly formalized?
It is both a fuzzy idea and several precise ideas. One of the precise ideas is "2-monad", and with this version you can develop a number of important things: the presentation of doctrines by generators and relations, and the presentations of theories in the doctrine by sketches. Based on the exposition of Kinoshita, Power, and Takeyama (https://www.sciencedirect.com/science/article/pii/S0022404998001145?via%3Dihub), Daniel Gratzer and I wrote some elementary tutorial examples here: https://www.jonmsterling.com/abstracts.html#gratzer-sterling:2020
Jon Sterling (Nov 30 2021 at 16:46):Jacques Carette said:
To flesh out the analogy: you only need the axiomatic description of groups, not reason over actual presentations in terms of generators and relations.
Note that although I am familiar with the idea of 'doctrine' (and some generalizations), I have yet to see a definition that is formal enough that I can "write it down in Agda". Do you know if it is indeed a fuzzy idea, or something that can be properly formalized?
Maybe to be a little more precise: it is always important / non-optional to be able to present groups in terms of generators and relations, but the generators and relations are still just treated as ordinary mathematical objects and not as syntax. For algebraic theories there is actually very little difference (which is why it is easy in a second-semester categorical logic course to have the students derive the syntactic metatheory of algebraic theories completely from scratch), the difference between "generators and relations" and "the entire syntax of the language of XXX theories" becomes quite large. This is the difference between presenting MLTT by a number of constants in the Logical Framework, vs. presenting it as dozens of rules (including congruence rules, etc.).
Jon Sterling (Nov 30 2021 at 16:47):So there are two layers of presentation, which in much of the literature get squashed into one. There is the presentation of the logical framework by rules of deduction (unnecessary but sometimes useful) and there is the presentation of the theory by constants in the logical framework (almost always necessary). In mainstream type theoretic literature, people do both steps at once --- and therefore lose the opportunity to skip unnecessary work.
Nathanael Arkor (Nov 30 2021 at 16:52):If I understand the distinction you're making, my feeling is that, in practice, people tend not to use logical frameworks at all, and usually instead choose to informally write down some rules they know will be generally understood by their audience. Papers using logical frameworks are typically being more rigorous than most.
Jon Sterling (Nov 30 2021 at 16:52):In the case of groups, guess there's really three layers!
1) You can present the doctrine of algebraic theories by judgments and rules of deduction.
2) You can present the theory of groups by a (non-unique choice of) generators and equations in the language of algebraic theories.
3) You can present a single group in the language of groups by generators and relations.
Anyway, it's good to be able to decide for yourself where you are getting mileage out of presentations. My experience is that presentations play an crucial role in all three levels, but that "mathematical" versions of presentations are better in all cases than the "turnstiles and horizontal lines" presentations --- what makes a presentation "mathematical" in my view is that it doesn't require you to specify silly congruence rules, etc., which tend to just blow up your theory in ways that make it too unwieldy to prove anything about rigorously.
So I am not against presentations... But I am very much against presentations in languages where you must manually close your language under "substitution of equals for equals". There is absolutely no need for this anywhere, but it is something that people often insist on...
Jon Sterling (Nov 30 2021 at 16:54):Nathanael Arkor said:
If I understand the distinction you're making, my feeling is that, in practice, people tend not to use logical frameworks at all, and usually instead choose to informally write down some rules they know will be generally understood by their audience. Papers using logical frameworks are typically being more rigorous than most.
Right. People who don't use LFs like to make mountains out of the molehill of things like initiality etc., in particular because their ill-equipped methods truly do turn it into Mount Everest... My preference is to just work informally, but make sure everything I am doing corresponds to something mathematically meaningful on its own, as opposed to building up these immense sand-castles and then making sure that every turret has an even number of grains.
John Baez (Nov 30 2021 at 22:19):Jonathan Sterling said:
Jacques Carette said:
To flesh out the analogy: you only need the axiomatic description of groups, not reason over actual presentations in terms of generators and relations.
Note that although I am familiar with the idea of 'doctrine' (and some generalizations), I have yet to see a definition that is formal enough that I can "write it down in Agda". Do you know if it is indeed a fuzzy idea, or something that can be properly formalized?
It is both a fuzzy idea and several precise ideas. One of the precise ideas is "2-monad", and with this version you can develop a number of important things: the presentation of doctrines by generators and relations, and the presentations of theories in the doctrine by sketches.
Right: it's a fuzzy idea which has been formalized in a number of very fruitful ways. There are a number of ways of describing algebraic structures on sets (or objects in other categories): monads is one, and Lawvere theories is another, and there are plenty more. We can categorify any one of these concepts and get a way of describing algebraic structures on categories (or objects in other 2-categories). Any of these ways of describing algebraic structures on categories can loosely be called a 'doctrine'.
But we can be precise too: we can categorify the concept of monad and get the concept of 2-monad or more generally pseudomonad, and there's a huge wonderful literature on pseudomonads.
John Baez (Nov 30 2021 at 22:20):James Dolan prefers to categorify the concept of Lawvere theory, and he's been doing a bunch of work on doctrines using that approach.
Nathanael Arkor (Nov 30 2021 at 22:29):John Baez said:
James Dolan prefers to categorify the concept of Lawvere theory, and he's been doing a bunch of work on doctrines using that approach.
Is this his work on algebraic geometry? Do you have any idea when we might be able to read about his ideas in more detail? I'm very intrigued by what I've read on the nLab.
Mike Shulman (Dec 01 2021 at 02:13):One reason for there being different notions of doctrine is that just as each doctrine (= 2-theory) comes with its own separate class of (1-)-theories (e.g. finite product theories, finite limit theories, ...), each 3-theory comes with its own separate class of 2-theories! I wrote some about this here.
John Baez (Dec 01 2021 at 05:23):Nathanael Arkor said:
Is this his work on algebraic geometry?
Yes, and maybe other things - I haven't been talking to him for quite a while. Todd Trimble has.
Do you have any idea when we might be able to read about his ideas in more detail?
I doubt you ever will! I wrote some notes about the doctrine of algebraic geometric theories, but that covered just a short stretch of our conversations back in 2010.
John Baez (Dec 01 2021 at 05:24):If you really want to learn what he's doing, it'd be best to talk to him.
Morgan Rogers (he/him) (Dec 01 2021 at 09:30):Jonathan Sterling said:
People who don't use LFs like to make mountains out of the molehill of things like initiality etc., in particular because their ill-equipped methods truly do turn it into Mount Everest... My preference is to just work informally, but make sure everything I am doing corresponds to something mathematically meaningful on its own, as opposed to building up these immense sand-castles and then making sure that every turret has an even number of grains.
Sometimes there be gold in them mountains!
Jacques Carette (Dec 01 2021 at 12:32):@Mike Shulman Thanks. In the wording of that essay, I am equally interested in the fully syntactic and the fully semantic approaches.
And as @Jonathan Sterling mentions, for groups there are (at least) 3 layers to be seen, and that hints that indeed there will be situations with layers. And I'd like to be able to be quite precise about that (i.e. by formalizing what others have written down as 'precise', inventing when I have no other choice).
Asad Saeeduddin (Jan 08 2022 at 13:53):@Jacques Carette I believe that the recent categorical databases stuff is all secretly based on sketches
Jacques Carette (Jan 10 2022 at 14:01):Secretly?