Fall 2023

TBA

Spring 2023

Seminar meets normally on Mondays at 1:30pm Pacific Time, in the math department Faculty Research Library (SH 169), located here (see the image below for instructions).

• February 20, 1:30pm: Christian Williams, “Category theory as Logic”  (Slides)
  
  Abstract

  We propose a unifying story and language of category theory.

  Categories form a bifibrant double category, aka “equipment”. This structure can be understood as a logic: categories and functors are types and terms, while profunctors and transformations are judgements and inferences.

  From this view, we propose a story of category theory as logic. There are three parts: Binary Logic (Rel), Matrix Logic (VMat), and Active Logic (VCat). We construct logics by forming categories as “matrices with composition”, and this defines the language of logic as the coend calculus.

  Then, we begin to explore metalogic. Just as a category is a matrix with composition, a bifibrant double category is a “matrix category” with composition. The triple category BDC is constructed in the same way as particular BDCs: a matrix construction followed by a monad construction. Hence we propose that the language of metalogic is the double coend calculus of BDC.

  Below, we outline the three-part story of category as logic.

  Binary Logic
  Sets and functions, relations and implications: Rel serves as a simple introduction to double categories as logics.

  Matrix Logic
  Beyond 0/1, a “relation” between types can contain all kinds of content. A monoidal bifibration provides a notion of “predicate” on a type, and Shulman’s “frame construction” forms a double category Mat(V) by defining a “relation” (horizontal morphism) to be a predicate on a pair of types.

  Active Logic
  In a “complete” logic, types contain the same content as relations. A *monad* in Mat(V) is a V-category, defining the double category VCat = Mnd(Mat(V)). What distinguishes this logic from dependent type theory of Mat(V) is that types *act* on relations, i.e. categories act on profunctors. The defines the coend calculus: judgements compose by a “bilinear existential”, and inference-homs form by a “natural universal”.

• February 27, 1:30pm: Jonathan Weinberger, “Synthetic fibered (∞,1)-category theory”
  
  Abstract

  Infinite-dimensional categories play an increasing role in various areas of mathematics, from homotopy theory and algebraic geometry to logic. Working with these objects is considered very ambitious since it already requires a lot of background in ordinary category theory to even make the basic definitions. Is there a more intrinsic way?

  In 2017, Riehl and Shulman proposed an extension of homotopy type theory (HoTT) to provide a language appropriate for this purpose. HoTT is an alternative foundational system in which the basic objects are not sets but spaces up-to-homotopy aka homotopy types, so the theorems intrinsically have homotopy-theoretic meaning. It is also particularly nice from a logical point of view since due to Voevodsky’s Univalence Axiom all theorems are automatically transported along isomorphisms between types which can be seen as homotopy equivalences. This allows one to do homotopy theory in a synthetic way. Adding Riehl–Shulman’s extensions to the theory gives rise to simplicial homotopy type theory (sHoTT). In the presence of this theory’s strict simplicial shapes such as the triangle, tetrahedron etc., it turns out one can reason synthetically about infinity-categories in a more native and genuinely homotopy invariant way.

  We present some results extending Riehl–Shulman’s work about fibrations of synthetic infinity-categories. The talk contains joint work with Ulrik Buchholtz as well as some of the speaker’s PhD thesis work.

• March 13, 10:00am: Thomas Jan Mikhail, “A Type Theoretic Definition of ω-Categories”
  
  Abstract

  In his thesis, partly inspired by Grothendieck’s definition Brunerie extracted from HoTT a minimal type theory describing an oo-groupoid. Finster and Mimram in turn, inspired by Brunerie’s work and Maltsiniotis’s generalization of Grothendieck’s definition to ω-categories developed a type theory describing an ω-category. In this talk we will start with a survey of Finster and Mimram’s type theory and then discuss a slight variation of the rules, with which the type theory acquires a more geometric flavor.

• March 27, 1:30pm: Christian Williams, “The triple category of categories”
  Abstract
• April 10, 1:30pm: Pierre Cagne, “Symmetries of groups in univalent foundations”
  
  Abstract

  In this talk, I will present a proof, in univalent foundations, of a theorem by Gottlieb, from 1965, on the space of self homotopy equivalences of the classifying space of a group: given a group G, the space of homotopy equivalences from its classifying space BG to itself has a connected component for each outer automorphism of G and each of these components is a classifying space for the center of G. The proof I will present is by no means revolutionary, but I hope to illustrate through it how univalent type theory is a natural fit for group theory.

• April 17, 10:00am: Eric Finster, “The Baez-Dolan +-Construction for Generalized Algebraic Theories”
  
  Abstract

  The Baez-Dolan +-construction is an operation on symmetric operads which produces, from a given operad O, a new operad O+ whose algebras are operads equipped with a map to O. Iteratively applying this construction to the identity operad, whose algebras are just sets, generates a family of polytopes (the “opetopes”) which play a central role in Baez and Dolan’s approach to higher algebra.

  In this talk, I will discuss the application of Baez-Dolan construction to arbitrary generalized algebraic theories and outline some possible applications.

