The n-Category Café

There’s a new paper on the problem of comparing different definitions of $(\infty,n)$-category:

• Clark Barwick and Chris Schommer-Pries, On the unicity of the homotopy theory of higher categories.

My thesis advisor often used the word ‘unicity’ instead of the more common ‘uniqueness’. I’ve never seen anyone else do that until now! But that’s not the most exciting thing about this paper…

This post is essentially a summary of a long discussion between Urs and myself about axiomatizing cohesive $(\infty,1)$-toposes in homotopy type theory. But it should be accessible and interesting even if you don’t care about cohesive $(\infty,1)$-toposes. I think it yields interesting general conclusions about internalization, type theory, higher modal logic, and the importance of codiscreteness.

Note that practically everything I’m going to say below has been formalized in Coq, and it can be found here.

Suppose we have a forgetful functor $U\colon H \to S$, and we want to speak about properties of this functor without “leaving the world of $H$”. (The example I particularly have in mind is when $S=Sets$ or $\infty Gpd$ and $U$ is the direct image functor of the global-sections geometric morphism for a topos or $(\infty,1)$-topos.) A clear prerequisite for this is that we can somehow recover $S$ from data in or on $H$, and an obvious way to do this is to assume that $U$ has either a monadic right adjoint or a comonadic left adjoint. For various reasons, including simplicity, let’s restrict to the case when these adjoints are fully faithful (so they equip $H$ with “discrete objects” or “codiscrete objects” in the sense used in my last post). Then it’s easy to describe $S$ and $U$ purely in terms of data on $H$: we simply specify a reflective or coreflective subcategory.

However, now suppose we want to describe this in the internal logic of $H$. Roughly speaking, the internal logic is a way of speaking about objects as if they were sets or spaces with “elements”, together with a way to “interpret” or “compile” such language into statements about $H$ in the usual language of category theory that uses generalized elements. For instance, an assertion in the internal language such as “for any $x\in A$ and $y\in B$, there exists a unique $(x,y)\in A\times B$ such that …” compiles to the usual definition of a cartesian product: “for any $x\colon U\to A$ and $y\colon U\to B$, there exists a unique $(x,y)\colon U\to A\times B$ such that … “.

In the internal logic of $H$, therefore, the objects of $H$ act like sets (if $H$ is a 1-topos) or $\infty$-groupoids (if $H$ is an $(\infty,1)$-topos). The internal logic of a 1-topos is sometimes called its Mitchell-Benabou language, while the internal logic of an $(\infty,1)$-topos is (conjecturally) homotopy type theory. From now on, I’ll use the language of the latter; so for instance “type” should be read as referring to an object of $H$. (I’ll also slip into the implicit ∞-category theory convention, just because it would be way too cumbersome otherwise.)

This is to announce the workshop

Higher Geometric Structures along the Lower Rhine

Organisers: Christian Blohmann, Marius Crainic, Ieke Moerdijk

Date: Thu, 2012-01-12 – Fri, 2012-01-13

Details: Program, Abstracts

This is the first in a series of short workshops jointly organized by the Geometry/Topology groups in Bonn, Nijmegen, and Utrecht, all situated along the Lower Rhine.

This week takes place this year’s workshop on

Higher structures in mathematics and physics

in Göttingen.

Myself, I speak about

$\infty$-Chern-Simons functionals (pdf slides).

I’ll report on some talks in the comment section below.

A while back some of us started thinking that it would be useful to add to the nLab a peer-review functionality, whereby certain versions of entries could get an official stamp saying something like “This material has been read and carefully checked by an expert referee, it seems to be reliable”. This is the way it works for instance also at the scientific wiki called Manifold Atlas.

We have made this happen for instance with the entry geometric realization of simplicial topological spaces, after we noticed that it was being cited in publications. You can see its referee report here.

