About

The category theory seminar runs every other week at Utrecht University. Here category theory is understood in a broad sense, and topics can include higher category theory, applications to homotopy theory and computer science, among other things. The sessions will take up to 1h30m, including questions.

If you would like to give a talk, please talk to me or Léonard.

Schedule

• March 30, 2026 ❘ 11:00am - 12:30pm ❘ HFG 7.07

  Léo Hubert - Grothendieck's test categories and the Dold-Kan correspondence

  Grothendieck's theory of test categories allows to characterize small categories with the property that an appropriate localization of their categories of presheaves modelize the homotopy category of spaces. Presheaves on test categories then allows to do homotopy theory just as well as traditional simplicial sets can. However, simplicial sets exhibit other niceties. Among them is the Dold-Kan correspondence: simplicial abelian groups are equivalent to non-negative chain complexes of abelian group, and therefore are also a model for homology types. In this talk I will introduce, following Grothendieck's work in Pursuing Stacks, a homotopical version of the Dold-Kan correspondence and show that it is satisfied for a wide class of test categories, including Joyal's category Θ.

• March 16, 2026 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Francesca Pratali - On operads and pre-coCartesian operads

  Operads, or multicategories, can be viewed as a generalization of categories, in which morphisms are allowed multiple inputs but a single output. They play a fundamental role in describing categories of algebras and multiplicative structures on categories. Symmetric monoidal categories provide a classical source of examples of operads, where multivariable morphisms are represented via the tensor product. Operads, however, encode a broader range of multiplicative structures where multimorphisms need not be representable. In particular, the class of pre-coCartesian operads sits strictly between the two, encoding monoidal-like structures with only a partially defined monoidal product. In this talk, we compare these three structures via a chain of forgetful functors and their left adjoints. The central question is whether the classical envelope functor factors through pre-coCartesian operads, and what this reveals about the interplay between partial monoidal structures and full representability.

• March 2, 2026 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Benno van den Berg - Effective Kan fibrations

  In an attempt to give a constructive account of the Kan-Quillen model structure on simplicial sets, Eric Faber and I defined a notion of an "effective Kan fibration". Roughly speaking, an effective Kan fibration is a map of simplicial sets which comes with a specified solution for each lifting problem against a horn inclusion, where these solutions are also expected to satisfy a certain compatibility condition. In a classical metatheory every Kan fibration can be equipped with such a structure; however, this definition is stronger than the usual one in a constructive metatheory, and allows us to give constructive proofs of results such as the following: if A is an effective Kan complex, then so is A^B for each simplicial set B, which cannot be shown constructively for "standard" Kan complexes. I will give an idea of what we have proved so far about these effective Kan fibration and what still remains to be done.

