The n-Category Café

One talk that I particularly enjoyed was John Bourke’s. He’s found a way to use F-categories to formulate a 2-dimensional “monadicity theorem” which includes lax and oplax morphisms as well as strict and pseudo ones. This further justifies Steve’s and my claim that $\mathcal{F}$-categories are a natural context in which to talk about 2-monads.

As it happens, doctrinal adjunction becomes one of the defining properties of a monadic $\mathcal{F}$-functor, similar to conservativity and creation of split coequalizers in the traditional case. The others are that the forgetful functor is locally an isofibration (i.e. any morphism which is isomorphic to a lax (or pseudo or oplax) morphism has a unique compatible such structure) and reflects identity-ness of 2-cells.

This is one of those things that when you see it, you think (or at least I did) “why on Earth hasn’t someone done this before?” As John pointed out, in ordinary monad theory, Beck’s monadicity theorem lets us say that (for instance) the category of groups is monadic over sets without knowing anything about the “free group” functor other than that it exists. In 2-monad theory, we had the strict $Cat$-enriched monadicity theorem to tell us about strict algebras and strict morphisms, and a bicategorical monadicity theorem to tell us about pseudo algebras and pseudo morphisms, but in order to identify (say) lax monoidal functors with lax $T$-morphisms, where $T$ is the monad induced on $Cat$ by the forgetful functor from $MonCat$ and its left adjoint, we needed to compute $T$ very carefully! This is kind of a barrier to working with 2-monads in practice, since left adjoints to forgetful functors are often quite hairy to construct. John’s 2-dimensional monadicity theorem solves this problem.

Mike Stay’s subject of compact closed bicategories was also close to my heart, although I don’t have much to say about it. We’ve talked about presenting “theories with duality” once or twice over two years ago. Mike described the “free compact closed bicategory on a symmetric-monoidal-closed object”, using some pretty but intricate pictures.

Eugenia Cheng’s talk was also related to duality, but in a different way. Ordinary adjunctions are something we can talk about internal to any 2-category, but they give rise to a mates correspondence which is most naturally described using double categories. Multi-variable adjunctions are something we can talk about internal to a compact closed bicategory (or proarrow equipment, or extraordinary 2-multicategory, etc.). But they also give rise to a “parametrized mates” correspondence, which is most naturally described using something that Eugenia (describing joint work with Nick Gurski and Emily Riehl) called a cyclic double multicategory. What on earth is that?

In the double category that we use to talk about ordinary mates, the vertical morphisms are adjoint pairs. In a multivariable version of this, the vertical morphisms should therefore be multivariable adjunctions. A two-variable adjunction from $(C,D)$ to $E$ is usually described using three functors looking like this: $$\begin{aligned} \otimes :& C \times D \to E \\ hom_l :& C^{op} \times E \to D \\ hom_r :& D^{op} \times E \to C \end{aligned}$$ but EGR realized that it looks a lot more symmetric if you write $F=E^{op}$, since then we have functors: $$\begin{aligned} \otimes :& C \times D \to F^{op} \\ hom_l^{op} :& F \times C \to D^{op} \\ hom_r^{op} :& D \times F \to C^{op} \end{aligned}$$ We also switched the order of the inputs to $hom_l^{op}$, so as to make the cyclic ordering of the objects be preserved in all three cases. Thus, the “vertical part” of this double-category-like structure should contain “morphisms” indexed by cyclically ordered $n$-tuples of objects. Once you make that precise (a “cyclic multicategory”) you can just define a cyclic double multicategory to be an internal category in cyclic multicategories.

Eugenia also mentioned a subtle issue that I don’t fully understand. It turns out to be kind of tricky to make precise what you mean by “morphisms indexed by cyclically ordered tuples of objects”. The way that EGR did it is to consider instead morphisms indexed by an ordered tuple of inputs and a single output, but with an action of cyclic groups. That is, given a morphism in $Hom(a,b,c \,;\, d^{op})$, we can act on it cyclically to obtain morphisms in $Hom(b,c,d \,;\, a^{op})$, $Hom(c,d,a \,;\, b^{op})$, and $Hom(d,a,b \,;\, c^{op})$.

Note that we need an involution $(-)^{op}$ on objects here. This is true even if you take more literally the idea of “morphisms indexed by cyclically ordered tuples of objects”, since in order to “compose” two of these morphisms along an object $a$, you need to be able to specify that $a$ is part of the “domain” of one morphism and the “codomain” of the other. With only a cyclically ordered list of objects, the only way to do that is to have it appear “opped” in one list but not the other.

It may seem at first glance as though the two ways of describing cyclic multicategories should be equivalent, once you figure out how to make them both precise. But no — the one with cyclic group actions seems to be more expressive, because the group actions don’t have to be free. The other description can apparently only describe versions where the action is free.

