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

  TBA

  TBA

• 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.