In the course of the discussion of these issues, it became clear that not only does peer-review add value to existing $n$Lab material, but offering official publication status also adds incentive for authors to put material into the $n$Lab in the first place. In other words, in addition to its functionality as a “lab book”, it could also function as a scientific journal. That branch now exists and is called

• The Publications of the nLab,

  a web-based journal for peer-reviewed publication of original research and expository writing on topics in mathematics and mathematical physics that are usefully discussed from the point of view of category theory and homotopy theory/higher category theory.

There are still some administrative issues to be organized behind the scenes, but we do have a first published article now:

• Tom Leinster, An informal introduction to topos theory, Publications of the $n$Lab, vol 1, no. 1 (2011) .

This went through a refereeing process as usual for journals. The referee report is in fact publically available, see the details listed here.

Meanwhile a second article has been submitted and is with the referee. Our idea is that once two articles have gone fully through the publication process, so that one can see at examples what the $n$Publications are going to be like, we formally install an editorial board consisting of names from the list of “tentatively confirmed” editors here (whereas currently the nLab steering committee still plays the role of the editorial board for the $n$Publications).

Today I realized that two old friends of mine are closely related: categories of spaces with discrete and codiscrete objects, and the monadicity of fibrations and opfibrations. The glue between them is called the scone.

Tomorrow morning I will be giving a talk at the Hausdorff institute in Bonn. It will be a piece in chalk on blackboard, but for convenience I have created accompanying pdf slides:

Chern-Simons terms on higher moduli stacks .

I’d enjoy hearing whatever comment you might have.

[edit: A little later, on Dec 14, I am giving in Hamburg a more gentle introduction of the basic idea to a general audience. Again chalk on blackboard, but again with accompanying pdf slides.]

Following “exercise I” on Axiomatic Cohesion in Homotopy Type Theory, where we saw (thanks to Guillaume Brunerie!) the HoTT-Coq code incantation of the Maurer-Cartan form on cohesive ∞-groups, it should now be a small step to conjure up something rather interesting: the definition of differential cohomology and the proof of its characteristic curvature exact sequence.

A writeup of this in the pseudocode formerly known as traditional mathematics is in section 2.3.14, p. 147 of Differential Cohomology in a Cohesive ∞-Topos. The following “exercises a) – d)” try to extract from this a core statement that should have a fairly straightforward implementation in HoTT-Coq (I hope!).

As before, this “exercise” is an exercise that I am posing myself. But also as before, it is more than likely that HoTT experts can solve this many orders of magnitudes quicker than I will. Don’t hesitate, there are plenty of further “exercises” along these lines waiting to get attention.

Exercise II a) In exericse I you found HoTT encoding of the fiber sequence

$$G \stackrel{\theta}{\to} \flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G \to \mathbf{B}G$$

exhibiting the Maurer-Cartan form with values in de Rham coefficients inside the moduli ∞-stack of flat ∞-connections for a cohesive ∞-group $G$.

Take now $G = \mathbf{B}^n A$ to be an Eilenberg-MacLane object. Then, as before, the fiber sequence continues further to the left to yield

$$\Omega \flat \mathbf{B}^{n+1} A \to \mathbf{B}^n A \stackrel{\theta}{\to} \flat_{dR} \mathbf{B}^{n+1}A \to \cdots \,.$$

Show that $\flat$ – being a right adjoint – commutes with forming loop space objects and thus deduce the fiber sequence

$$\flat \mathbf{B}^{n} A \to \mathbf{B}^{n} A \stackrel{\theta}{\to} \flat_{dR} \mathbf{B}^{n+1}A \,.$$

Exercise II b) Consider a morphism into $\flat_{dR} \mathbf{B}^{n+1}A$ out of a 0-truncated object, to be denoted

$$\Omega^{n+1}_{cl}(-,A) \to \flat_{dR} \mathbf{B}^{n+1} A \,.$$

