The n-Category Café

This is to share a little observation about the formulation of flat Ehresmann connections in cohesive homotopy type theory.

For context, this can be understood as following up on two different threads on this blog:

1. You may think of this as part IV of the little series HoTT Cohesion (part I: de Rham cohomology, part II: differential cohomology, part III: geometric prequantization) in which we discussed very simple constructions in homotopy type theory that exist as soon as the axiom of cohesion is added and which, simple as they are, are interpreted as fundamental constructions in higher differential geometry.

2. You may think of this as a curious example of the theory of twisted principal ∞-bundles discussed in the previous entry. For I will describe how a flat Ehresmann connection on a $G$-principal $\infty$-bundle is formalized as a $\flat G$-twisted $\infty$-bundle on its total space, where $\flat$ (“flat”) is one of the two reflectors in the definition of cohesive homotopy type theory.

A few weeks back I had mentioned that with Thomas Nikolaus and Danny Stevenson we are busy writing up some notes on bundles in higher geometry. Now we feel that we are closing in on a fairly stable version, and so we thought it may be about time to share what we have and ask for feedback.

As it goes, this project has become a collection of three articles now. They are subdivided as

Principal ∞-bundles

1. General theory (pdf)

2. Presentations (pdf)

3. Applications (not yet out)

The idea is that the first proceeds in full abstraction, using just the axioms of $\infty$-topos theory (so roughly, up to the technical caveats discussed here at length: using just the axioms of homotopy type theory), while the second discusses models of the axioms by presentations in categories of simplicial (pre)sheaves.

More explicitly, in the first one we discuss how, in a given $\infty$-topos, principal $\infty$-bundles are equivalent to cocycles in the $\infty$-topos, how fiber $\infty$-bundles are associated to principal $\infty$-bundles and how their sections are cocycles in twisted cohomology classifying twisted principal $\infty$-bundles and extensions of structure $\infty$-groups. We close by identifying the universal twisting bundles/local coefficient bundles with $\infty$-gerbes and discuss how this reproduces various notions of $n$-gerbes.

In the second one we show how principal $\infty$-bundles are equivalent to cocycles in simplicial hyper-Čech-cohomology, and we prove a strictification result: in a 1-localic $\infty$-topos the space of principal $\infty$-bundles over any $\infty$-stack is modeled by ordinary simplicial bundles with an ordinary action of a simplicial group, the only weakening being that the principality condition holds only up to local weak equivalence. We discuss what this looks like for discrete geometry and for smooth geometry.

For a tad more detail see the abstracts (General Theory abstract, Presentations abstract). And for full details, including references (see page 4 of part 2 for a discussion of the literature) etc. see – of course – the writeups themselves: 1. General theory, 2. Presentations.

All comments would be welcome!

I found the following article when John posted about it on Google Plus:

• DragonBox: Algebra Beats Angry Birds

Go read it; I’ll wait for you below the fold.

I have been looking for examples, accessible to a lay audience, to illustrate the prevalence of cohomology. Here are some possibilities:

• Penrose’s impossible figures, such as the tribar
• Carrying in arithmetic
• Electrical circuits and Kirchhoff’s Law
• Pythagorean triples (Hilbert’s Theorem 90)
• Condorcet’s paradox (concerning the impossibility of combining comparative rankings)
• Entropy, but I think we never quited nailed this.

Anyway, I’d be grateful for any other cases of cohomology in everyday life.

Recently I’ve been talking a lot about homotopy type theory, and its potential role as a foundation for mathematics in which homotopy types — which is to say $\infty$-groupoids — are basic objects. However, when I say this to $n$-categorists, I inevitably get the question “Why stop with $\infty$-groupoids? What about $n$-categories, or $(\infty,n)$-categories, or $(\infty,\infty)$-categories?” Until now, I’ve had only two answers:

1. Maybe there is a foundation in which higher categories are basic objects — but we don’t know yet what it might look like. For instance, some of us have thought about a “directed type theory” for 1-categories. This seems to work, but it’s not as clean as homotopy type theory: the composition laws seem to have to be put in by hand, rather than falling out automatically like they do for $\infty$-groupoids using the inductive definition of identity types. For $n$-categories or $\omega$-categories, it seems that we would essentially have to build something like a Batanin operad into the structure of the type theory. This is probably possible, but not especially appealing to me, unless someone finds a clean way of “generating” such an operad in the same way that Martin-Löf identity types “generate” all the structure of a Batanin $\infty$-groupoid.

   There is also the question of what a “dependent type” should mean for directed categories. Presumably some sort of fibration — but of what variance? We seem to need different kinds of “dependent type” for fibrations and opfibrations, and as we go up in categorical level this problem will multiply itself. Moreover, not all functors are exponentiable, so dependent product types will require some variance assumptions. Furthermore, I think there are some issues with the categorical semantics when you get up to 3-categories: comma objects don’t seem to do the right thing any more.

