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: learning: questions

Topic: Doctrines, adjoints, and all that

Simon Burton (Jul 03 2023 at 10:26):

I recently was inspired by a talk at SYCO 11 by @Joshua Wrigley . The talk opens with an example doctrine:
image.png

A doctrine here is defined to be any (contravariant) functor landing in the category of pre orders. In the example we see the domain of this functor is the category of finite sets. These we think of as sets of variables, and the maps are relabellings. The arrows in this picture show two such relabellings, or rather, the image under the doctrine functor of two relabellings.

Simon Burton (Jul 03 2023 at 10:31):

So these are monotone maps, whose adjoints somehow capture quantification:
image.png
The diagram here has encoded the adjoint maps (i think its the left adjoint) using colours. And I'm just wondering, how exactly do these adjoints capture (existential) quantification?

Joshua Wrigley (Jul 03 2023 at 21:11):

Hi Simon, it's still a surprise to see my slides used to explain doctrines, but I'm glad my time spent in tikzpicture didn't go to waste!

Existential quantification is the left adjoint to the substitution map given by the inclusion of a subcontext $\vec{y} \hookrightarrow \vec{x},\vec{y}$. The left adjointness comes in because the axioms that describe existential quantification are identical to requirement that existential quantification is a left adjoint. The unit condition is the sequent $\varphi(\vec{x},\vec{y}) \vdash_{\vec{x},\vec{y}} \exists \vec{x} \ \varphi(\vec{x},\vec{y})$ that expresses the fact that "if $\varphi(\vec{n},\vec{m})$ (for some $\vec{n},\vec{m}$), well then it is evidently true that there exists some $\vec{x}$ such that $\varphi(\vec{x},\vec{m})$". Meanwhile the counit condition is almost more trivial: $\exists \vec{x} \ \psi(\vec{y}) \vdash_{\vec{y}} \psi(\vec{y})$ expresses that whenever there exists some $\vec{x}$, then $\psi(\vec{y}) \vdash_{\vec{y}} \psi(\vec{y})$. The only reason this later sequent is not an equivalence (notationally $\exists \vec{x} \psi(\vec{y}) \equiv_{\vec{y}} \psi(\vec{y})$) is because the type might not always be inhabited. If we restrict to theories in which every model is inhabited, equivalently every model is non-empty, or in the presence of the axiom $\top \vdash_{\emptyset} \exists \vec{x} \ \vec{x} = \vec{x}$, then we do obtain an equivalence $\exists \vec{x} \ \psi(\vec{y}) \equiv_{\vec{y}} \psi(\vec{y})$.

The other conditions we require of the left adjoint in doctrine theory, namely Frobenius reciprocity and Beck-Chevalley, describe how existential quantification interacts with, respectively, conjunction $\land$ and substitution. All of this can be found in more detail in the original paper by Lawvere.

Simon Burton (Jul 11 2023 at 11:54):

I'm guessing that the unit and counit conditions that you have written correspond to closure operators on one of these preorders (Heyting algebras in this case). However, i still have no clue how this connection is made. These closure operators don't seem to have anything to do with existential quantification that I can see. Probably it is something obvious that I'm missing.

John Baez (Jul 11 2023 at 12:58):

And I'm just wondering, how exactly do these adjoints capture (existential) quantification?

My blog series with Michael Weiss might help:

• First-order categorical logic.

We use a rather old-fashioned concept of 'hyperdoctrine', which starts out being a functor from the category FinSet of finite sets to the category BoolAlg of boolean algebras and order-preserving maps. So, any function gives such a map between Boolean algebras, and in Part 3 we figure out/explain how the adjoints of this map correspond to quantifiers. But maybe you already understand that by now and are trying to figure out something else, like how 'closure operators' come into the game.

Simon Burton (Jul 11 2023 at 13:44):

Thankyou John that looks very helpful. I'll try to draw some pictures of posets (boolean algebras in this case), and see if i can join this up with Joshua's diagrams. Maybe what's confusing me is the distinction between a semantic boolean algebra, like a powerset, and a syntactic boolean algebra, where its all formulas up to equivalence.

