The n-Category Café

First, Dana Scott talked about models for modal logic. He started by recalling the definition of a complete frame-valued set, an alternate way to construct the category of sheaves on a locale. Then he proposed to replace the frame (= complete Heyting algebra) by a complete Lewis algebra: a complete lattice $L$ equipped with a lex comonad $\Box$ (that is, $\Box 1 = 1$, $\Box\Box x = \Box x \le x$, and $\Box(x\wedge y)=\Box x \wedge \Box y$). With this he defined an intensional map of complete $L$-sets to be a function $f$ which preserves extents $|f x|=|x|$ and such that $\Box [x=y] \le [f x = f y]$. I guess this means that it only preserves “necessary” or “definitional” equality rather than “contingent” or “extensional” equality as the condition $[x=y]\le [f x = f x]$ would require. This defines a supercategory of the category of sheaves on $L$, and one can then investigate and attempt to axiomatize its properties as a “modal version of a topos.”

Then Richard Garner talked about topological models of type theory. It looks like type theory has come up a few times in passing on the nCafe but never been discussed in detail, so I thought it would be worthwhile writing a brief introduction. But rather than posting it here, I decided to put it over at the nLab. So go read that and then come back here.

Back? Okay, one thing I didn’t mention about the “propositions as types” paradigm (although someone may have added it by the time you read this) is that it gets a bit subtle when you start thinking about equality. In typed predicate logic, equality is given by a particular proposition $x=_A y$ for two variables $x,y$ of type $A$. Semantically this is usually modeled by an equalizer. In dependent type theory, instead of a proposition $x=_A y$ we have an identity type $Id_A(x,y)$, which you can think of as the “type of all proofs that $x=_A y$.” Of course, if $x=y$ there may be many proofs of that fact, so $Id_A(x,y)$ may not be a subobject of $A\times A$.

If $Id_A(x,y)$ is inhabited (there exists a term $p$ of type $Id_A(x,y)$) we say that $x$ and $y$ are propositionally equal with $p$ as witness. The rules for manipulating identity types ensure that equality is transitive, reflexive, and symmetric: for instance, we have a term $$Id_A(b,c)\times Id_A(a,b) \to Id_A(a,c).$$ and a term $$Id_A(a,b) \to Id_A(b,a)$$ and a term $1_a$ of type $Id_A(a,a)$.

Now obviously, $Id_A$ is a groupoid, just as the proposition $x=_A y$ is an equivalence relation. Well, not quite—it’s a groupoid up to propositional equality! The composition is associative, unital, and has inverses, but only up to propositional equality. You shouldn’t have any trouble guessing that in fact, we have an infinity-groupoid $$A \leftleftarrows Id_A \leftleftarrows Id_{Id_A}\leftleftarrows \cdots.$$ This was apparently observed simultaneously by Garner-van den Berg and by Peter Lumsdaine. By applying the homotopy hypothesis, we conclude that the semantics of propositions-as-types type theory should really happen in topological spaces (or some other equivalent model), with propositional equality modeled by homotopy.

To make this precise, Richard suggested to consider, as a model of dependent type theory, a category $C$ equipped with a nice weak factorization system $(L,R)$. A dependent type $B(x)$ with $x\in A$ represents a map $B\to A$ which is moreover required to be in $R$; we think of it as a sort of “fibration.” And the identity type $Id_A$ represents a path object of $A$, given by the $(L,R)$-factorization of the diagonal $A\to A\times A$. There are a couple subtleties required to make this work. In particular, you need to assume that the pullback of an $L$-map along an $R$-map is again an $L$-map; this “Frobenius property” “makes the identity types parametrizable.” This is satisfied by the (trivial cofibration, fibration) wfs for the folk model structure on groupoids, which reproduces a model of type theory due to Streicher and Hoffman, but not for the (trivial cofibration, fibration) wfs for the Hurewicz model structure on $Top$ unless we use Moore paths (paths of arbitrary nonnegative real length) instead of the usual paths of length 1. One can also try to emulate Moore paths in the simplicial world.

A couple people talked about other aspects of type theory and logic, but the next talk that I understood was by Oliva Caramello, who showed that subtoposes of the classifying topos of a geometric theory are in bijective correspondence with quotients of the theory (theories with the same signature which can prove at least as much). You can then look for correspondences between topos-theoretic properties of subtoposes (open, closed, quasi-closed) and logical properties of the corresponding theories.

Then Nick Duncan talked about the difference between gros and petit toposes, which is a subject that came up here recently. He said that intuitively, the difference is that

