The n-Category Café

Dominic Verity and I have just posted a paper on the arXiv entitled “The comprehension construction.” This post is meant to explain what we mean by the name.

The comprehension construction is somehow analogous to both the straightening and the unstraightening constructions introduced by Lurie in his development of the theory of quasi-categories. Most people use the term $\infty$-categories as a rough synonym for quasi-categories, but we reserve this term for something more general: the objects in any $\infty$-cosmos. There is an $\infty$-cosmos whose objects are quasi-categories and another whose objects are complete Segal spaces. But there are also more exotic $\infty$-cosmoi whose objects model $(\infty,n)$-categories or fibered $(\infty,1)$-categories, and our comprehension construction applies to any of these contexts.

The input to the comprehension construction is any cocartesian fibration between $\infty$-categories together with a third $\infty$-category $A$. The output is then a particular homotopy coherent diagram that we refer to as the comprehension functor. In the case $A=1$, the comprehension functor defines a “straightening” of the cocartesian fibration. In the case where the cocartesian fibration is the universal one over the quasi-category of small $\infty$-categories, the comprehension functor converts a homotopy coherent diagram of shape $A$ into its “unstraightening,” a cocartesian fibration over $A$.

The fact that the comprehension construction can be applied in any $\infty$-cosmos has an immediate benefit. The codomain projection functor associated to an $\infty$-category $A$ defines a cocartesian fibration in the slice $\infty$-cosmos over $A$, in which case the comprehension functor specializes to define the Yoneda embedding.

Australia’s Prime Minister Malcolm Turnbull, today:

The laws of mathematics are very commendable, but the only law that applies in Australia is the law of Australia.

The context: Turnbull wants Australia to undermine encryption by compelling backdoors by law. The argument is that governments should have the right to read all their citizens’ communications.

Technologists have explained over and over again why this won’t work, but politicians like Turnbull know better. The recent, enormous, Petya and WannaCry malware attacks (hitting British hospitals, for instance) show what can happen when intelligence agencies such as the NSA treat vulnerabilities in software as opportunities to be exploited rather than problems to be fixed.

Thanks to David Roberts for sending me the link.

My students are trying to piece together general theory of networks, inspired by many examples. A good general theory should clarify and unify these examples. What some people call network theory, I’d just call ‘applied graph invariant theory’: they come up with a way to calculate numbers from graphs, they calculate these numbers for graphs that show up in nature, and then they try to draw conclusions about this. That’s fine as far as it goes, but there’s a lot more to network theory!

Last time I sketched how the $E_8$ Dynkin diagram arises from the icosahedron. This time I’m fill in some details. I won’t fill in all the details, because I don’t know how! Working them out is the goal of this series, and I’d like to enlist your help.

As Kennedy said: ask not what your n-Café can do for you. Ask what you can do for your n-Café!

The ‘geometric McKay correspondence’, actually discovered by Patrick du Val in 1934, is a wonderful relation between the Platonic solids and the ADE Dynkin diagrams. In particular, it sets up a connection between two of my favorite things, the icosahedron:

and the $\mathrm{E}_8$ Dynkin diagram:

When I recently gave a talk on this topic, I realized I didn’t understand it as well as I’d like. Since then I’ve been making progress with the help of this book:

• Alexander Kirillov Jr., Quiver Representations and Quiver Varieties, AMS, Providence, Rhode Island, 2016.

I now think I glimpse a way forward to a very concrete and vivid understanding of the relation between the icosahedron and E₈. It’s really just a matter of taking the ideas in this book and working them out concretely in this case. But it takes some thought, at least for me. I’d like to enlist your help.

guest post by Mike Stay

Last year, my son’s math teacher introduced the kids to the concept of a function. One of the major points of confusion in the class was the idea that it didn’t matter whether he wrote $f(x) = x^2$ or $f(y) = y^2$, but it did matter whether he wrote $f(x) = x y$ or $f(x) = x z$. The function declaration binds some of the variables appearing on the right to the ones appearing on the left; the ones that don’t appear on the left are “free”. In a few years when he takes calculus, my son will learn about the quantifiers “for all” and “there exists” in the “epsilon-delta” definition of limit; quantifiers also bind variables in expressions.

Reasoning formally about languages with binders is hard:

“The problem of representing and reasoning about inductively-defined structures with binders is central to the PoplMark challenges. Representing binders has been recognized as crucial by the theorem proving community, and many different solutions to this problem have been proposed. In our (still limited) experience, none emerge as clear winners.” – Aydemir, Bohannon, Fairbairn, Foster, Pierce, Sewell, Vytiniotis, Washburn, Weirich, and Zdancewic, Mechanized metatheory for the masses: The PoplMark challenge. (2005)

