Event categories Archives:

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 […]

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 […]

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 […]

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 […]

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 […]

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 […]

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, […]

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 […]

Title: Elements of the Theory of Quasi-categories Abstract: We outline some of the theory of quasi-categories that is required to set up the functor calculus. First we review the definition of left, right and inner factorisation systems and describe an alternative characterisation of these factorisation systems that makes certain computations more straightforward. Then we define […]

Title: A Two Dimensional Setting for the Calculus of Infinity Functors: Part II Abstract: In this talk we continue describing the calculus of infinity functors in terms of derivators. First we recall what a derivator is, the basic examples of derivators, the definition of Cartesian square and what it means to be an excisive morphism […]