• A gros topos is a topos whose objects have geometrical structure, such as simplicial sets or sheaves on a full subcategory of $Top$, while

• A petit topos is a topos constructed from a single geometric object, such as sheaves on a single topological space, or $G$-sets for some group $G$.

Nick argued that taken separately, these notions are fairly vacuous. For example, there are well-known “representation theorems” saying that any (Grothendieck) topos is equivalent to the category of sheaves on a localic groupoid (a groupoid internal to the category of locales) — which is surely a single geometric object. The important thing is the relationship between a gros topos and the petit toposes corresponding to its objects.

Nick presented the following tentative definition: a gros topos is a topos $G$ equipped with, for every object $F\in G$, a topos $P(F)$ called the petit topos of $F$ and a local geometric morphism $p_F: G/F \to P(F)$, and for every $g:F\to H$ in $G$, a geometric morphism $P(g):P(F)\to P(H)$ and various commutativity relationships, presumably including coherence isomorphisms.

(A geometric morphism is local if its direct image $p_*$ has a right adjoint $p^!$.
Then $(p_\star, p^!)$ is also a geometric morphism, which exhibits $P(F)$ as a subtopos of $G/F$, and $P(F)$ and $G/F$ are “homotopy equivalent” and have the same cohomology.)

We call the topos $P(1)$ the topos of points of $G$; since $G/1\simeq G$ we have $p = p_1:G \to P(1)$. Objects of the form $p^*(A)$ are called discrete, and objects of the form $p^!(A)$ are called codiscrete. I believe that $P(1)$ is supposed to function as something like “the topos of sets relative to $G$.”

The canoncial example is the Zariski topos $k Zar$ over a field $K$: the topos of sheaves on the cosite of $k$-algebras with coverage consisting of the finite families $\{A\to A[a_i^{-1}]\}$ where $(a_1,\dots,a_n)=1$. For any $k$-algebra $A$, we define $P(A) = Sh(Spec A)$. For an arbitrary object $F$ in $k Zar$, we write $F$ as the colimit of representables, let $|F|$ be the topological space obtained as the corresponding colimit of Zariski spectra, and let $P(F)= Sh(|F|)$. There is a functor $O:k Alg \to Set$ that takes a $k$-algebra to its underlying set, and for any $F$ in $k Zar$ we can pull back $O$ to $k Zar/F$ and then restrict to $P(F)$ to obtain a structure sheaf $O_F \in Sh(|F|)$ making $|F|$ into a locally ringed space (and $Sh(|F|)$ a locally ringed topos).

Toby Kenney talked about the “free diad” using graphical calculus, in the same way that the algebraic simplex category $\Delta_+$ gives the free monad. A diad is a structure that simultaneously generalizes a monad and a comonad; it’s a functor $T$ with natural transformations $\alpha:T\to T T$ and $\beta: T T \to T$ satisfying certain axioms. A monad $(T,\mu,\eta)$ gives rise to two diads, one with $\alpha = \eta T$ and $\beta = \mu$, and one with $\alpha = T \eta$ and $\beta = \mu$. A comonad likewise gives rise to two diads. It turns out that one can define both a category of dialgebras and a di-Kleisli category for any diad, and when applied to the diads coming from a monad or comonad one can recover the usual categories of algebras and Kleisli categories. Also, if $T$ is any idempotent functor ($T \cong T T$), then $\alpha = \beta^{-1}$ is a diad, and if $T$ is any diad, then $T T$ can be made into a diad as well.

One other thing worth mentioning is that if $T$ is any finite-limit-preserving diad on a topos which is “distributive” (an extra axiom relating $\alpha$ and $\beta$), then its category of distributive dialgebras is again a topos. This unifies the two classical theorems that the category of coalgebras for a lex comonad on a topos, and the category of algebras for a lex idempotent monad on a topos, are again toposes. It feels quite similar to Todd’s three topos theorems in one, but Toby and I were unable to work out a very precise connection.

Pino Rosolini told us about a construction of an extension of the effective topos. The effective topos $Eff$ is a topos in which “everything is computable,” although you have to interpret that suitably broadly. It includes $Set$ as a full subcategory, so not everything can be computable; however, the natural numbers object $N$ is not the one coming from $Set$, and every function $N\to N$ is in fact computable. Moreover, you can look at all the objects “built from” $N$, called modest sets, and all the maps between them will be computable.

Furthermore, it turns out that the modest sets form an internal category $PER$ in $Eff$, and that internal category is complete. So while it’s true in $Set$ that any small complete category must be a poset, this is not true in $Eff$. However, making this precise involves comparing the “externalization” of $PER$ with the fibration of modest sets, and these aren’t as equivalent as you might like; rather the latter is the stackification of the former. Pino’s talk was about a construction of a topos $\mathcal{F}$, which logically extends $Eff$, and which contains a internal category which is strongly equivalent to the complete fibration of modest sets.

