Differential categories provides the categorical semantics of differential linear logic. In particular, differential categories come equipped with an exponential modality, which categorically speaking is a comonad, and where the differential structure is captured by a natural transformation called the codereliction. CoKleisli categories of differential categories are well studied, they are Cartesian differential categories, or in other words, categorical models of the differential lambda calculus. On the other hand, coEilenberg-Moore categories of differential categories (.i.e the category of coalgebras of the comonad) are less-well studied.

In this talk, we will take a look at the coalgebras of a differential category and explain how to construct coderelictions from coalgebra structure, which results in a new axiomatization of differential categories. This new axiomatization helps provide an alternative proof that free exponential modalities always come equipped with a unique codereliction, and thus every Lafont category with biproducts is a differential category. We will also explain how, under a mild limit condition, the coEilenberg-Moore category of differential category is in fact a tangent category! Tangent categories formalize the basis of differential calculus on smooth manifolds. Thus, the coalgebras of a differential category can be seen as generalized smooth manifolds, while the cofree coalgebras are interpreted as generalized Euclidean spaces.

This talk is based on and is an extension of a paper by Cockett, Lucyshyn-Wright, and Lemay: https://drops.dagstuhl.de/opus/volltexte/2020/11660/pdf/LIPIcs-CSL-2020-17.pdf

In 'A practical type theory for symmetric monoidal categories’ M. Shulman presents a type theory in which we may reason about symmetric monoidal categories as if they were categories of 'sets with elements' with one major caveat: whereas in Set elements of products are 'decomposable', terms of product types in PTT are 'not necessarily decomposable’.

In this talk I will:

-) motivate Shulman’s PTT and provide an introduction to that theory; and

-) describe progress towards a similar type theory for symmetric monoidal bi-categories.

In particular, in this second part:

+) I will compare the role played by nice presentations, PROPs, and signatures in the semantics of PTT to the role played by (generalized) 2- and 3-computads for (the globular operad for) quasi-strict symmetric monoidal bi-categories; and

+) introduce the basic judgements of our proposed syntax - along with their ‘sets with elements’ style interpretation

You will find more on Paul Lessard's work here: https://sites.google.com/view/paul-roy-lessard

The goal of this work is to get a better understanding of the type Sn=Sn where Sn is the sphere of dimension n, inductively defined by repeated suspensions. I will first prove in full details that S1=S1 is equivalent to S1+S1 (the disjoint sum of two copies of the circle), and explain why it is highly unrealistic to conjecture a straightforward generalization for Sn. However, part of the argument for S1 can be extended in higher dimensions to prove that Sn=Sn has two equivalent connected components, one centered at the identity function and one centered at its “opposite” (to be defined properly during the talk). This generalization is done by induction on n, and the case n=1 does not constitutes a good base case. Consequently I will detail the case n=2 (interesting in its own), and sketch the induction step for n>3. This is joint work with M.Bezem and N.Kraus.

We discuss a simple Turing-complete extension of first-order logic FO. The extension adds two new features to FO. The first one of these is the capacity to add new points to models and new tuples to relations; the corresponding deletion operators are also introduced. The second new feature is a construct that allows formulae to refer to themselves. We survey some of the principal properties of this logic and its extensions with, e.g., generalized quantifiers.

The General Adjoint Functor Theorem of Freyd has a straightforward extension to the enriched setting. There is also a Weak Adjoint Functor Theorem, due to Kainen, and providing a sufficient condition for the existence of a weak left adjoint, where weakness refers to the existence but not uniqueness of factorizations. I will report on recent joint work with Steve Lack and Lukas Vokrinek, in which we prove a weak adjoint functor theorem in the enriched context. This actually contains the other three theorems as special cases. Our base for enrichment will be a monoidal model category. Our motivating example involves simplicially enriched categories, where the base category of simplicial sets is equipped with the Joyal model structure. The theorem then has applications to the Riehl-Verity theory of infinity-cosmoi.

Cet exposé sera une introduction à l'algèbre linéaire graphique (graphical linear algebra), un langage qui permet de raisonner de façon compositionnelle à propos de système R-linéaires, pour divers semi-anneaux R. Lorsque que R est un corps, sa sémantique et sa théorie équationnelle sont bien comprises. Dans ce contexte, l'algèbre linéaire graphique est proche des signal flow graphs, un autre langage communément utilisé en théorie du contrôle pour spécifier des systèmes dynamiques au comportement linéaire. Des travaux récents ont montrés que, pour R = ℕ, la même syntaxe graphique permet de spécifier des systèmes concurrents qui manipulent des ressources discrètes. On obtient alors un langage suffisamment expressif pour y encoder très naturellement tous les réseaux de Petri et raisonner de façon modulaire à propos de leur comportement. Nous donnerons des axiomatisations complètes pour ces différentes interprétations et étudierons leurs extensions affines.

Il s'agit de travaux en collaboration avec Filippo Bonchi, Pawel Sobocinski et Fabio Zanasi.