Speakers

Title: Two dimensional Lie theory

Abstract: This week I present an outline of a joint project with Ben MacAdam. The main aim is to generalise the theory of Lie groupoids and Lie algebroids by using 2-cubical sets. One advantage of this approach is that it avoids a certain quotient that is required in the classical theory and is therefore more amenable to generalisation in terms of tangent categories. An additional advantage of this approach is that when the tangent category is assumed representable the appropriate modification of the Lie approximation functor becomes representable also.

Title: The free Lie algebras in Tebbe’s calculation of the derivatives of atomic functors
Abstract: A discrete module is a functor from finite pointed sets to chain complexes of R-modules. There are two ways to do functor calculus for discrete modules. The first is to find the Taylor tower in a way analogous to the Taylor series of functions of a real variable. A second approach is to something more akin to Lagrangian approximation. For functions of a real variable, f, the n-th Lagrangian approximation is the degree n polynomial function which agrees with f on n+1 point. In the case of a discrete module, F, one uses a left Kan extension to produce the best Lagrangian approximation to F. The quotient of successive Lagrangian polynomial functors are called atomic functors.
In her PhD thesis, Amelia Tebbe showed that the n-th derivatives of atomic functors, in the sense of Goodwillie calculus, involve products of free Lie algebras and simple cross effects. The goal of this talk is to present this calculation, and to ask the audience if this looks familiar.

Title: Interpretations of algebraic theories, and the adjunctions they induce: Part II
Abstract: Many cases of free/forgetful adjunctions are special cases of a more general theorem: any interpretation of algebraic theories induces an adjunction on their categories of models. Free monoid, free groups, free modules, tensor algebras, and polynomial rings are all instances of this. In my talk I will prove this theorem.

Title: Interpretations of algebraic theories, and the adjunctions they induce
Abstract: Many cases of free/forgetful adjunctions are special cases of a more general theorem: any interpretation of algebraic theories induces an adjunction on their categories of models. Free monoid, free groups, free modules, tensor algebras, and polynomial rings are all instances of this. In my talk I will prove this theorem.

Title: Introduction to univalence in Coq IV
Abstract: This week we conclude our sequence of talks on homotopy type theory (HoTT). We revisit the univalence axiom and use a simple example to illustrate its use.
The audience is encouraged to follow the development of the theory on their own computers so please bring a laptop if you want to do this! (You will need about 300mb of space to install the Coq proof assistant.) There will be short exercises that the audience can complete at their own pace which will not be vital to the theory but rather are intended to familiarise the audience with the proof assistant and tactics.

Title: Introduction to univalence in Coq III
Abstract: This week we continue our sequence of talks on homotopy type theory (HoTT) for which we are approaching the denouement. First we define h-propositions and what it means to be a contractible type. Then we distinguish between a couple of different types of equivalence and show that a particular choice satisfies all the conditions for being an h-proposition. If we have time we will formulate the univalence axiom and make some straightforward deductions that illustrate its use.
The audience is encouraged to follow the development of the theory on their own computers so please bring a laptop if you want to do this! (You will need about 300mb of space to install the Coq proof assistant.) There will be short exercises that the audience can complete at their own pace which will not be vital to the theory but rather are intended to familiarise the audience with the proof assistant and tactics.

Title: Introduction to univalence in Coq II
Abstract: This week we continue our sequence of talks on homotopy type theory (HoTT). We will introduce some more tactics and work towards the univalence axiom.
The audience is encouraged to follow the development of the theory on their own computers so please bring a laptop if you want to do this! (You will need about 300mb of space to install the Coq proof assistant.) There will be short exercises that the audience can complete at their own pace which will not be vital to the theory but rather are intended to familiarise the audience with the proof assistant and tactics.

Title: Introduction to univalence in Coq
Abstract: This week we begin a sequence of talks on homotopy type theory (HoTT). In this first talk we introduce the elementary definitions and tactics that are required to get started with HoTT using the Coq proof assistant. We endeavour to introduce as little programming syntax as possible and develop the theory using only a very few syntactic constructs that have clear mathematical interpretations.
The audience is encouraged to follow the development of the theory on their own computers so please bring a laptop if you want to do this! (You will need about 300mb of space to install the Coq proof assistant.) There will be short exercises that the audience can complete at their own pace which will not be vital to the theory but rather are intended to familiarise the audience with the proof assistant and tactics.

Title: Every CDC embeds into the coKleisli category of a monoidal differential category
Abstract: The coKleisli category of a monoidal differential category is always a Cartesian differential category. However, it seems that not every CDC arises this way. In the category of smooth maps between finite dimensional real vector spaces, there does not appear to be a “bang” on the subcategory of linear maps, as the “bang” should give rise to an infinite dimensional space. However, the question of whether any CDC embeds into a coKleisli category of some monoidal differential category has been floating around for a while. This talk will address this question directly.

Title: A structural definition of symmetric multicategories
Abstract: Symmetric multicategories are a basic structure in the categorical semantics of linear logic. One can define them elementarily, but already the coherence are difficult to track. The problem compounds when one tries to define functors and natural transformations to get a 2-category of symmetric multicategories, which is necessary for stating properly 2-categorical theorems like coherence. I will give a structural definition of symmetric multicategories based on profunctors which will provide the basic definition upon which the 2-category of symmetric multicategories can be built.