## May 24, 2017

### A Type Theory for Synthetic ∞-Categories

#### Posted by Emily Riehl

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.

Posted at 12:11 AM UTC | Permalink | Followups (13)

## May 12, 2017

### Unboxing Algebraic Theories of Generalised Arities

#### Posted by Emily Riehl

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.

Posted at 4:38 AM UTC | Permalink | Followups (2)

## May 1, 2017

### A Discussion on Notions of Lawvere Theories

#### Posted by Emily Riehl

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.

Posted at 11:37 PM UTC | Permalink | Followups (1)

## April 19, 2017

### Functional Equations, Entropy and Diversity: A Seminar Course

#### Posted by Tom Leinster

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:

Now, the posts I wrote every week:

Posted at 5:06 PM UTC | Permalink | Followups (2)

### The Diversity of a Metacommunity

#### Posted by Tom Leinster

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.

## April 17, 2017

### On Clubs and Data-Type Constructors

#### Posted by Emily Riehl

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.

Posted at 12:30 AM UTC | Permalink | Followups (4)

## April 14, 2017

### Value

#### Posted by Tom Leinster

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.

Posted at 4:17 PM UTC | Permalink | Followups (9)

## April 5, 2017

### Applied Category Theory

#### Posted by John Baez

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.

### Functional Equations IX: Entropy on a Metric Space

#### Posted by Tom Leinster

Yesterday’s functional equations class can be described in two ways:

From a mathematical point of view, I gave a definition of the entropy of a probability distribution on a metric space. The high point was a newish maximum entropy theorem (joint work with Mark Meckes).

From a biological point of view, it was all about measuring the diversity of a community in a way that factors in the varying similarity between species. This approach is well-adapted to situations where there’s no clear division into “species” — for instance, communities of microbes. It also addresses a point made yesterday on this blog. All this is based on joint work with Christina Cobbold.

You can read the notes from yesterday’s class on pages 35–38 here.

## April 4, 2017

### Elementary (∞,1)-Topoi

#### Posted by Mike Shulman

Toposes come in two varieties: “Grothendieck” and “elementary”. A Grothendieck topos is the category of sheaves of sets on some site. An elementary topos is a cartesian closed category with finite limits and a subobject classifier. Though these definitions seem quite different, they are very closely related: every Grothendieck topos is an elementary topos, while elementary toposes (especially when considered “over a fixed base”) behave very much like Grothendieck ones.

All the fervor about $(\infty,1)$-toposes nowadays has centered on Grothendieck ones: $(\infty,1)$-categories of $\infty$-sheaves of $\infty$-groupoids on $(\infty,1)$-sites. (Technically, this is only true if we use a perhaps-excessively-general notion of “site”, but it’s the right idea.) However, it’s quite natural to speculate about a corresponding notion of elementary $(\infty,1)$-topos. Because an elementary 1-topos is essentially “a category whose internal logic is intuitionistic higher-order type theory”, it’s natural to try to define an elementary $(\infty,1)$-topos to be an $(\infty,1)$-category whose “internal logic” is, or at least should be, a kind of homotopy type theory. However, even laying aside the unresolved questions involved in the “internal logic” of $(\infty,1)$-categories, it’s never been entirely clear to me exactly what “kind” of homotopy type theory we should use here.

Until now, that is. I propose the following definition: an elementary (∞,1)-topos is an $(\infty,1)$-category such that

• It has finite limits and colimits (in the $\infty$-sense, i.e. homotopy limits and colimits).
• It is locally cartesian closed.
• It has a subobject classifier, i.e. a map $\top:1\to \Omega$ such that for any $X$ the hom-$\infty$-groupoid $Hom(X,\Omega)$ is equivalent, by pullback of $\top$, to the $\infty$-groupoid of subobjects of $X$ (which is equivalent to a discrete set). Here a “subobject” is a map $S\to X$ such that each $\infty$-functor $Hom(Z,S) \to Hom(Z,X)$ is fully faithful.
• For any morphism $f:Y\to X$, there exists an object classifier $p:V\to U$ that classifies $f$ (i.e. $f$ is a pullback of $p$) and such that the collection of morphisms it classifies (i.e. the pullbacks of $p$) is closed under composition, finite fiberwise limits and colimits, and dependent products. Here $p:V\to U$ is an “object classifier” if for any $X$, pullback of $p$ yields a fully faithful functor from $Hom(X,U)$ to the core (the maximal sub-$\infty$-groupoid) of the slice $(\infty,1)$-category over $X$.
Posted at 9:08 AM UTC | Permalink | Followups (16)

