Semantics
Tuesday December 6, 2022, 10:30AM, Salle 1007
Ariadne Si Suo (University of Oxford) Semiring Tensor and Iteration Theory
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.
Semantics
Friday November 25, 2022, 10:30AM, Salle 3052
Marco Abbadini (Université de Salerno) A generalization of de Vries duality to closed relations between compact Hausdorff spaces
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).
Semantics
Monday November 14, 2022, 2PM, Salle 3052
Floris Van Doorn (Université de Paris Saclay) Formalizing sphere eversion in Lean
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.
Semantics
Tuesday September 27, 2022, 10:30AM, Salle 3052
Rick Blute (University of Ottawa) Finiteness Spaces and Monoidal Topology
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.
Semantics
Monday September 26, 2022, 2PM, Bâtiment Sophie Germain, salle 1007
Marek Zawadowski (Université de Varsovie) Polynomial and analytic functors, revisited
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.
Semantics
Tuesday June 28, 2022, 9:30AM, Salle 3052
Eigil Fjeldgren Rischel (University of Strathclyde) An invitation to categorical cybernetics
Attention à l'horaire inhabituel
Semantics
Monday May 9, 2022, 4:30PM, Exposé en ligne depuis San Diego sur galene
Chaitanya Leena Subramaniam (University of San Diego) The higher universal algebra of dependently typed theories
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.
Semantics
Tuesday May 3, 2022, 4:30PM, Exposé en ligne depuis San Diego sur galene
Chaitanya Leena Subramaniam (University of San Diego) The universal algebra of dependently typed theories
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.
Semantics
Tuesday April 5, 2022, 10:30AM, Salle 3052
Najwa Ghannoum (Université de Nice) Classification of finite categories with grouplike endomorphism monoids
Semantics
Monday March 28, 2022, 11AM, Salle 3052
Sylvain Douteau (Stockholm University) Théories de l'homotopie stratifiées et équivalences de Kan-Quillen stratifiées.
Semantics
Monday March 28, 2022, 9:30AM, Salle 3052
Pierre-Alain Jacqmin (Université catholique de Louvain) Propriétés d'exactitude stables par pro-complétion