The paper quoted above reviews around a dozen approaches in section 2.3, and takes pains to point out that their review is incomplete. However, recently Andrew Pitts and his students (particularly Murdoch Gabbay) developed the notion of a nominal set (introductory slides, book) that has largely solved this problem. Bengston and Barrow use a nominal datatype package in Isabell/HOL to formalize $\pi$-calculus, and Clouston defined nominal Lawvere theories. It’s my impression that pretty much everyone now agrees that using nominal sets to formally model binders is the way forward.

Sometimes, though, it’s useful to look backwards; old techniques can lead to new ways of looking at a problem. The earliest approach to the problem of formally modeling bound variables was to eliminate them.

guest post by Mike Stay

Programs are an expression of programmer intent. We want the computer to do something for us, so we need to tell it what to do. We make mistakes, though, so we want to be able to check somehow that the program will do what we want. The idea of semantics for a programming language is that we assign some meaning to programs in such a way that we can reason about the behavior of a program. There are two main approaches to this: denotational semantics and operational semantics. I’ll discuss both below, but the post will focus for the most part on operational semantics.

There’s a long history of using 2-categories and related structures for term rewriting and operational semantics, but Greg Meredith and I are particularly fond of an approach using multisorted Lawvere theories enriched over the category of reflexive directed graphs, which we call Gph. Such enriched Lawvere theories are equal in power to, for instance, Sassone and Sobociński’s reactive systems, but in my opinion they have a cleaner categorical presentation. We wrote a paper on them:

• Representing operational semantics with enriched Lawvere theories.

Here I’ll just sketch the basic ideas.

One of the observations that launched homotopy type theory is that the rule of identity-elimination in Martin-Löf’s identity types automatically generates the structure of an $\infty$-groupoid. In this way, homotopy type theory can be viewed as a “synthetic theory of $\infty$-groupoids.”

It is natural to ask whether there is a similar directed type theory that describes a “synthetic theory of $(\infty,1)$-categories” (or even higher categories). Interpreting types directly as (higher) categories runs into various problems, such as the fact that not all maps between categories are exponentiable (so that not all $\prod$-types exist), and that there are numerous different kinds of “fibrations” given the various possible functorialities and dimensions of categories appearing as fibers. The 2-dimensional directed type theory of Licata and Harper has semantics in 1-categories, with a syntax that distinguishes between co- and contra-variant dependencies; but since the 1-categorical structure is “put in by hand”, it’s not especially synthetic and doesn’t generalize well to higher categories.

An alternative approach was independently suggested by Mike and by Joyal, motivated by the model of homotopy type theory in the category of Reedy fibrant simplicial spaces, which contains as a full subcategory the $\infty$-cosmos of complete Segal spaces, which we call Rezk spaces. It is not possible to model ordinary homotopy type theory directly in the Rezk model structure, which is not right proper, but we can model it in the Reedy model structure and then identify internally some “types with composition,” which correspond to Segal spaces, and “types with composition and univalence,” which correspond to the Rezk spaces.

Almost five years later, we are finally developing this approach in more detail. In a new paper now available on the arXiv, Mike and I give definitions of Segal and Rezk types motivated by these semantics, and demonstrate that these simple definitions suffice to develop the synthetic theory of $(\infty,1)$-categories. So far this includes functors, natural transformations, co- and contravariant type families with discrete fibers ($\infty$-groupoids), the Yoneda lemma (including a “dependent” Yoneda lemma that looks like “directed identity-elimination”), and the theory of coherent adjunctions.

Guest post by José Siqueira

We began our journey in the second Kan Extension Seminar with a discussion of the classical concept of Lawvere theory , facilitated by Evangelia. Together with the concept of a model, this technology allows one to encapsulate the behaviour of algebraic structures defined by collections of $n$-ary operations subject to axioms (such as the ever-popular groups and rings) in a functorial setting, with the added flexibility of easily transferring such structures to arbitrary underlying categories $\mathcal{C}$ with finite products (rather than sticking with $\mathbf{Set}$), naturally leading to important notions such as that of a Lie group.

Throughout the seminar, many features of Lawvere theories and connections to other concepts were unearthed and natural questions were addressed — notably for today’s post, we have established a correspondence between Lawvere theories and finitary monads in $\mathbf{Set}$ and discussed the notion of operad, how things go in the enriched context and what changes if you tweak the definitions to allow for more general kinds of limit. We now conclude this iteration of the seminar by bringing to the table “Monads with arities and their associated theories”, by Clemens Berger, Paul-André Melliès and Mark Weber, which answers the (perhaps last) definitional “what-if”: what goes on if you allow for operations of more general arities.

At this point I would like to thank Alexander Campbell, Brendan Fong and Emily Riehl for the amazing organization and support of this seminar, as well as my fellow colleagues, whose posts, presentations and comments drafted a more user-friendly map to traverse this subject.

Guest post by Daniel Cicala

The Kan Extension Seminar II continues with a discussion of the paper Notions of Lawvere Theory by Stephen Lack and Jirí Rosický.

