This talk is about the semantics of commutative combinations of effects.

A basic class of effects comes from the algebraic theory of modules for a semiring. The tensor of such theories is determined by the usually more tractable semiring tensor. I’ll give some examples, and then look at how the tensors work in languages with iteration. Our main contribution concerns an important class of subtheories of module theories. We observe that the subtheory tensor is also determined by the semiring tensor for several fundamental effects. I'll look at some examples of these subtheories and their tensors, and discuss how they support iteration via the underlying subsets.

This is my undergraduate summer project with Cristina Matache, Sean Moss, and Sam Staton.

De Vries (1962) obtained a categorical duality for the category KHaus of compact Hausdorff spaces and continuous functions. The objects of the dual category DeV are complete boolean algebras equipped with a proximity relation, known as de Vries algebras, and the morphisms are functions satisfying certain conditions. One drawback of DeV is that composition of morphisms is not usual function composition.

We propose an alternative approach, where morphisms between de Vries algebras are certain relations and composition of morphisms is usual relation composition. This gives a solution to the aforementioned drawback of DeV. The usage of relations as morphisms between de Vries algebras allows us to extend De Vries duality to a duality for the larger category of compact Hausdorff spaces and closed relations, solving a problem raised by G. Bezhanishvili, D. Gabelaia, J. Harding, and M. Jibladze (2019).

I will discuss the strong connections with the literature on domain theory, in particular with the notions of R-structures, information systems and abstract bases (Smyth, Scott, Abramsky, Jung, Vickers), and with other duality theoretical results (Jung, Sünderhauf, Kegelmann, Moshier).

Lean's mathematical library mathlib is a rapidly growing unified library of formalized mathematics, with over 1 million lines of code. The library contains most of an undergraduate math curriculum, and many graduate topics. It is used as a basis to formalize advanced results in mathematics.

One such result is the sphere eversion project, a formalization that shows that you can turn a sphere inside out without creasing or tearing it. We prove sphere eversion as a corollary of a much deeper theorem in differential topology, the h-principle, proven by Mikhael Gromov in 1973. The h-principle (or homotopy principle) roughly states that the only obstructions to the existence of a solution to a partial differential relation come from algebraic topology, e.g. because there is some algebraic invariant that prevents any solution from existing. This project is a collaboration of Patrick Massot, Oliver Nash and me.

Much of my recent research has been in demonstrating the idea that working with Ehrhard's notion of finiteness space forces certain sums which would a priori be infinite to become finite, and hence well-defined, without resorting to limit structure or infinitary computations. It is hoped that this will lead to a great many applications, and that one of those applications is in the field of monoidal topology. Typically monoidal topology takes place in the category of quantale-valued relations.

In this talk, we'll briefly review some previous results which demonstrate the utility of finiteness spaces in the types of settings we are considering and then introduce monoidal topology, and finally consider possible extensions of monoidal topology via finiteness spaces. By using Ehrhard's linearization construction, we can instead consider relations on finiteness spaces which take values in a positive partially ordered semiring. In particular, we no longer require infinitary operations. This type of semiring is important in the theory of weighted automata among other places.

In my talk I will show that some versions of operads/multicategories (non-Sigma, symmetric, with amalgamations) and finitary polynomial and analytic functors, i.e., the devices that have been used to define opetopic sets by various authors, are either very closely related or even two sides of the same coin, if placed in the suitable context. These structures have been used in many contexts and not always with the understanding to what extent they are similar.

I will start with some easy examples showing how these structures can be related to one another in the category Set. It turns out that polynomial functors and monads are related to Kleisli algebras, whereas analytic functors and monads are related to Eilenberg-Moore algebras for the same monad.

Then I will show that in fact this kind of structures and relations between them can be constructed in any 2-category with some mild completeness properties, whenever a lax monoidal monad sits inside it.

Over the past ~5 years, a number of authors trying to apply methods from category theory to game theory, machine learning, and dynamical systems, have noticed a strong convergence. It seems that very similar categorical structures emerge from the study of all of these things, centering around the notion of /lens/. I'll give a survey of this research program and sketch some recent advances.

Two syntactic classes of theories play preponderant rôles in traditional category-theoretic universal algebra: algebraic (a.k.a. “Lawvere” or “Lawvere-Bénabou”) theories, and essentially algebraic theories (introduced by Freyd). Models of the former are precisely Set-based algebraic structures that can be defined using finite products, while those of the latter are Set-based algebraic structures that can be defined using finite limits. Theories in each of these classes are defined using simple (i.e. non-dependent) sorts, and the generalisation from Lawvere-Bénabou theories to essentially algebraic theories involves allowing certain partial functions in addition to total functions. A different approach involves replacing the simple sorts of Lawvere-Bénabou theories with dependent types, while continuing to allow only total functions, such as in Cartmell's notion of generalised algebraic theory (GAT). Indeed, many algebraic structures defined using finite limits (such as categories) have more natural descriptions by GATs than by EATs. However, much of the elegant universal algebra of Lawvere-Bénabou theories, such as their equivalent description as monads, cannot be recovered for GATs (“GATs are a bit too general”).

