Category Theory
Zulip Server
Archive

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.

Stream: practice: terminology & notation

Topic: Doctrines

John Baez (Oct 13 2023 at 10:57):

I bumped into a potentially interesting new paper on the arXiv today:

• Francesca Guffanti, Rich doctrines and Henkin's Theorem.

I'd been wanting to prove a version of Henkin's theorem for Boolean hyperdoctrines and this seems to do something like that in much greater generality. Which would be great. But I'm thrown by one thing: she seems to be using the word "doctrine" to mean something like what I'd call a "hyperdoctrine". Is this common now?

John Baez (Oct 13 2023 at 11:02):

On the one hand I like this because in the old sense a hyperdoctrine is

essentially an axiomatization of the collection of slices of a locally cartesian closed category (or something similar): a category T together with a functorial assignment of “slice-like”-categories to each of its objects, satisfying some conditions.

or in other words:

a collection of contexts together with the operations of context extension/substitution and quantification on the categories of propositions or types in each context.

while a doctrine,

.... as the word was originally used by Jon Beck, is a categorification of the concept of “theory”. Thus, a doctrine could also reasonably be called a “2-theory.” Here we are using the word “theory” in a vague non-precise sense. For instance, there is a theory of groups, a theory of abelian groups, a theory of commutative rings, and so on. Likewise, there is a doctrine of monoidal categories, a doctrine of categories with finite products, a doctrine of rig categories, and so on.

John Baez (Oct 13 2023 at 11:02):

So, in the old sense, a hyperdoctrine doesn't feel (to me) like a "hyper" version of a doctrine.

John Baez (Oct 13 2023 at 11:03):

But on the other hand, it seems pretty confusing to just get rid of the prefix "hyper-" and use "doctrine" to mean "hyperdoctrine". After all, there are plenty of people who use "doctrine" to mean a categorified theory: either a 2-monad on Cat, or a 2-Lawvere theory, or something else like that.

Nathanael Arkor (Oct 13 2023 at 11:07):

My impression is that it went a little like this: Lawvere introduced a structure he called a "hyperdoctrine". In subsequent years, people reused the terminology for variations on the concept (sometimes prefixing "hyperdoctrine" with some qualifier to distinguish it from Lawvere's definition). At a certain point, those in the hyperdoctrine community dropped "hyper" for convenience, using "doctrine" with a qualifier to refer to similar concepts (with "hyperdoctrine" continuing to refer to Lawvere's original definition). However, people outside the hyperdoctrine literature continue to use "hyperdoctrine" for anything resembling a Lawvere hyperdoctrine, and "doctrine" for the the general concept of a 2-dimensional notion of theory.

Nathanael Arkor (Oct 13 2023 at 11:08):

So there is an unfortunate divergence of terminology.

John Baez (Oct 13 2023 at 11:18):

At a certain point, those in the hyperdoctrine community dropped "hyper" for convenience, using "doctrine" with a qualifier to refer to similar concepts ....

Wow, they forgot to tell me! :upside_down:

John Baez (Oct 13 2023 at 11:19):

About when did this happen, and who were some of the big names in the hyperdoctrine community at that time?

John Baez (Oct 13 2023 at 11:22):