John Power’s talk about generalized Lawvere theories began with a calculatedly inflammatory statement: the emphasis on monads to understand universal algebra is the single worst mistake in the history of category theory. His claim: Lawvere theories are much better. Why? He listed a few reasons.

• The coproduct of Lawvere theories always exists; not so for monads.

• The tensor product of Lawvere theories always exists; not so for monads.

• Calculating a monad from generators and relations is a nightmare, but it is easy and natural with a Lawvere theory.

• Lawvere theories are also a natural beginning to categorical logic: they are finite-product theories, from which we can move up to finite-limit theories, finite limit and finite sum theories, geometric theories, and so on.

Monads are interesting and useful (said John), but for purposes of universal algebra, Lawvere theories are better. (Note that changing “finite” to a bound of any other cardinality is a trivial variation. It’s only monads having “operations” of potentially arbitrarily large arities, like the monads whose algebras are complete lattices or compact Hausdorff spaces, which don’t fit the Lawvere theory framework.)

However, while one can talk about monads on any category (and in fact, in any 2-category), to talk about Lawvere theories one needs a notion of “size.” John proposed the following framework: if $C$ is a locally finitely presentable category, a Lawvere $C$-theory is a category $L$ and a functor $J:C_f^{op}\to L$ that preserves finite limits. Here $C_f$ is (a skeleton of) the category of finitely presentable objects in $C$. Then a model of $L$ is a functor $M:L\to Set$ such that $M J$ preserves finite limits (and hence is representable by an object of $C$). Theorem: Lawvere $C$-theories, thusly defined, are equivalent to finitary monads on $C$ (those that preserve filtered colimits).

(My personal take on the question: a monad represents the extensional essence of an algebraic theory, and it’s important to keep in mind both this essence as well as any particularly convenient presentations of it that may exist. There are many such situations where we need to think about one object as a “presentation” of another one, the presentation being non-canonical and not always existing, but easier to construct and manipulate when it does. For example, topological spaces present homotopy types, model categories present $(\infty,1)$-categories, sites present topoi, and even group presentations present groups!)

Bill Lawvere then ended the first day by discussing some open problems in topos theory, relating in particular to what he called “quotient toposes” (a stronger notion than just a “surjective” geometric morphism).

The next day, Michael Fourman started off by talking about ways to represent quantales using relations in a presheaf topos. Given a quantale, you can write down a geometric theory describing it as relations, and then in the resulting classifying topos there will be an internal collection of relations representing that quantale.

Ieke Moerdijk gave a nice talk about generalized Reedy categories (“greedy categories?”). I thought that Reedy categories deserved a page on the nLab, so I made one, including a brief summary of the generalization Ieke presented.

Nicola Gambino’s talk on monads in double categories was dear to my heart because he started off by giving the definition of a framed bicategory. He then proceeded to consider a (horizontal) monads in such, but forming a different framed bicategory $Mnd(C)$ than the one $Mod(C)$ that I studied. Nicola (and Tom Fiore and Joachim Kock) are interested instead in a framed version of the 2-category $Mnd(K)$ used in Street’s “Formal theory of monads,” where a morphism from a monad $s:A\to A$ to a monad $t:B\to B$ consists of a morphism $f:A\to B$ and a 2-cell $\phi:t f \to f s$ satisfying exactly the axioms necessary for $f$ to lift to a functor from $s$-algebras to $t$-algebras. Nicola then stated a theorem that if $C$ is a framed bicategory, so is $Mnd(C)$. The point was to use the framed structure to make it easier to construct free monads on endofunctors.

The motivating example was polynomial endofunctors, which happen in a generalization of the framed bicategory of spans. Let $E$ be a locally cartesian closed category; then we have a framed bicategory whose objects and vertical morphisms are those of $E$, and in which a horizontal arrow $I\to J$ is a diagram $$I \overset{s}{\leftarrow} B \overset{f}{\to} A \overset{t}{\to} J.$$ We view this as a “presentation” of the polynomial functor $E/I\to E/J$ defined by $\Sigma_t \Pi_f s^*$. When $J=I$ this is intended to be thought of as a “many-sorted signature:” $I$ is the set of sorts, $A$ is the set of operations, $t$ assigns the target sort of each operation, the fiber $B_a$ is the arity of the operation $a\in A$, and $s$ assigns a sort to each input. A monad in this framed bicategory is then a polynomial monad, and Nicola stated a theorem that if $E$ has initial algebras for all these functors, then it admits the construction of free monads.