John Baez (Jul 11 2023 at 14:54):

Part of the point of hyperdoctrines is precisely to blur that distinction, and work with syntax and semantics in a common framework, so that the map from syntax to semantics is a map between two things of the same kind!

Remember, this idea goes back to Lawvere, and Lawvere is the guy who described an "algebraic theory" as a category with finite products, and a model of such a theory as a product-preserving functor to another category with finite products.

John Baez (Jul 11 2023 at 14:55):

At the time some logicians complained that Lawvere didn't understand the difference between syntax and semantics!

John Baez (Jul 11 2023 at 14:55):

Anyway, we talk about both kinds of boolean algebras in our discussion, for precisely this reason.

Josselin Poiret (Jul 12 2023 at 08:13):

if I may add: syntax is semantics, most of the time the freely generated one!

Fernando Chu (Jul 12 2023 at 15:18):

Josselin Poiret said:

if I may add: syntax is semantics, most of the time the freely generated one!

Just wondering, are there cases were it is not the freely generated one?

Jencel Panic (Jul 12 2023 at 20:32):

@Simon Burton Please share some of those diagrams here if you get around to drawing them, I, personally, always have a hard time understanding such concepts without looking at examples.

Gabriel Goren Roig (Nov 12 2023 at 02:00):

John Baez said:

And I'm just wondering, how exactly do these adjoints capture (existential) quantification?

My blog series with Michael Weiss might help:

• First-order categorical logic.

We use a rather old-fashioned concept of 'hyperdoctrine', which starts out being a functor from the category FinSet of finite sets to the category BoolAlg of boolean algebras and order-preserving maps. So, any function gives such a map between Boolean algebras, and in Part 3 we figure out/explain how the adjoints of this map correspond to quantifiers. But maybe you already understand that by now and are trying to figure out something else, like how 'closure operators' come into the game.

I've read that blogpost series and wished it hadn't come to a premature end :smiling_face_with_tear:

I'm curious, why do you say hyperdoctrines are an old-fashioned concept?

John Baez (Nov 12 2023 at 09:41):

I'm sorry... I got busy with something else.

I got the feeling that category theorists consider hyperdoctrines less interesting than more fully "typed" approaches to categorical logic, which use other formalisms. Hyperdoctrines - at least the ones I was talking about - are a nice categorical formalization of untyped first-order logic.

John Baez (Nov 12 2023 at 09:43):

Part of the reason for my feeling was that I wasn't seeing any modern papers on hyperdoctrines! But now, maybe due to this thread, I've discovered that modern papers on hyperdoctrines call them "doctrines". This came as a big surprise to me, especially since "doctrines" also means something else in categorical logic.

Todd Trimble (Nov 12 2023 at 12:30):

Hyperdoctrines can be just as typed as you wish. Here the choice of FinSet as the domain of the hyperdoctrine could be what's "old-fashioned": this is the opposite of the free category with finite products generated by a single type, so this is a unityped or untyped version. But the base $B$ of the hyperdoctrine $B^{op} \to Cat$ can be lots of things.

John Baez (Nov 12 2023 at 17:48):

What I was referring to was the inability to form new types as limits, etc. of existing ones. So e.g. you can write down the axioms for a group in untyped first-order logic but not define a type of groups.

John Baez (Nov 12 2023 at 17:52):

Anyway, if there's some other reason why there's so little work on hyperdoctrines I'd like to know it. I'd been wanting to use them as a bridge between traditional model theory and categorical logic but (unsurprisingly) didn't have the energy × technical skill to go very far.

Evan Patterson (Nov 12 2023 at 20:32):

I share your impression that hyperdoctrines have gotten less attention than other ideas in categorical logc---are they even mentioned in The Elephant?---but there is a small but active group of people working on them. They recently had a Workshop on Doctrines and Fibrations, where "doctrine" seems to be shorthand for "hyperdoctrine" as discussed earlier. Notably, a group of Italians (Rosolini, Maietti, Trotta, maybe others) have been writing a bunch of papers about hyperdoctrines.

John Baez (Nov 12 2023 at 23:09):

