Hyperdoctrines and Contravariance

Question

I've been reading through the extremely useful discussion of First-Order Categorial Logic that recently popped up over at The Diagonal Argument. But when I compare Baez and Weiss's construction to what's found over at the nLab, one striking difference is that where B&W build a covariant functor from FinSet (the category of finite sets with functions between them) to Bool (the category of boolean algebras) the nLab suggests hyperdoctrines will in general be contravariant functors.

Here are five ways I might explain this difference:

1. B&W messed something up.
2. the nLab folks have messed something up
3. this is one of those weird facts that make classical logic funky, and it wouldn't matter if we used FinSet or FinSet$^{op}$, the result would be the same.
4. B&W simplified some things, and this is one of the consequences of the simplification
5. Something else entirely.

My question: which of these is to blame and, if it's number 5, can you elaborate at all? (2) seems unlikely, since all the publications cited by the nLab folks also assume contravariance. But I felt obligated to include it for completeness sake.

Answer 1

I'm sure Kevin's answer is correct, but here's some additional stuff to chew on from someone whose understanding of this is more about type theory and computer science.

I think the answer is that it's actually a hyperdoctrine on $\mathbf{FinSet}^{op}$. A reason this might be the case is that this category arises naturally when modelling variable binding, which is something you might want to study categorically in the fields above. The way you might go about this is as follows:

We want a category for talking about variables bound in a context. The variables will all just range over a single universe of discourse, rather than having possibly distinct types. So, we will accomplish this by taking a Cartesian category freely generated by one object $U$. $1$ is the empty context, $U$ is a 1-variable context, $U×U$ is a 2-variable context, and $U^n$ is an $n$-variable context. A map $U^m → U^n$ decomposes into $n$ projections from $U^m$, saying how each of the $n$ variables in the result is bound in the $U^m$ context. You can think of this like:

$$x_1, x_2, ..., x_n ⊢ x_i, x_j, x_j,...,x_k$$

expressing some kind of simultaneous substitution of variables with contraction, weakening and exchange. Now, presheaves on this category can be used for talking about algebras with variable binding.

But, consider what I mentioned about the maps. A map $f : U^m → U^n$ is equivalent to for each $i < n$ a specification of which projection $π_j : U^m → U$ is used. Another way to look at this is that we have a function $[n] → [m]$ specifying this information ($[n]$ being a finite set of size $n$). So, the context category we built is equivalent to $\mathbf{FinSet}^{op}$, and presheaves/hyperdoctrines on it are functors out of $\mathbf{FinSet}$.

If you want a more thorough explanation of the variable binding stuff, see here.

Answer 2

(This answer is basically the same as Dan Doel's. We wrote them in parallel, but he posted first. I decided this may still be helpful.)

Unsurprisingly, no one's wrong.

In the nLab article for hyperdoctrines, it talks about "contexts" and classical logic being the case where $T$ is a "category of contexts". For something like first-order logic, what we call the "context" has two parts, usually left implicit. There's a variable context that tells us which free variables are allowed and what their sorts are, and then there are the assumptions. I'm going to focus on the variable contexts, though in some cases these things mix together. As an example, imagine a multi-sorted theory of vector spaces. If we want to say $r(\mathbf v+\mathbf u)=r\mathbf v+r\mathbf u$ we need to specify that $r$ is a scalar, and $\mathbf v$ and $\mathbf u$ are vectors. We could write this like: $r:S,\mathbf v:V,\mathbf u:V\vdash r(\mathbf v+\mathbf u)=r\mathbf v+r\mathbf u$, where $S$ and $V$ are the two sorts of our theory.

The question now is how do we represent variable contexts. The most obvious choice is to think of them like tuples of sorts. We can drop the variable names and just use their positions, giving us something like an object like $S\times V\times V$ identifying the variable context for the above formula. If we want to "forget" the scalar, we can use the projection $S\times V\times V\to V\times V$. When we use a functor to map this category, which we can define to be the category with finite products freely generated by a set of objects (which represent the sorts), we find that it should be contravariant. It's not clear how to turn a formula like $r(\mathbf v+\mathbf u)=r\mathbf v+r\mathbf u$ into one that doesn't have $r$ free, but it's clear how to turn a formula like $\mathbf u+\mathbf v=\mathbf v+\mathbf u$ into one that does have $r$ free. As another example, given the diagonal $V\to V\times V$, we can turn a formula with two variables free, e.g. $\mathbf u-\mathbf v = 0$, into a formula with one variable free, i.e. $\mathbf u-\mathbf u=0$.

Now, in the single-sorted case, we can simplify notation by writing $S\times S$ as $S^2$ and so forth. The diagonal arrow $S\to S^2$ can then be described via $S^{!_2}$ which is the pre-composition of $S$ with $!_2 : 2\to 1$ in the category $\mathbf{FinOrd}$. ($\mathbf{FinOrd}$ is the skeleton of $\mathbf{FinSet}$ and thus they are equivalent.) In other words, we have a contravariant functor $\mathbf{FinOrd}$ to $T$. In fact, $\mathbf{FinOrd}$ is the category with finite coproducts freely generated by a single object. In other words, if we define $T$ to be, in the single-sorted case, the category with finite products freely generated by a single object, then $T\simeq\mathbf{FinOrd}^{op}$. This is basically what Baez is doing. He chooses $T=\mathbf{FinSet}^{op}$ producing $T^{op}\to\mathbf C$ or $\mathbf{FinSet}\to\mathbf C$.

Answer 3

Baez and Weiss are talking about something Baez is calling "polyadic Boolean algebras", which are functors from $\mathbf{FinSet}\to\mathbf{Bool}$, for instance, $n\mapsto \mathcal{P}(V^n)=\mathbf{Set}(V^n,\{0,1\})$ for a fixed set $V$. This is covariant since a function $f:n\to m$ induces a function $V^f:V^m\to V^n$, which then induces the pullback function $\mathcal{P}(V^f):\mathcal{P}(V^n)\to \mathcal{P}(V^m)$. There is a closely related hyperdoctrine $\mathcal P:\mathbf{Set}^{\mathrm{op}}\to \mathbf{Bool}$ which is just $\mathcal P$ itself, but these aren't trying to talk about quite the same thing.