• June 20, 2025 ❘ 1:15pm - 2:45pm ❘ HFG 7.07

  Freek Geerligs - A foundation for synthetic dualities

  In synthetic algebraic geometry, an axiom system is presented to study the Zariski topos internally. The axioms are on a duality between rings and (affine) schemes. This talk is on a variant of synthetic algebraic geometry called synthetic Stone duality. We present an axiom system where the rings will be replaced by countably presented Boolean algebras, the affine schemes by Stone spaces, and the schemes by compact Hausdorff spaces. We conjecture these axioms describe the internal results in the topos of light condensed sets. We define a type of open propositions, inducing a synthetic topology on each type. For Stone and compact Hausdorff spaces, this topology is as expected. From the axioms, we can decide Bishop's omniscience principles. In particular, we can show every map from the interval to itself is continuous in the epislon-delta sense. We can also show Brouwer's fixed-point theorem. This talk is based on a paper submitted to TYPES24 (https://arxiv.org/abs/2412.03203), which was authored by Felix Cherubini, Thierry Coquand, Freek Geerligs and Hugo Moeneclaey. The paper is part of the synthetic algebraic geometry project (https://github.com/felixwellen/synthetic-zariski).

• June 3, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Paige North - The enriched Curry-Howard-Lambek correspondence

  I will talk about developments of type theory with semantics in enriched categories. Category theory has gained a lot of flexibility and expressive power by enlarging its domain of study to include enriched categories. On the other hand, the Curry-Howard-Lambek correspondence is the basis for much of modern type theory and categorical logic: it connects logic to the simply typed lambda calculus which then is seen as the internal language for cartesian closed categories. In this talk, I will describe an “enriched” simply typed lambda calculus which is an internal language for enriched cartesian closed categories. I will also describe a corresponding logic (generalizing the Curry-Howard correspondence). There will be a running example of intuitionistic fuzzy logic, and if time permits I will also describe other potential applications to directed type theory and domain theory.

• May 20, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Canceled

  Canceled

• May 6, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Tom de Jong - Epimorphisms and acyclic types

  Homotopy type theory (HoTT) is a foundation for mathematics where spaces (in the form of types) as opposed to sets are taken as primitive objects. A natural question is what epimorphisms look like in this foundation. After introducing a homotopically well behaved definition of epimorphism, we characterize the epimorphisms as the fiberwise acyclic maps. Classically, a space is said to be acyclic if its reduced homology vanishes. An equivalent definition, which we adopt in HoTT, is that the suspension of the space is contractible. We illustrate our synthetic approach by showing how to obtain results and examples via simple techniques from (higher) category theory as opposed to traditional methods (such as homology calculations). This talk is based on joint work with Ulrik Buchholtz and Egbert Rijke (Epimorphisms and acyclic types in univalent foundations. The Journal of Symbolic Logic 2025. https://doi.org/10.1017/jsl.2025.76).

• April 22, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Niels van der Weide - The Univalence Maxim and Univalent Double Categories

  Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating not just objects, but also morphisms capturing interactions between objects. It has influenced areas of computer science such as automata theory, functional programming, and semantics. Of particular importance in some applications are double categories, which are categories with two classes of morphisms, axiomatizing two different kinds of interactions between objects. These have found applications in many areas of mathematics and theoretical computer science, for instance, the study of lenses, open systems, and rewriting. However, double categories come with a wide variety of equivalences, which makes it challenging to transport structure along equivalences. To deal with this challenge, we propose the univalence maxim: each notion of equivalence of categorical structures has a corresponding notion of univalent categorical structure which induces that notion of equivalence. We also prove corresponding univalence principles, which allow us to transport structure and properties along equivalences. In this way, the usually informal practice of reasoning modulo equivalence becomes grounded in an entirely formal logical principle. We apply this perspective to various double categorical structures, such as (pseudo) double categories and double bicategories. Concretely, we characterize and formalize their definitions in Rocq UniMath up to chosen equivalences, which we achieve by establishing their univalence principles.

• April 8, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Léonard Guetta - Lax Functoriality of the Grothendieck construction for ω-Categories (Part 2)

  In this talk, I will present recent joint work with Dimitri Ara on the generalization of the Grothendieck construction to ω-categories, focusing on its functorial properties. In order to do so, we had to work within the realm of lax Gray ω-categories—higher categories in which the interchange law holds only up to a non-invertible cell. Despite the technical nature of this topic, I will assume only a basic familiarity with category theory and will introduce all the necessary notions. I will also highlight how these ideas arise naturally within the broader landscape of higher category theory. Reference: arXiv:2503.08832

• March 25, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Léonard Guetta - Lax Functoriality of the Grothendieck construction for ω-Categories

  In this talk, I will present recent joint work with Dimitri Ara on the generalization of the Grothendieck construction to ω-categories, focusing on its functorial properties. In order to do so, we had to work within the realm of lax Gray ω-categories—higher categories in which the interchange law holds only up to a non-invertible cell. Despite the technical nature of this topic, I will assume only a basic familiarity with category theory and will introduce all the necessary notions. I will also highlight how these ideas arise naturally within the broader landscape of higher category theory. Reference: arXiv:2503.08832

• March 11, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Canceled

  Canceled

• February 11, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Canceled

  Canceled

• February 11, 2025 ❘ 3:00pm - 4:30pm ❘ HFG 7.07

  Remy van Dobben de Bruyn - Pretopoi and profinite Galois theory

  Grothendieck's Galois theory sets up an analogy between covering space theory in topology and the Galois theory of fields. After briefly explaining the historical motivation, I will explain an extension of these results to pretopoi with a finite jointly conservative family of fibre functors (models). This gives a quick proof of a (simplified but more computationally feasible) version of the exodromy theorem of Barwick-Glasman-Haine from 2018. Time permitting, I will also sketch the connection to Makkai's strong conceptual completeness theorem and Lurie's ultracategories.

• December 16, 2024 ❘ 2:30pm - 4:00pm ❘ HFG 7.07

  Niels van der Weide - The internal languages of univalent categories

  Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One of such theorems was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, ∑-types, and ∏-types. This theorem expresses that, up to adjoint equivalence, the internal language of locally Cartesian closed categories is extensional Martin-Löf type theory with dependent sums and products. In this talk, we prove the theorem by Clairambault and Dybjer for univalent categories, and we extend their biequivalence to various classes of toposes, among which are ∏-pretoposes and elementary toposes. Univalent categories give an interesting framework for studying internal language theorems of dependent type theory. This is because of the fact that univalent categories are identified up to adjoint equivalence, and that internal language theorems give us biequivalence for various classes of categories and theories. In addition, we shall see that univalence gives us several ways to simplify the necessary constructions and proofs, because it allows us to transfer properties and structure along equivalences for free. The results in this paper have been formalized using the proof assistant Coq and the UniMath library. The material in this talk is based on the preprint https://arxiv.org/abs/2411.06636.

• December 2, 2024 ❘ 2:30pm - 4:00pm ❘ HFG 7.07

  Canceled

  Canceled

• November 18, 2024 ❘ 2:30pm - 4:00pm ❘ HFG 7.07

  Alex Simpson - The random topos

  I'll talk about one particular Grothendieck topos, which is most straighforwardly defined as the topos of sheaves for the countable cover Grothendieck topology on a certain small category. Surprisingly, this topology is both canonical and dense, hence the topos is boolean. Its classical internal logic validates the axiom of dependent choice and also the existence of a translation-invariant measure, extending Lebesgue measure, defined on all subsets of the reals. The measure can be uniquely characterised by exploiting an intrinsic independence relation, closely related to the Day monoidal structure on the topos.

• November 4, 2024 ❘ 2:30PM-4:00PM ❘ HFG 7.07

  Paige North - Coinductive control of inductive data types

  In classical programming language theory, characterizing data types as initial algebras of an endofunctor that represents a specification of the data types is an important tool. In this work, we observe that the category of algebras of such an endofunctor is often enriched in its category of coalgebras. This enrichment carries strictly more information than the traditional, unenriched category. For example, when considering the endofunctor whose initial algebra is the natural numbers, we find that the enrichment encodes a notion of 'partial' homomorphism, while the unenriched category encodes only 'total' homomorphisms. We can also leverage this extra information to generalize the notion of initial algebras, following the theory of weighted limits.

• October 21, 2024 ❘ 2:30PM-4:00PM ❘ HFG 7.07

  Niek Mulleners - Example-Based Reasoning about the Realizability of Polymorphic Programs

  Parametricity states that parametrically polymorphic functions behave the same regardless of how they are instantiated. When developing polymorphic programs, Wadler’s free theorems can serve as free specifications, which can turn otherwise partial specifications into total ones, and can make otherwise realizable specifications unrealizable. We are interested in automating the process of computing the realizability of polymorphic programs specified by a set of monomorphic input-output examples. We restrict ourselves to those polymorphic programs that are natural transformations between strictly positive functors, allowing us to make use of the isomorphism between such programs and container morphisms (morphisms between polynomial endofunctors). By translating monomorphic input-output examples to constraints on container morphisms, we can compute the realizability of polymorphic programs implementing those examples.

• October 7, 2024 ❘ 2:30PM-4:00PM ❘ HFG 7.07

  Léonard Guetta - When Does Cocompleteness Imply Completeness? A Primer on the Theory of Total Categories.

  It is a well-known result in poset theory that a poset admitting all joins automatically admits all meets. While the straightforward generalization to categories is true—a category admitting all (possibly large) colimits also admits all (possibly large) limits—it is practically useless due to Freyd's famous result, which states that in such cases, the category is necessarily a poset. Therefore, standard examples of categories (Set, Ab, Grp, etc.) do not satisfy this property. However, the correct generalization of this poset result to category theory is the following: A totally cocomplete category (referred to as a "total category") is automatically complete. The goal of this talk is to introduce the elegant notion of a total category, a strong and natural cocompleteness property introduced by Street and Walters in 1978, which many standard categories possess. For example, all locally presentable categories are total. However, unlike local presentability—which is rarely self-dual (it is almost never the case that a category is both locally and co-locally presentable)—many categories are both total and cototal, synthesizing very nice and convenient (co)completeness properties that a category can have.