In this talk, I will define “dependently typed algebraic theories” (DTTs), a strict subclass of GATs for which all of the universal algebra of Lawvere-Bénabou theories generalises perfectly. Happily, the GATs describing many familiar algebraic structures (such as algebraic n-categories and n-groupoids, n ≤ ∞) are DTTs. Moreover, we will see that every kind of Set-based algebraic structure defined using finite limits can be classified by (i.e. has a syntactic description in the form of) some DTT. DTTs are especially important in the context of Martin-Löf Type Theory, since they correspond to algebraic definitions admissible within this syntactic framework.

Two syntactic classes of theories play preponderant rôles in traditional category-theoretic universal algebra: algebraic (a.k.a. “Lawvere” or “Lawvere-Bénabou”) theories, and essentially algebraic theories (introduced by Freyd). Models of the former are precisely Set-based algebraic structures that can be defined using finite products, while those of the latter are Set-based algebraic structures that can be defined using finite limits. Theories in each of these classes are defined using simple (i.e. non-dependent) sorts, and the generalisation from Lawvere-Bénabou theories to essentially algebraic theories involves allowing certain partial functions in addition to total functions.

A different approach involves replacing the simple sorts of Lawvere-Bénabou theories with dependent types, while continuing to allow only total functions, such as in Cartmell's notion of generalised algebraic theory (GAT). Indeed, many algebraic structures defined using finite limits (such as categories) have more natural descriptions by GATs than by EATs. However, much of the elegant universal algebra of Lawvere-Bénabou theories, such as their equivalent description as monads, cannot be recovered for GATs (“GATs are a bit too general”).

In this talk, I will define “dependently typed algebraic theories” (DTTs), a strict subclass of GATs for which all of the universal algebra of Lawvere-Bénabou theories generalises perfectly. Happily, the GATs describing many familiar algebraic structures (such as algebraic n-categories and n-groupoids, n ≤ ∞) are DTTs. Moreover, we will see that every kind of Set-based algebraic structure defined using finite limits can be classified by (i.e. has a syntactic description in the form of) some DTT. DTTs are especially important in the context of Martin-Löf Type Theory, since they correspond to algebraic definitions admissible within this syntactic framework.

Counting associative structures has been presented for many years in different applications and techniques, for examples counting finite groups, semigroups and monoids, etc.. In our work, we extend the count to finite categories. Our aim is to analyze the structure of finite categories, and develop structure theorems for these. We use McCune's Prover9/Mace4 to construct models, providing in particular a count of the number of categories with two non-isomorphic objects and such that all hom-sets have size 3. As a result of our counting, we obtain that the algebraic structure of monoids in categories is very important in the classification problem. For example, we will present a classification of a specific kind of monoids called “grouplike”, these are monoids that contain a group plus an ordered set of identities. Studying grouplike categories clarifies greatly the enumeration question and the numbers that are obtained from the counting.

On appelle équivalence de Kan-Quillen l'équivalence de Quillen entre ensembles simpliciaux et espaces topologiques donnée par l'adjonction entre realisation géométrique et ensemble simplicial des simplexes singuliers. L'équivalence entre ces deux catégories modèles est un résultat fondateur de la théorie de l'homotopie. Une bonne notion de théorie de l'homotopie stratifiée devrait reproduire ce résultat. Dans cet exposé, je présenterai la construction de catégorie modèles d'espaces et d'ensembles simpliciaux stratifiés, et j'expliquerai pourquoi l'équivalence de Kan-Quillen, dans ce contexte, n'est obtenue que sous la forme d'une équivalence entre catégories infinies.

La pro-complétion, et sa duale la ind-complétion, jouent des rôles majeurs en informatique théorique, en théorie des catégories et en géométrie algébrique notamment. L'exemple type est la catégorie des espaces de Stone qui est la pro-complétion de la catégorie des ensembles finis. Dans la littérature, il a été montré que quelques propriétés se transfèrent d'une catégorie à sa pro-complétion. C'est le cas des propriétés d'être une catégorie régulière, co-régulière, additive, abélienne ou encore extensive. Dans cet exposé, nous formulerons un théorème qui englobe tous ces résultats et donne pléthore de nouveaux exemples. Appliqué à la catégorie des ensembles finis, nous en déduirons que la catégorie Stone est cohérente, extensive, distributive, régulière, co-régulière, co-arithmétique, co-Mal'tsev, co-protomodulaire etc. Afin d'énoncer le théorème principal, nous introduirons une notion de séquents d'exactitude, qui permet d'encoder une grande variété de propriétés catégoriques. Cet exposé est basé sur un travail en collaboration avec Zurab Janelidze