For later exercises we will demand the morphism thus denoted to be an effective epimorphism. But describing effective epiness will require more work than fits into the present exercise. Since the following parts c) and d) do not yet depend on this morphism being effective epi, we can ignore it for the moment and just assume some morphism out of a 0-truncated object. Extra credit, of course, if you manage to code effective epiness nevertheless!

Exercise II c) Define the type $\mathbf{B}^n A_{conn}$ – to be called the moduli ∞-stack of A-principal n-connections – as the ∞-pullback

$$\array{ \mathbf{B}^n A_{conn} &\stackrel{F}{\to}& \Omega^{n+1}_{cl}(-,A) \\ \downarrow && \downarrow \\ \mathbf{B}^n A &\stackrel{\theta}{\to}& \mathbf{\flat}_{dR} \mathbf{B}^{n+1} A } \,.$$

Exercise II d) Prove that the type thus defined fits into a fiber sequence of the form

$$\flat \mathbf{B}^n A \to \mathbf{B}^n A_{conn} \stackrel{F}{\to} \Omega^{n+1}_{cl}(-,A)$$

to be called the $\infty$-stack refinement of the curvature exact sequence.

Remark. The meat is in a). The rest should be straightforward consequences whose main point is to amplify the relevance of a).

The last time I talked about derivators, we ended up making an interesting comparison between derivator techniques and quasicategory techniques. In particular, we looked at a proof of the pasting law for homotopy pullbacks using derivators (presented in that post) and the analogous proof for quasicategories from Higher Topos Theory (partially described here). We thought at the time it would be nice to continue with further comparisons, but got sidetracked.

Along those lines, here’s another little fact that was easy for me to prove with derivators. Anyone care to try their hand at a proof using quasicategories, so we can compare them?

After a gestation period of many years, the following paper is finally ready for the light of day:

• Kate Ponto and Michael Shulman, Duality and traces in indexed monoidal categories. We’re currently having issues with the arXiv compiler, but you can get it from my web page. There are three versions:
  • If you’re going to read it on a screen, or print it in color, get this version
  • If you’re going to print it in black and white, get this version
  • If you’re going to do both, but you only want to download one file, get this version.

There are also (at least) two ways to read this paper. If you’re mainly interested in duality and trace (especially their applications in fixed-point theory), then you can read sections 1–8 and stop there. On the other hand, if you’re mainly interested in indexed monoidal categories and their string diagrams, you can read sections 1–3, then 9–10. (But you may still want to go back and read sections 4–8 and 11–12, to see the applications of the string diagrams.)

I’m not going to say anything about traces today—you can read the paper for that. But I’ll say a bit about indexed monoidal categories and string diagrams, which I expect will be of interest to several people here; especially since we got the basic idea of these string diagrams from another discussion here.

In the discussion of a previous entry finally the Coq-formulation of the axioms of cohesion in homotopy type theory (HoTT) materialized (thanks to prodding by David Corfield and expertise by Mike Shulman). See

• Axiomatic cohesion in HoTT .

With these axioms in hand, I would now enjoy to see the machinery put to work. I’ll try to take this as an occasion to learn HoTT and its coding as we go along. Currently I still know next to nothing, and so I am hoping that by stating in public the exercises that I pose to myself, I might get some hints from the experts and some help from whoever likes to join in.

The following should be a very basic and nevertheless interesting first exercise to warm up.

Exercise I a) Give the Coq-code that describes from a connected type – to be denoted

BG : Type

the homotopy fiber type of

map_from_flat BG : flat BG -> BG

to be denoted

flat_dR BG : Type

(The de Rham coefficient object.)

Exercise I b) Give the Coq-code that describes the canonical term

theta : G -> flat_dR BG

where G is the identity type

Id_BG pt pt : Type

(This $\theta$ formalizes the notion of the Maurer-Cartan form on $G$.)

Hint: use uuo.v.

Warning: I assume that comprehensive code for the notion of connected objects is more involved than the rest of the exercise, so probably it is helpful to first adopt a more ad hoc treatment.