• May 1, 9:00am: Paige Randall North, “Fuzzy type theory”
  
  Abstract

  In this talk, I will report on progress developing a fuzzy type theory, a project that started as part of the ACT 2022 Adjoint School. The motivation is to develop a logic which can model opinions, and we do this by generalizing Martin-Löf type theory. Martin-Löf type theory provides a system in which one can construct a proof (aka a term) of a proposition (aka a type), and we usually interpret such a term as saying that the proposition holds. Fuzzy type theory is a similar system in which one can provide or construct evidence (aka a fuzzy term) to support an opinion (aka a type), but the evidence (fuzzy term) comes with a parameter, for instance a real number between 0 and 1, which expresses to what extent the opinion holds. Martin-Löf type theory is closely related to category theory: from such a type system one can construct a category in which (very roughly) the types become objects and the terms become morphisms, and this can be made part of an equivalence. Thus, we base our development of fuzzy type theory to be the thing which corresponds to categories enriched in a category of fuzzy sets in the same way that Martin-Löf type theory corresponds to categories (enriched in sets).

  This is joint work with Shreya Arya, Greta Coraglia, Sean O’Connor, Ana Tenório, and Hans Riess.

• May 8, 1:30pm: Kobe Wullaert, “Towards a homotopy theory of univalent category theory”
  
  Abstract

  In this talk, I present/report on work in progress with the aim of constructing a “homotopy theory of univalent category theory”. More formally, I aim to construct a model structure whose fibrant objects are precisely the univalent categories and the fibrant replacement is given by the Rezk completion. In order to consider (structured) categories as objects, one is forced to leave the framework of (1-)categories and work in the setting of bicategories. Hence, a first challenge is to define a suitable notion of model structure on a bicategory. A definition of a model bicategory has already been presented in the literature. However, it seems that this definition is not immediately suitable for our problem. Hence, I will sketch a definition of a different notion of a model structure.
  I first explain my interest/motivation in the question/construction (and solution). After providing some intuition, I present the definition of a model structure. Furthermore, I conjecture a construction of a suitable model structure on the bicategory of categories, that also generalizes to other bicategories of structured categories. After this, I discuss some future work and related work.

Fall 2022

Seminar mets normally at 4:00pm Pacific Time, in the math department Faculty Research Library (SH 169), located here (see the image below for instructions).

• September 21, 3:30pm: Chaitanya Leena Subramaniam, “Factorisation systems and the small object argument – part I”
  
  Abstract

  The pullback-hom enrichment on arrow categories provides a good framework to define (weak) orthogonal systems and (weak) factorisation systems in 1-category theory and higher category theory. This talk will describe this enrichment and the various flavours of factorisation systems that it provides.

• September 28, 4:00pm: Chaitanya Leena Subramaniam, “Factorisation systems and the small object argument – part II”
  
  Abstract

  The small object argument is a classical technique of constructing weak factorisation systems. In this talk, I will describe a general version of this construction that works to construct any generalised factorisation system provided by the pullback-hom enrichment.

• October 5, 4:00pm: Chaitanya Leena Subramaniam, “Factorisation systems and the small object argument – part III (the ‘plus’ construction)”
  
  Abstract

  The plus construction for sheafification is a well-known alternative way of constructing the strong factorisation system generated by a Grothendieck topology on a presheaf topos (or by a Lawvere-Tierney topology on an arbitrary Grothendieck topos). In this talk I will explain why the plus construction is a particular case of the generalised small object argument, and why it works in more general settings than Grothendieck topoi.

• November 30, 10:00am: Nicola Gambino, “A new monoidal bicategory: coloured symmetric sequences and the arithmetic product” (Slides)
  
  Abstract

  It is well-known that symmetric operads are monoids in the category of symmetric sequences, equipped with the so-called substitution monoidal structure. Similarly, symmetric coloured operads (aka symmetric multicategories) are monoids in the bicategory of coloured symmetric sequences, whose composition is given by a generalisation of the substitution monoidal structure.

  The aim of this talk is to introduce a monoidal structure on the bicategory of coloured symmetric sequence, making use of the double-categorical approach of Garner and Gurski, Shulman, and Wester Hansen and Shulman to address coherence issues. More specifically, we extend the arithmetic product of symmetric sequences studied by Maia and Mendez and by Dwyer and Hess to coloured symmetric sequences and show that it determines a normal oplax monoidal structure on the bicategory of coloured symmetric sequences. In order to do this, we establish general results on extending monoidal structures to Kleisli bicategories.

  This is based on joint work with Richard Garner and Christina Vasilakopoulou, available as https://arxiv.org/abs/2206.06858.