Dominic Verity then gave a brief tour of the “simplicial approach” to (nerves of) weak $\omega$-categories, which involves defining the simplicial nerve of a strict $\omega$-category, characterizing the things that arise as such nerves, and then weakening the conditions. This was the very first definition of weak $\omega$-category, proposed by Ross Street back in the dark ages, and has since been carried forward, also by Street and others but especially by Dominic.

The idea is, as you probably know, to define the free strict $\omega$-category on an $n$-simplex and use that to define the nerve $Str\omega Cat\to sSet$. But (unlike for 1-categories and $(\infty,1)$-categories) we can’t expect that functor to be full and faithful; we need to remember which simplices are identities. A collection of simplices, called thin and thought of as being identities (or equivalences), is called a stratification on a simplicial set. The nerve of strict $\omega$-categories is fully faithful to stratified simplicial sets and we can characterize its full image by certain unique horn-filling conditions.

In the strict case, you can’t get rid of this extra structure; one can construct simplicial sets having many different stratifications that correspond to many different $\omega$-categories. For instance, let $M$ be a monoid, regarded as a chaotic monoidal category (all objects uniquely isomorphic), and deloop it to get a 2-category $B M$. Then its simplicial nerve $N(B M)$ is 1-coskeletal, which means that an isomorphism $N(B M_1) \cong N(B M_2)$ is just an isomorphism of pointed sets. So you just need to find a set admitting two different monoid structures.

The stratified simplicial sets arising as nerves of strict $\omega$-categories are called complicial sets. If we simply relax the uniqueness of the horn filler (now thinking of thin elements as “equivalences” rather than identities), we get the notion of weak complicial set. But these are not quite yet a notion of weak $\omega$-category, since they might not have enough thin elements. This is clear when you observe that the category of weak complicial sets contains the category of complicial sets, and hence the category of strict $\omega$-categories and strict $\omega$-functors, as a full subcategory; whereas while we can certainly regard a strict $\omega$-category as a weak one, we want to see all the weak functors as well.

One natural thing to do now is to “saturate” our weak complicial sets so that “everything that should be thin is.” This turns out to involve some more difficult combinatorics, but the upshot is that it’s possible. (The proof actually involves showing that weak complicial sets are equivalent to categories enriched in weak complicial sets, the same way that quasi-categories are equivalent to simplicially enriched categories.) So we can think of a weak complicial set as a “presentation” of a weak $\omega$-category, where we’ve noticed enough internal equivalences to show that it is a weak $\omega$-category, but perhaps we haven’t noticed all the equivalences. This is very analogous to the “completion” process applied to Segal spaces.

However, it’s not yet clear to what extent the stratification can be dispensed with entirely. Dominic mentioned some partial results:

• A simplicial set can have no more than one stratification which is a saturated 2-trivial weak complicial set (everything is thin above dimension 2).

• Given a saturated $n$-trivial weak complicial set, its stratification is maximal among complicial stratifications on its underlying simplicial set.

Aaron Lauda then gave a lovely talk about categorifying quantum groups, but it depended so much on beautiful colored slides that I can’t say anything very coherent about it. The slides will supposedly be here.

Tom Leinster and Apostolos Matzaris spoke together about a new way of constructing terminal coalgebras for finitary endofunctors of locally finitely presentable categories, using distributors. If we write our lfp category as the category $Lex(A,Set)$ of finite-limit-preserving functors on some category $A$ with finite limits, then any finitary endofunctor is of the form $M\otimes_A -$ for some flat distributor $M:A^{op}\times A \to Set$. In this case, the terminal coalgebra can be constructed as follows: $T(a)$ is the set of connected components of the category of complexes $$\dots \to a_3 \overset{m_3}{\to} a_2 \overset{m_2}{\to} a_1 \overset{m_1}{\to} a$$ where $m_i \in M(a_i,a_{i-1})$. The intuition behind this is that $T(a)$ is the set of “ways in which $a$ can behave under repeated application of the endofunctor $M\otimes_A -$.”

Julia Goedecke then spoke about satellites in semi-abelian categories. It seems there are many different ways to define such satellites, which work under different conditions and agree whenever they are all defined. One uses comonads (as has been discussed, for instance here), one uses “Hopf formulae,” and one uses Kan extensions. In particular, the latter works without the assumption of enough projectives. Unfortunately, I didn’t understand the details.

Finally, Paul-Andre Mellies spoke about game semantics for proof theory.