Statement on Black Lives Matter
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.
Title: Linearisation of infinity categories
Abstract: In a paper on the Goodwillie calculus Lurie defines a linearisation procedure that forms a map of infinity bi-categories. In this talk we show how this result transfers into the 2-categorical setting for quasi-categories developed by Riehl and Verity. If we have time we sketch how to express a tangent bundle pseudo-functor in terms of the linearisation pseudo-functor.
Title: The differential lambda-calculus: syntax and semantics for differential geometry
Abstract: This talk will introduce semantics for the differential lambda-calculus using tangent categories. We will show how to obtain models of the differential lambda-calculus that stem from differential geometry. We will also explore the coherence required for tangent categories to model the differential lambda-calculus from different points of view.
Title: Operad structures in abelian functor calculus
Abstract: Abelian categories are a cartesian differential category, and the derivative corresponds to the same derivative which is used in functor calculus (a branch of homotopy theory). In 2011, Cockett and Seely showed that any Cartesian differential category has a higher-order chain rule for the derivative.
B. Johnson, S. Yeakel and I have identified this higher order chain rule in the abelian functor calculus example. Furthermore, we have shown that a consequence of the higher-order chain rule is that higher order derivatives of a functor of R-modules form an operad (a monoid in the category of symmetric sequences). The existence of this operad was predicted by a similar result for functors of topological spaces (discovered by G. Arone and M. Ching). In the case of abelian calculus, we have identified this operad as a consequence of the existence of a (lax) functor from abelian categories to the category Faa(AbCat), as defined by Cockett and Seely. We see our result as a kind of translation between the homotopy theoretic and category theoretic results.
In this talk, I will define the abelian functor calculus derivative, explain the higher order chain rule and produce the resulting operad.
Title: A Tangent Category of Fibrant Objects
Abstract: We shall consider Getzler and Behrend’s construction of a category of fibrant objects from a descent category in the setting of tangent categories. This will generate a category of fibrant objects with a well defined tangent structure. A particularly important class of objects will be those equipped with an infinite family of higher order horizontal connections.