## April 3, 2017

### Gluing Together Finite Shapes with Kelly

#### Posted by Emily Riehl

Guest post by David Jaz Myers

The Kan Extension Seminar continues with Kelly’s Structures defined by limits in the enriched context, I, or as I like to call it, Presenting categories whose objects are glued together out of finite shapes. This paper hit the presses in 1982 and represented both a condensation and generalization of the theory of locally finitely presentable categories. Kelly achieved both the condensing and the generalizing through his use of weighted (or, as he calls them, indexed) limits and colimits. The resulting theory is slick and highly categorical, but very dense. So, in this post, we’re going to button down a bit and skim over a few details so that we can focus on the story and the powerful results which sustain it, rather than the technicalities. I will label the propositions by where they appear in Kelly’s paper, so that you can find the technicalities if you would like.

At first, it will seem like this post is a radical departure from the previous seminar posts. But as we go on, we’ll see that gluing together finite shapes has a lot to do with the categorical approach to algebra that Evangelia wrote about in the post that kicked off our seminar.

Before I start, I’d like to thank Emily, Alexander, and Brendan for organizing this lovely seminar and inviting me to participate. I’d also like to thank my fellow students for their insight and conversation.

Posted at 1:52 AM UTC | Permalink | Followups (3)

### Enrichment and its Limits

#### Posted by Emily Riehl

Guest post by David Jaz Myers

What are weighted limits and colimits? They’re great, that’s what!

In this post, we prepare for the next part of the Kan Extension Seminar by learning a bit about enrichment and weighted limits and colimits. I’ll also describe the “$\mathcal{V}\,$ point of view” that I’ll be adopting for the next post.

Posted at 1:16 AM UTC | Permalink | Followups (4)

## April 1, 2017

### Jobs at U. C. Riverside

#### Posted by John Baez

The Mathematics Department of the University of California at Riverside is trying to hire some visiting assistant professors. We plan to make decisions quite soon!

The positions are open to applicants who have PhD or will have a PhD by the beginning of the term from all research areas in mathematics. The teaching load is six courses per year (i.e. 2 per quarter). In addition to teaching, the applicants will be responsible for attending advanced seminars and working on research projects.

This is initially a one-year appointment, and with successful annual teaching review, it is renewable for up to a third year term.

For more details, including how to apply, go here:

https://www.mathjobs.org/jobs/jobs/10162

## March 29, 2017

### Functional Equations VIII: Measuring Biodiversity

#### Posted by Tom Leinster

Posts entitled “Such-and-Such Part 8” can be intimidating…! But in this week’s instalment of the functional equations course, we just began a new topic. So if you’ve been interested in this course at a distance, without having actually dived in, now is a decent entry point.

This week, I introduced the difficult conceptual question of how to quantify biological diversity. A partial answer is given by what ecologists call the Hill numbers, which are the exponentials of what others call the Rényi entropies. I explained what these are, how they behave, and how they’re linked to other mathematical concepts.

There were hardly any actual functional equations this week, but they’ll come back soon! This week was mainly just background and intuition.

You can find the notes from this week’s session on pages 30–34 of the notes so far.

Posted at 2:32 AM UTC | Permalink | Followups (4)

## March 22, 2017

### Functional Equations VII: The p-Norms

#### Posted by Tom Leinster

The $p$-norms have a nice multiplicativity property:

$\|(A x, A y, A z, B x, B y, B z)\|_p = \|(A, B)\|_p \, \|(x, y, z)\|_p$

for all $A, B, x, y, z \in \mathbb{R}$ — and similarly, of course, for any numbers of arguments.

Guillaume Aubrun and Ion Nechita showed that this condition completely characterizes the $p$-norms. In other words, any system of norms that’s multiplicative in this sense must be equal to $\|\cdot\|_p$ for some $p \in [1, \infty]$. And the amazing thing is, to prove this, they used some nontrivial probability theory.

All this is explained in this week’s functional equations notes, which start on page 26 here.