While writing this post, it just occurred to me that this issue already comes up in the single-variable case! The vertical category whose morphisms from $a$ to $b$ are adjoint pairs $a\rightleftarrows b$ also has an involution $(-)^{op}$, and an adjoint pair $a\rightleftarrows b$ yields equivalently an adjoint pair $b^{op}\rightleftarrows a^{op}$ (passing to opposite categories switches which functor is the left and which the right adjoint). And we can also have non-free actions here: if it should happen that $b = a^{op}$, then we can ask whether an adjoint pair $a\rightleftarrows a^{op}$ is fixed by the involution. If so, what we have is a contravariant endofunctor which is “adjoint to itself on the right”, i.e. we have isomorphisms $Hom(x,F(y)) \cong Hom(y,F(x))$. For instance, the powerset functor has this property. Perhaps Eugenia, Nick, and Emily have already thought about this.

There were many other nice talks: Nick spoke about the Gray tensor product, Tom about the eventual image, and I talked about cardinalities and Euler characteristics. I’ll blog about the latter some day (hopefully soon) when the paper is finished. But the only other one I want to say anything about right now is Benno van den Berg’s.

The notion of “elementary topos” is considered “impredicative” in that it contains subobject classifiers. Various people have proposed “predicative” versions of it, but none of them have ever been really satisfactory. For one thing, since the notion of “Grothendieck topos” makes perfect sense predicatively, you’d like your “predicative elementary toposes” to be closed under constructions like sheaves — but this turns out to be kind of tricky to do predicatively.

Benno (describing joint work with Ieke Moerdijk, which has now appeared) proposed that a predicative topos should be a Pi-W-pretopos (a fairly standard thing to ask) which also satisfies the internal version of the axiom WISC. (They also propose to call WISC the “axiom of multiple choice”, replacing the axiom previously known by that name and now to be called “strong AMC”, since it implies WISC but seems just a bit stronger. I don’t think I have strong feelings about that either way.) WISC turns out to be “just enough choice” to deduce closure under sheaves and realizability, as well as ex/lex completion (which ordinary elementary toposes are not closed under).

Of course, WISC has the disadvantage that not all elementary toposes satisfy it, so not every elementary topos would be a predicative topos (although since WISC is preserved by sheaves, every Grothendieck topos over a classical version of Set will be). Benno took the radical point of view that that means something is not quite right with the definition of elementary topos!

I’m actually in sympathy with that: the main problem I have with elementary toposes (which Benno also emphasized) is that they don’t admit all sorts of free/inductive/recursive constructions. They do automatically have W-types (at least, as soon as they have a natural numbers object), but in a way that’s sort of an accident. Having W-types bascially means having free algebras for “free” algebraic theories, but elementary toposes don’t necessarily have free algebras for arbitrary algebraic theories.

In fact, Benno mentioned a theorem of Andreas Blass that free algebras for arbitrary algebraic theories cannot even be constructed in ZF! (The problem is that you want to first build a set of all words in the operations of the theory, then quotient by all the relations of the theory, but it’s not clear how to make the operations act on the resulting quotient unless you have a choice principle to “lift” the inputs back to the set of words.) Surely something is wrong with a foundation for mathematics in which not all algebraic theories have free algebras. (-:

Personally, while I like WISC, I would prefer not to have to include any sort of choice principle in a foundational system intended as “constructive”. (I know that many “constructivists” would disagree, being fond of even stronger choice principles such as COSHEP, which are not even valid in every Grothendieck topos over ZFC.) I would prefer something like higher inductive types which are a natural generalization of W-types. Of course, they were originally motivated by $\infty$-considerations, but they make perfect sense even in a traditional set-based foundational system; in that case, what they essentially allow us to do is to inductively define a set and quotient it by an equivalence relation at the same time. This is sufficient to construct free algebras, and also to do things like sheafification.

The paper on HITs that Peter Lumsdaine and I are writing intends to show how to construct HITs in Grothendieck $(\infty,1)$-toposes over a classical foundation of ZFC. Blass’ result implies that ZF is insufficient, but we conjecture that WISC (plus ordinary W-types) suffices (and we have a general idea of how the proof will go—we’re also currently writing another paper about that sort of thing). I am also tempted to conjecture that $\Pi W$-pretoposes with HITs are stable under constructions like sheaves and realizability. If so, maybe they could also be a notion of “predicative elementary topos” — one which might generalize more directly to “predicative elementary $(\infty,1)$-toposes”. (Okay, I lied: cf. the last slide of my Swansea talks.)

I should also mention another possibly contentious issue: in contrast to Benno’s talk at the PSSL, their paper on the arXiv works in the context of “algebraic set theory”, i.e. with a “category of classes” rather than merely a topos-like “category of sets”. Benno says that this isn’t essential, though, and that there may be a second paper that works only with a topos-like category.

Relatedly, one might also be tempted to include the existence of “universes” in a notion of predicative topos — this is certainly natural from the $(\infty,1)$-point of view (cf. object classifiers and the univalence axiom). Benno expressed a dislike for universes as a foundational assumption; my own feeling about them seems to vacillate with the phase of the moon. One thing that universes give you is what type theorists call large elims: the ability to define sets recursively. For instance, in an elementary topos with NNO (even one satisfying full AC) one can’t in general define the $\mathbb{N}$-indexed family of iterated power-objects $P^n(X)$ of an object $X$. One can consider allowing large elims directly, but universes (especially univalent ones) are a very convenient way to obtain them.

Regardless, it’s nice to see WISC finally getting some attention!