(It's unfortunate that I came up with the dream of redoing a lot of model theory for classical first-order logic using Boolean hyperdoctrines without knowing anything about the "hyperdoctrine community" and their work. It was just a dream of mine, and I quit working on it almost before I got started, but if I ever decide to resume I should educate myself a bit first.)

Nathanael Arkor (Oct 13 2023 at 12:12):

John Baez said:

About when did this happen, and who were some of the big names in the hyperdoctrine community at that time?

The earliest usage in this sense that I'm aware of is in Maietti–Rosolini's 2012 Elementary quotient completion and Quotient completion for the foundation of constructive mathematics. There, "doctrine" is often qualified, but not always. By "hyperdoctrine community", I am really referring to the community who have been working on topics stemming from these and related papers. So my impression is that this usage is fairly modern.

Nathanael Arkor (Oct 13 2023 at 12:15):

I imagine someone who is closer to that community, e.g. @Joshua Wrigley, could give a better answer, though.

John Baez (Oct 13 2023 at 12:17):

Thanks!

Reid Barton (Oct 13 2023 at 16:16):

I noticed that usage here: https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/Doctrines.2C.20adjoints.2C.20and.20all.20that/near/371948569
and was slightly confused by it. I mean, it was not confusing in that the word "doctrine" was obviously being used to refer to what I would call a "hyperdoctrine", but I was slightly confused about why that was happening.

John Baez (Oct 13 2023 at 16:48):

Oh yeah, that puzzled me too.

John Baez (Oct 13 2023 at 16:49):

Well, now that hyperdoctrines are being called doctrines, I guess we can call the old-fashioned doctrines "hypodoctrines".

Mike Shulman (Oct 13 2023 at 17:03):

Like how now that $(\infty,1)$-categories get called $\infty$-categories, we have to call the old-fashioned ones $(\infty,\infty)$-categories?

Kenji Maillard (Oct 13 2023 at 17:04):

Maybe that's a bit of a side-track, but are hyperdoctrines instances of the concept of doctrine (at least in the sense of some sort of 2-theory/some structured category/some collection of algebras for a 2-monad) ?
I can see how the collection of hyperdoctrines should collectively form a doctrine (each hyperdoctrine is a category equipped with some structure) but not how each individual hyperdoctrine can be seen as a general theory.

Mike Shulman (Oct 13 2023 at 17:05):

I don't think so -- I think hyperdoctrines are really a kind of theory, not a kind of doctrine.

Evan Patterson (Oct 13 2023 at 20:12):

Would it be reasonable to say that classes of hyperdoctrines with certain structure---regular hyperdoctrines, coherent hyperdoctrines, first-order hyperdoctrines, etc---are doctrines? That kind of makes sense to me, but it would be an unfortunate misalignment of terminology.

Evan Patterson (Oct 13 2023 at 20:13):

Ah nevermind, I see that Kenji just said exactly that.

Jonas Frey (Oct 13 2023 at 20:40):

Evan Patterson said:

Would it be reasonable to say that classes of hyperdoctrines with certain structure---regular hyperdoctrines, coherent hyperdoctrines, first-order hyperdoctrines, etc---are doctrines? That kind of makes sense to me, but it would be an unfortunate misalignment of terminology.

Yes I agree with your and @Kenji Maillard 's point of view, and I'm really confused about Lawvere's use of the word "hyper" when going from 2-theories to indexed categories.

Jonas Frey (Oct 13 2023 at 21:02):

But it seems that Lawvere himself was aware that his terminology was problematic: In this talk he says around 4:50:

Here I use the term doctrine, due to Jon Beck, which in general is supposed to signify "something like a theory, but higher". Now there've been interpretations to this "higher", so ... um ... maybe even unfortunately I've used the word doctrine in quite distant, different ways ... one interpretation of higher, as I've mentioned already today, was to treat the logic of (a) higher types but (b) not simply in terms of predicates on these types but rather a mathematical model of actual proofs as opposed to mere existence of proofs. These two features were incorporated in my 1968 notion of hyperdoctrine which has figured in some later work for example in Bart Jacobs' thesis (1990) on *comprehension categories". (mumble) However in the present connection I'm referring to doctrines in the general sense of "a kind of theory whose models can in turn be construed as theories". And much more specifically [...] to 2-monads on the category of categories -- 2-monads on the category of categories with the property that the category S of small categories is an algebra.

I'm stopping to write here, but I recommend the entire talk.

Concerning the word "hyper", he seems to justify it by referencing proof-relevance in indexed categories? That would justify dropping it again for indexed posets ... still, "(posetal) hyperdoctrines" are in no way theories of theories, which I assume he is referring to when saying "maybe even unfortunately".

Jonas Frey (Oct 13 2023 at 21:04):

(I wonder what he meant by "the logic of higher types")

Nathanael Arkor (Oct 13 2023 at 21:07):

Jonas Frey said:

(I wonder what he meant with the logic of higher types)

I might guess he could have meant a "types of types" ("kinds" in type theory parlance), for instance as featuring in the polymorphic $\lambda$-calculus (PLC), which is also called the "second-order $\lambda$-calculus". The PLC may be modelled using a kind of hyperdoctrine, so it would fit in this context.

Jonas Frey (Oct 13 2023 at 21:11):

That's a possibility, but he could also have meant higher types in the classical sense of proof theory, ie (iterated) function types.

Or he could have meant "higher types" in the sense of categorification, since the overall theme is categorification of theories.

John Baez (Oct 14 2023 at 13:56):

I haven't listened to him but since Lawvere didn't like categorification I'd guess he would use "higher" in the same sense as Lambek and Scott's Introduction to Higher-Categorical Logic: basically just iterated function types.

Joshua Wrigley (Oct 15 2023 at 12:27):

Reid Barton said:

I noticed that usage here: https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-questions/topic/Doctrines.2C.20adjoints.2C.20and.20all.20that/near/371948569
and was slightly confused by it. I mean, it was not confusing in that the word "doctrine" was obviously being used to refer to what I would call a "hyperdoctrine", but I was slightly confused about why that was happening.

I appreciate that in that thread I only answered @Simon Burton's direct question and didn't give any context for what was going on in that example. The particular doctrine (hyperdoctrine) shown in the first slide is built from formulae using only the symbols $\bot, \land, \lor, \top$ and the unary predicate symbol $U$. It is the doctrine associated to the empty theory over this fragment.

The second slide was an attempt at visualizing that this doctrine also has left adjoints to the inclusions $\vec{x} \hookrightarrow \vec{x},\vec{y}$. In other words, the doctrine interprets existential quantification $\exists$. Indeed, it is the doctrine associated to the theory $\{\,\top \vdash \exists x \ U(x)\,\}$ over the fragment $\bot, \land, \lor, \top, \exists$.

So this doctrine simultaneously represents two inequivalent theories $\emptyset \not \equiv \{\,\top \vdash \exists x \ U(x)\,\}$ over two different fragments of logic. The purpose of this example was to motivate endowing a doctrine with further structure to keep track of which logical operations are being interpreted.

Steve Awodey (Oct 21 2023 at 17:20):

John Baez said:

But on the other hand, it seems pretty confusing to just get rid of the prefix "hyper-" and use "doctrine" to mean "hyperdoctrine". After all, there are plenty of people who use "doctrine" to mean a categorified theory: either a 2-monad on Cat, or a 2-Lawvere theory, or something else like that.

I agree that this is potentially confusing -- and inaccurate, based on the past use of the word "doctrine" -- but it's spreading. I was recently at this meeting, which seemed to be using the same terminology.

Mike Shulman (Oct 22 2023 at 00:13):

On the other hand, I've always found it a bit weird to introduce a whole new word "doctrine" for what is really just a "2-theory". So maybe if "doctrine" gets stolen to mean something else, we can all start talking more sensibly about "2-theories" instead for the things that used to be called "doctrines". (-:O

Ivan Di Liberti (Oct 22 2023 at 14:39):

Mike Shulman said:

On the other hand, I've always found it a bit weird to introduce a whole new word "doctrine" for what is really just a "2-theory". So maybe if "doctrine" gets stolen to mean something else, we can all start talking more sensibly about "2-theories" instead for the things that used to be called "doctrines". (-:O

I only agree to some extent. The models of the "doctrine of coherent categories" are (a certain kind of) theories, so I would rather call them "logics", if anything. I am ok with "2-theories", but I find "doctrine" more leaning towards the word "logic", and thus more conceptually appropriate.