November 30, 2011
The (∞,1)Category of (∞,n)Categories
Posted by John Baez
There’s a new paper on the problem of comparing different definitions of $(\infty,n)$category:
 Clark Barwick and Chris SchommerPries, 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…
November 29, 2011
Internalizing the External, or The Joys of Codiscreteness
Posted by Mike Shulman
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 globalsections 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 1topos) or $\infty$groupoids (if $H$ is an $(\infty,1)$topos). The internal logic of a 1topos is sometimes called its MitchellBenabou 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.)
Higher Structures Along The Lower Rhine
Posted by Urs Schreiber
This is to announce the workshop
Higher Geometric Structures along the Lower Rhine
Organisers: Christian Blohmann, Marius Crainic, Ieke Moerdijk
Date: Thu, 20120112 – Fri, 20120113
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.
November 28, 2011
Higher Structures 2011
Posted by Urs Schreiber
This week takes place this year’s workshop on
Higher structures in mathematics and physics
in Göttingen.
Myself, I speak about
$\infty$ChernSimons functionals (pdf slides).
I’ll report on some talks in the comment section below.
November 23, 2011
Publications of the nLab
Posted by Urs Schreiber
A while back some of us started thinking that it would be useful to add to the nLab a peerreview 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 peerreview 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

a webbased journal for peerreviewed 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).
November 22, 2011
Discreteness, Concreteness, Fibrations, and Scones
Posted by Mike Shulman
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.
November 15, 2011
ChernSimons Terms on Higher Moduli Stacks
Posted by Urs Schreiber
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:
ChernSimons 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.]
November 9, 2011
HoTT Cohesion – Exercise II
Posted by Urs Schreiber
Following “exercise I” on Axiomatic Cohesion in Homotopy Type Theory, where we saw (thanks to Guillaume Brunerie!) the HoTTCoq code incantation of the MaurerCartan 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 HoTTCoq (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 MaurerCartan 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 EilenbergMacLane 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 0truncated 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 0truncated 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 Aprincipal nconnections – 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).
November 7, 2011
Productive Homotopy Pullbacks
Posted by Mike Shulman
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?
November 4, 2011
Traces in Indexed Monoidal Categories
Posted by Mike Shulman
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 fixedpoint 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.
November 2, 2011
HoTT Cohesion – Exercise I
Posted by Urs Schreiber
In the discussion of a previous entry finally the Coqformulation of the axioms of cohesion in homotopy type theory (HoTT) materialized (thanks to prodding by David Corfield and expertise by Mike Shulman). See
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 Coqcode 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 Coqcode 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 MaurerCartan 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.