Yes, I was very excited to see a paper on Henkin's theorem for (hyper)doctrines since that's heading in the direction of using them to understand ordinary first-order logic more deeply.

John Baez (Nov 12 2023 at 23:15):

This paper should imply some sort of version of Goedel's completeness theorem for (boolean?) hyperdoctrines, but I don't know if they work that out.

Simon Burton (Nov 13 2023 at 00:34):

I was getting the sense that Lawvere's work on hyperdoctrines evolved into his work on topos theory. Is that at all true, or have i filed these two subjects erroneously ?

Jonas Frey (Nov 13 2023 at 03:18):

Since nobody else has brought it up: hyperdoctrines, specifically triposes play a crucial role in the construction of realizability toposes. The reason that's not in the elephant is that it's supposed to be in the third volume.

Kevin Arlin (Nov 13 2023 at 04:13):

Ooh, that's very helpful, I've seen the word tripos a number of times but never read the definition so I had no idea that a tripos is a hyperdoctrine.

Jonas Frey (Nov 13 2023 at 04:41):

I spent a lot of time working on triposes, so I'd be happy to answer any questions :-)

Gabriel Goren Roig (Nov 13 2023 at 14:30):

Great to know that hyperdoctrines are now sometimes called doctrines, I wouldn't have known how to identify this new work. Thanks @John Baez @Evan Patterson !

Todd Trimble (Nov 13 2023 at 15:08):

Simon, as far as I know, Lawvere never mentioned that hyperdoctrines was one of the things leading to his work on elementary toposes.

Todd Trimble (Nov 13 2023 at 15:08):

In his book Variable Sets, Etendue, and Variable Structure in Topoi, he mentions I think five different streams that were current in and around the year 1963, which stimulated and were later unified by the work he did with Tierney. I don't have the book in front of me, so I'm trying to remember them. One was the theory of Grothendieck toposes. He also cites Cohen's work on the continuum hypothesis, and I believe also Robinson's work on nonstandard analysis, and finally I think his Elementary Theory of the Category of Sets which he prepared for classes he would be teaching at Reed College. I'm drawing a blank on what the fifth may have been.

Todd Trimble (Nov 13 2023 at 15:08):

Hyperdoctrines are an (elegant, IMO) formalism he devised for doing predicate calculus. Typically the base category $B$ can be thought of as a category of types (objects) and terms in context (morphisms), and the hyperdoctrine itself is a functor $B^{op} \to Cat$ which assigns to each object or type the category (often a Boolean or Heyting algebra) of "predicates" or "attributes" of that type. But, he being Lawvere, he jolly well knew that the same formalism would handle lots of other things not ordinarily thought of in the same breath as predicate calculus. For example, the base category $B$ could be the category of groups or of groupoids, and the hyperdoctrine assigns to the group its category of representations (of whatever sort: permutation, linear, etc.).

Evan Patterson (Nov 13 2023 at 18:02):

Here's a link to the notes you reference: https://github.com/mattearnshaw/lawvere/blob/master/pdfs/1975-variable-sets-etendu-and-variable-structure-in-topoi.pdf

Todd Trimble (Nov 13 2023 at 18:24):

Ah, many thanks, Evan. I'll keep this in mind, Matt Earnshaw's site, next time I'm looking for a hard-to-find Lawvere paper.

Todd Trimble (Nov 13 2023 at 18:26):

And so the fifth contributing mathematical stream that I couldn't think of in my reply to Simon was: Kripke's semantics for intuitionistic predicate calculus.

Simon Burton (Nov 16 2023 at 07:30):

Thanks for that summary Todd. The original reason for starting this thread was Joshua Wrigley's neat picture of a doctrine (=hyperdoctrine): it looks to me remarkably like Pascal's triangle, in it's combinatorial (bijective) form, but Joshua's diagram is sideways of course. I think there is a way of expressing Pascal's triangle using categories of GSets, where G ranges over the symmetric groups, and the bijections become various functors. So the idea was that hyperdoctrines would be a nice way of unifying these two ideas, and much more. I have a whole menagerie of weird and wonderful Pascal triangle variants that i would like to understand better.