In his landmark thesis, William Lawvere introduced a method to the study of universal algebra that was vastly more abstract than those previously used. This method actually turns certain mathematical stuff, structure, and properties into a mathematical object! This is achieved with a Lawvere theory: a bijective-on-objects product preserving functor $T \colon \aleph^{\text{op}}_0 \to \mathbf{L}$ where $\aleph_0$ is a skeleton of the category $\mathbf{FinSet}$ and $\mathbf{L}$ is a category with finite products. The analogy between algebraic gadgets and Lawvere theories reads as: stuff, structure, and properties correspond respectively to 1, morphisms, and commuting diagrams.

To get an actual instance, or a model, of an algebraic gadget from a Lawvere theory, we take a product preserving functor $m \colon \mathbf{T} \to \mathbf{Set}$. A model picks out a set $m(1)$ and $n$-ary operations $m(f) \colon m(1)^n \to m(1)$ for every $T$-morphism $f \colon n \to 1$.

To read more about classical Lawvere theories, you can read Evangelia Aleiferi’s discussion of Hyland and Power’s paper on the topic.

With this elegant perspective on universal algebra, we do what mathematicians are wont to do: generalize it. However, there is much to consider undertaking such a project. Firstly, what elements of the theory ought to be generalized? Lack and Rosický provide a clear answer to this question. They generalize along the following three tracks:

• consider a class of limits besides finite products,

• replace the base category $\mathbf{Set}$ with some other suitable category, and

• enrich everything.

Another important consideration is to determine exactly how far to generalize. Why not just go as far as possible? Here are two reasons. First, there are a number of results in this paper that stand up to further generalization if one doesn’t care about constructibility. A second limiting factor of generalization is that one should ensure that central properties still hold. In Notions of Lawvere Theory, the properties lifted from classical Lawvere theories are

• the correspondence between Lawvere theories and monads,

• that algebraic functors have left adjoints, and

• models form reflective subcategories of certain functor categories.

Before starting the discussion of the paper, I would like to take a moment to thank Alexander, Brendan and Emily for running this seminar. I have truly learned a lot and have enjoyed wonderful conversations with everyone involved.

I’ve just finished teaching a seminar course officially called “Functional Equations”, but really more about the concepts of entropy and diversity.

I’m grateful to the participants — from many parts of mathematics, biology and physics, at levels from undergraduate to professor — who kept coming and contributing, week after week. It was lots of fun, and I learned a great deal.

This post collects together all the material in one place. First, the notes:

• Tom Leinster, Functional Equations. Rough and ready course notes, University of Edinburgh, 2017.

Now, the posts I wrote every week:

• I. Cauchy’s equation
• II. Shannon entropy
• III. Explaining relative entropy
• IV. A simple characterization of relative entropy
• V. Expected surprise
• VI. Using probability theory to solve functional equations
• VII. The $p$-norms
• VIII. Measuring biodiversity
• IX. Entropy on a metric space
• X. Value
• XI. The diversity of a metacommunity

The eleventh and final installment of the functional equations course can be described in two ways:

• From one perspective, I talked about conditional entropy, mutual information, and a very appealing analogy between these concepts and the most basic primary-school Venn diagrams.

• From another, it was about diversity across a metacommunity, that is, an ecological community divided into smaller communities (e.g. geographical sites).

The notes begin on page 44 here.

Guest post by Pierre Cagne

The Kan Extension Seminar II continues with a third consecutive of Kelly, entitled On clubs and data-type constructors. It deals with the notion of club, first introduced by Kelly as an attempt to encode theories of categories with structure involving some kind of coherence issues. Astonishing enough, there is no mention of operads whatsoever in this article. (To be fair, there is a mention of “those Lawvere theories with only associativity axioms”…) Is it because the notion of club was developed in several stages at various time periods, making operads less identifiable among this work? Or does Kelly judge irrelevant the link between the two notions? I am not sure, but anyway I think it is quite interesting to read this article in the light of what we now know about operads.

Before starting with the mathematical content, I would like to thank Alexander, Brendan and Emily for organizing this online seminar. It is a great opportunity to take a deeper look at seminal papers that would have been hard to explore all by oneself. On that note, I am also very grateful for the rich discussions we have with my fellow participants.

What is the value of the whole in terms of the values of the parts?

More specifically, given a finite set whose elements have assigned “values” $v_1, \ldots, v_n$ and assigned “sizes” $p_1, \ldots, p_n$ (normalized to sum to $1$), how can we assign a value $\sigma(\mathbf{p}, \mathbf{v})$ to the set in a coherent way?

This seems like a very general question. But in fact, just a few sensible requirements on the function $\sigma$ are enough to pin it down almost uniquely. And the answer turns out to be closely connected to existing mathematical concepts that you probably already know.

The American Mathematical Society is having a meeting here at U. C. Riverside during the weekend of November 4th and 5th, 2017. I’m organizing a session on Applied Category Theory, and I’m looking for people to give talks.