Seminars

The aim of this talk is to express the fully algebraic theory of monoidal bicategories as developed in the 1990's by Kapranov-Voevodsky, Baez-Neuchl, Day-Street and many others in the essentially homotopical language of higher algebra as developed in the 2010's by Lurie. We show that the theory of E_n-operads, which originates from May's geometric classification of $n$-fold loop spaces, provides a convenient way to handle concepts in both areas.

Indeed, we prove that braided, sylleptic and symmetric monoidal bicategories, in the sense of Day and Street, are exactly the E_n-algebras, for $n = 2, 3, 4$, respectively, in the sense of Lurie.

The proof of this result involves a study of the infinity-category of bicategories and subsequent subtle considerations on partial homotopy-coherent associative structures known as A_n-algebras. As an application, we give a conceptual proof of the bicategorical version of the fact that monoids in a (symmetric) braided monoidal category form a (braided, and in fact symmetric) monoidal category.

In this talk, I will introduce the theory of scroll nets, which is a novel diagrammatic formalism for representing proofs and programs. As the name indicates, it is based on the « scroll », a notation for logical implication invented by Charles S. Peirce at the end of the 19th century for his system of existential graphs, to which it adds a graphical syntax inspired by proof nets to represent inference rules. I will first motivate the notation from a philosophical standpoint, arguing that it captures the smallest motions of deductive reasoning in the most natural way. I will then show how it captures minimal implicative logic by simulating the rules of natural deduction. Through the Curry-Howard correspondence, this will lead us to identify a notion of detour/redex that generalizes that of simply-typed λ-calculus, making scroll nets into an expressive computational framework. If time remains, I will illustrate how to capture classical logic, as well as intuitionistic disjunction and co-implication by considering horizontal and vertical generalizations of the scroll.

We investigate the connection between automata theory and λ-calculus in terms of syntax, semantics and logic. A starting point for this investigation is Salvati’s notion of language of λ-terms recognized by a cartesian closed category, which generalizes to the higher-order setting the usual regular languages of finite words and trees.

First, we extend Salvati’s work by showing that all well-pointed, locally finite non-posetal cartesian closed categories recognize the same languages of λ-terms as the category of finite sets, which we call higher-order regular languages. In turn, we extend the syntactic approach of Hillebrand and Kanellakis to the higher-order setting, and show that the obtained languages coincide with higher-order regular languages, hence connecting our work to the implicit automata research program of Nguyễn and Pradic. This demonstrates the robustness of the notion of higher-order regular language.

Second, we take inspiration from ideas coming from Stone duality and introduce profinite λ-terms, a higher-order generalization of the notion of profinite word. The space of profinite λ-terms can be equivalently described in three ways: as a metric completion, as the Stone dual of the Boolean algebra of higher-order regular languages, and through parametricity à la Reynolds. Profinite λ-terms assemble into a cartesian closed category that verifies a universal property with respect to certain Stone-enriched categories; this amounts to a semantic interpretation of the profinite λ-calculus.

Recent developments in higher category theory suggest a directed form of algebraic topology or homotopy theory. In this framework, one studies (pointed) (∞,∞)-categories in place of (pointed) spaces, directed analogues of the loop–suspension adjunction, categorical spectra equipped with the Gray smash product, stable Gray categories,... (see e.g. [https://nmasuda2.github.io/notes/thesis_stable.pdf], [arXiv:2505.22640], [arXiv:2508.16787]).

A key ingredient in the theory of “directed spaces” (=(infty,infty)-categories) is the notion of fibrations (in the sense of a Grothendieck construction). For (∞,1)-categories, (co)cartesian fibrations admit a clean internal formulation via relative adjunctions. For (∞,n)-categories (including n = ∞), a definition of fibrations also exists (e.g. arXiv:2108.11431, arXiv:2307.11931) but one lacks a definition that can be given internally. We conjecture that just as adjunctions govern fibrations in the (∞,1) world, lax n-adjunctions may be used to give an internal definition of fibrations in the (∞,n) world. This would yield a notion of higher fibrations internal to any (∞,n+1)-category (with the right limits), and potentially enable the definition of higher Grothendieck topoi via fibrational descent (cf. [arXiv:2410.02014] for the (∞,2)-case).

In this talk, we will review the basics of (∞,∞)-categories, sketch a definition of lax n-adjunctions and the walking lax ∞-adjunction, and indicate how these structures relate to fibrations. Time permitting, we will also discuss analogues of this in a Gray setting (aka (∞,∞,1)-categories).

This is based on work in progress with Marcus Nicolas.

There is a huge variety of objects which deserve the name "dynamical system". Most important types fit into the framework called "double categorical systems theory", developed by Myers. In this framework, the trajectories of a dynamical systems are defined to be the homomorphisms of systems out of specified "clock systems" - for example, a trajectory of a discrete dynamical system is a homomorphism out of the dynamical system (N,+1). Describing clock systems for notions deterministic dynamical system is relatively straightforward, but their description for stochastic systems is more complicated. For discrete-time stochastic dynamical systems - that is, Markov chains - this was recently resolved, but the solution does not apply to continuous-time stochastic processes, such as SDEs (stochastic differential equations). In addition to giving an introduction to all of the preceding, I'll present some work in progress on defining clock systems for SDEs.

Whenever an algebraic structure is defined via a presentation A = < X | R>, a fundamental question arises: how can we tell if two elements generated from X are equal as elements in A? For commutative algebras, this was answered by Buchberger more than fifty years ago, using Gröbner bases. His seminal work has since been applied to many “classical” linear algebraic structures, including associative algebras.

In this talk, we explain how to extend Gröbner bases to linear 2-categories, taking insights from higher rewriting theory. Our approach is rooted in practical problems coming from representation theory and low-dimensional topology. We will emphasize differences with the classical setting as well as open directions of research.

In this talk, I will present my MSc Thesis work on the homotopy theory of equilogical spaces, motivated by the search for models of impredicative univalent type theory. The category of equilogical spaces is equivalent to the subcategory of modest sets in a realizability topos, which in particular makes it a model of impredicative type theory. But equilogical spaces furthermore admit a simple definition as (T0, countably-based) topological spaces equipped with equivalence relations, so in particular also carries homotopical content via the topology, i.e. where the notion of homotopy is induced by the real unit interval [0, 1] in the usual way. Therefore, (one wishes that) a homotopy theory of equilogical spaces should yield a model of impredicative univalent types.

It turns out that the category of equilogical spaces (and also its enveloping realizability topos) is already a homotopy category where the equivalence relation gives the notion of path. So a proper treatment of the homotopy theory of equilogical spaces requires us to “fuse” two notions of path: one given by the equivalence relation, and the other one given by the topology. I will present my attempts at constructing a homotopy theory fusing these two. Along the way, I also explore the homotopy theory of QCB (Quotient of Countably-Based) spaces, which are exactly the topological spaces obtaining by sending an equilogical space (X, ~) to its resulting quotient X/~. Here, I obtain a Quillen model structure on QCB spaces in which the weak equivalences are homotopy equivalences. This model structure looks exactly like the Strøm model structure on the category of topological spaces.