2. These problems suggest that maybe even in the long run, we’ll decide that it’s better to only build $\infty$-groupoids into the foundational system, with directed categories as a defined notion. (I’m not saying I think we necessarily will, just that I think it’s possible that we will.) If we go this route, then I think the most promising way to define $(\infty,n)$-categories inside homotopy type theory would be an adaptation of Charles Rezk’s “complete Segal spaces” and $\Theta$-categories, since these are defined entirely in terms of diagrams of $\infty$-groupoids and don’t require any truncatedness of the space of objects. (The fact that every $\infty$-groupoid admits an essentially surjective map from a 0-truncated one — that is, from a set — is a “classicality” property that doesn’t hold in general homotopy type theory. Thus, any definition of $(\infty,n)$-categories which requires that the objects form a set — which includes most definitions other than Rezk’s — would be insufficiently general.)

   However, we don’t yet know how to define simplicial objects or $\Theta$-objects inside of homotopy type theory (unless we are willing to allow infinite lists of definitions, which is fine mathematically if we assume a strong enough metatheory, but difficult to implement in a computer). Depending on how we end up solving that problem, this approach could also turn out to be technically complicated.

In this post, I want to present a third approach, which sort of straddles these two pictures. On the one hand, it gives us a way to talk about $(\infty,1)$-categories (and, probably, $(\infty,n)$-categories) inside homotopy type theory today, without waiting for a solution to the problem of defining simplicial objects (although in the long run, we’ll still need to solve that problem). On the other hand, we can think of it as a rough approximation to what an eventual “directed homotopy type theory” might look like.

However, this is still just a basic idea; there are technical issues as well as conceptual questions that need to be answered. I’ve been rolling them around in my head for a while and not making much progress, so I’m hoping to start a discussion in which other people may be able to see what I can’t.

guest post by Mike Stay

Thanks to primates’ propensity for trade and because our planet rotates, everyone is familiar with abelian groups. We can add, we’ve got a zero element, addition is commutative and associative, and we can negate any element—or, using multiplicative language: we can multiply, we’ve got a 1 element, multiplication is commutative and associative, and we can divide 1 by any element to get its inverse.

Thanks to the fact that for most practical purposes we live in $\mathbb{R}^3,$ everyone’s familiar with at least one vector space. Peano defined them formally in 1888. The collection of vector spaces is like a “categorified” abelian group: instead of being elements of a set, vector spaces are objects in a compact closed category. We can “multiply” them using the tensor product; we have the 1-dimensional vector space that plays the role of 1 up to an isomorphism called the unitor; the tensor product is associative up to an isomorphism called the associator, and is commutative up to an isomorphism called the braiding; and every object $A$ has a “weak inverse”, or dual, an object equipped with morphisms for “cancelling”, $e_A:A\otimes A^{\ast} \to 1$ and $i_A:1 \to A^{\ast}\otimes A$ and some “yanking” equations. As always in categorification, when we weaken equations to isomorphisms, we have to add new equations: a pentagon equation for the associator, triangle equations for the unitors, hexagon equations for the braiding, and braiding twice is the identity.

Thanks to the fact that everyone has family and friends, everyone is (ahem) familiar with relations. Sets, relations, and implications form a compact closed bicategory. In a compact closed bicategory, we weaken the equations above to 2-isomorphisms and add new equations: an associahedron with 14 vertices, 7-vertex prisms for the unitors, shuffle polytopes and a map of permutahedra for the braiding, and an equation governing the syllepsis. The syllepsis is what happens when we weaken the symmetry equation: braiding twice is merely isomorphic to the identity.

Sequences

We can start to see some sequences emerging from this process. The stuff below is mostly due to Chris Schommer-Pries’ definition of symmetric monoidal bicategories together with Day and Street’s definition of a compact closed Gray monoid. Their work, in turn, relies greatly on Paddy McCrudden’s Balanced coalgebroids and a handwritten note for the swallowtail coherence law. In the graphics below, I tried to make the symmetries apparent, something that was lacking from McCrudden’s presentation of the coherence laws due to the failings of the tools available for typesetting them.