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

• December 16, 2:30pm - 4:00pm, in 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, 2:30pm - 4:00pm, in HFG 7.07

  Canceled

  Canceled

• November 18, 2:30pm - 4:00pm, in 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, 2:30PM-4:00PM, in 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, 2:30PM-4:00PM, in 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, 2:30PM-4:00PM, in 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.