Program

This is joint work with Kathryn Hess, Brenda Johnson and Julie Rasmusen.

Colimits (and limits) are among the most fundamental notions in category theory, and also among the most useful of the basic structures. In topology, colimits are used to “glue” spaces together. However, problems arise when we try to work with spaces which continuously deform, because colimits are not invariant under such deformations. In this case, one uses a related notion called a homotopy colimit. But what are these, really? Homotopy colimits do not satisfy a universal property, even in the homotopy category, and are usually defined by the way they are computed in particular types of categories, such as model categories. In joint work, Hess and Johnson identified a list of properties that one would expect homotopy limits to satisfy in any homotopical category. These properties were chosen carefully because they are needed to perform certain constructions in functor calculus. Building on their work, we have identified the categorical structures that govern these properties. A distillation system relates two actions of the category of small categories on the category of categories through a lax linear functor. In two talks, I will review the classical notion of homotopy colimits and define distillation systems, ultimately proposing these as a new model for homotopy colimits.

First introduced by Mulvey in 1986, quantales are complete lattices with an associative binary operation which distributes over arbitrary joins. There has been renewed interest in their study in recent years, as they provide the appropriate framework for the generalization of relations, known as the quantale-valued relations. In this tutorial, we shall review the basics of quantale theory, introduce the category of quantale-valued relations Q-Rel, describe important examples, and study its two-dimensional structure. In particular, we shall show how Q-Rel is a quantaloid, describe when it is a cartesian bicategory and a linear bicategory, as well as demonstrate how it can be viewed as a double category. Moreover, we will discuss how Q-Rel provides a framework for monoidal topology, a categorical field which provides abstract foundations for ordered, metric and topological structures. Slides.

In the setting of a tangent category, a connection on the analog of a vector bundle has been defined and many properties for it worked out.  Here, we will consider how to define and work with a more general notion: a connection on the analog of a submersion from differential geometry.   This is joint work with Marcello Lanfranchi.

The category of affine schemes is a tangent category whose tangent bundle is given by Kahler differentials. How special is this tangent structure? Is there any other tangent structure in the category of affine schemes?

In this talk, we classify the representable tangent structures in the category of affine schemes, by introducing a useful tool: the notion of tangent monoid. When the base ring R is a principal ideal domain, we show there are only two of such tangent structures: the aforementioned one, and the trivial one. We also show that when R is not a PID, we have other non-trivial representable tangent structures. Slides.

 We can assign to each smooth manifold M the tangent category of its slice $Sman_{sub}/M$ (where $Sman_{sub}$ is the categroy of smooth manifolds and submersions). This assignment extends to a contravariant functor from $Sman_{sub}$ to TanCat.

We would like to generalize this to $L$-manifolds where L is a suitably nice Lie group. When the action of $L$ on $M$ is free, we can work with the slice of the quotient manifold$ L\backslash M$. When the action is not free, the quotient is not a manifold (and does not have a well-defined tangent structure). 

In this talk I will propose a way around this by considering a category of free $L$-manifolds that can be considered as resolutions of $M$. This will give us a diagram of tangent categories, and its pseudolimit is again a tangent category.  This is a suitable tangent category for the quotient $L\backslash M$  in the sense that:

--It is functorial for a suitable class of $L$-equivariant smooth maps.

--It is interacts well with covers of $M$ that consists of open $L$-invariant subspaces.

This is joint work with Geoff Vooys from the University of Calgary. Slides.

 The two-element Boolean algebra induces a hierarchy of Stone-type dualities including classical Stone duality, Priestly duality, and Roller duality.  We show that the categories involved in these three dualities are organized by a square-tiled hexagon of forgetful functors whose hexagon of left adjoints can surprisingly be obtained from the former “by duality.”  In this talk I will review the relevant dualities, construct the hexagonal network of underlying functors, and provide a unifying formula for the corresponding free constructions in terms of dualization.  Building slightly upon the latter, we will see that opposite sides of the hexagon consist of dual pairs of adjunctions and that the adjunction in the middle, which separates the hexagon into two squares, is self-dual. Slides.

The two protagonists of this story are Markov and partial Markov categories. We will start with Markov categories, and build towards the need for partial Markov categories. Partial Markov categories blend structures from Markov and restriction categories to enable probabilistic reasoning in the presence of constraints on experiments. After describing partial Markov categories, we will formulate a few fundamentals results in probability theory such as normalization and Bayes theorem in this setting.  

We will also examine a couple of well-studied problems from probabilistic decision  theory in this setting. Finally, we shall provide a compositional account of generalized reversible computing by setting it up as a resource theory which is a partial Markov category.  Slides.

References: 

1. Robin Cockett, and Stephen Lack. "Restriction categories I: categories of partial maps." (2002).

1. Elena Di Lavore, and Mario Román. "Evidential decision theory via partial markov categories." (2023).

2. Elena Di Lavore, Bart Jacobs, and Mario Román. "A Simple Formal Language for Probabilistic Decision Problems." (2024).

3. Jacobs, Bart, Aleks Kissinger, and Fabio Zanasi. "Causal inference by string diagram surgery." (2019)

4. Clemence Chanavat, Priyaa Varshinee Srinivasan. "A compositional account of generalized reversible computing" (2025) Under preparation

5. Robin Cockett, Isabelle Jianing Geng, Carlo Maria Scandolo, Priyaa Varshinee Srinivasan. "Extending Resource Monotones using Kan Extensions" (2022)

Haskell’s type system is based on the Hindley-Milner type system which supports only rank-1 types. As functional languages have evolved, higher-ranked polymorphism has become essential for expressing more general and reusable functions. However, full type inference for higher-ranked types is undecidable and often requires explicit type annotations. In this work we propose a simplified type inference approach in comparison to the system proposed by Peyton Jones. Our method explicitly handles universal quantification of type variables to improve predictability and help programmers determine when annotations are necessary. We demonstrate our approach using a minimal programming language syntax that provides a structured method for inferring types for higher-ranked polymorphism while maintaining clarity and usability. Furthermore, we propose a system that separates the collection of type equations from the solving process. We define a formal notion of a solution for the equations produced during inference and require the type inference algorithm to generate such a solution. This separation is still in progress and is intended to provide a clearer framework for reasoning about the soundness of the inference process. Slides

 Categorical Message Passing Language (CaMPL) is a concurrent programming language based on a categorical semantic given by a linear actegory. The sequential side of CaMPL is a functional-style programming language, while the concurrent side supports message passing between processes along channels with concurrent types called protocols. 

A desirable feature of a concurrent message passing language is the support for higher-order processes, which allows processes to be passed to other processes. While passing concurrent processes between processes is feasible, supporting recursive process definitions requires the ability to reuse the passed process multiple times. However, since concurrent resources cannot be duplicated, the processes must be passed as sequential data. Consequently, the concurrent side must be enriched into the sequential side.

This presentation concerns the categorical semantics that lets us store concurrent processes as sequential data and yet use them. This is abstractly given by the equivalence between an actegory with hom-objects and an enriched category with copowers. We present the proof of this equivalence in detail. In the closed symmetric case this problem was studied by kelly and Janelidze. We present the proof in the non-symmetric non-closed case. Slides.

Dr. Robin Cockett is leading a team at the University of Calgary that is developing a concurrent functional programming language called Categorical Message Passing Language (CaMPL). CaMPL uses message-passing concurrency, i.e. processes are connected by channels along which they pass messages. The categorical semantics of message passing is given by a linear M-actegory C where a monoidal category M (representing messages and sequential functions) acts on a linearly distributive category C (representing channels and concurrent processes) in two directions via the message-passing actions ○ : M × C -> C and ● : M^{op} × C -> C. In this talk, we will focus on the covariant action ○.

The above linear M-actegory C represents the categorical semantics for programs with deterministic processes. We recall the power set functor P : Set -> SupLat that constructs the free sup-lattice on a set. We define the change of enrichment 2-functor P* from set-enriched categories to sup-lattice-enriched categories using P. This produces the sup-lattice-enriched categories P*M and P*C and maps the set-action ○ : M × C -> C to the sup-lattice-action ○* : P*M /otimes P*C -> P*C.

The sup-lattice-enriched category P*C represents the categorical semantics for programs that have non-deterministic processes. This means that the non-deterministic message-passing action ○* requires the category of messages and sequential functions to also be non-deterministic. However, sequential functions are deterministic in CaMPL. We recall U : SupLat -> Set which takes the underlying set of a sup-lattice which is its carrier. This forms the monoidal adjunction P -| U that induces the power set monad on Set. In this talk, we will discuss in-progress work for how we construct an action for passing deterministic messages to non-deterministic processes using P -| U. Slides.

Coecke-Palvovic-Vicary (CPV) gave a correspondence between orthogonal bases in finite-dimensional Hilbert Spaces (FdHilb) and Commutative-Dagger Frobenius algebras in FdHilb. In the first part of my talk, I will go over this correspondence and the associated categorical statements.

In the second part of my talk, I will give an outline of the programme about how this correspondence can be generalised to arbitrary dimensions. I will first introduce the ingredients involved- Finiteness spaces, Lefschetz Spaces and linear monoids and then will give a few results connecting these mathematical objects.  Slides

A "Model category" is a category with some additional structure that encodes a notion of "homotopy theory" of its objects. For example, the categories of topological spaces, of chain complexes, or of simplicial sets all have such "model structures" that respectively encodes the ordinary homotopy theory of spaces, homological algebras, and simplicial homotopy theory.

Nowadays, the theory of model category mostly serve as the main technical tool that underlies the theory of higher categories: We generally expect any definition of some sort of higher algebraic structures to be organized into a model category, and model categories are also a very effective way to present certain specific $\infty$-categories.

But the notion predates higher category theory and can be studied completely independently of higher category - in fact for a very long time model categories were the main way we had to indirectly talk about $\infty$-categories before the notion was completely formalized.

The goal of the tutorial is to give a quick introduction to model categories from a purely category-theoretic point of view - so that you can get a general idea of how they work, and/or orient yourself in the literature if you ever want to learn the topic more systematically.

If time permits, I will also briefly discuss some more recent developments with the theory of semi and weak model structures. Slides.

This is joint work with Kathryn Hess, Brenda Johnson and Julie Rasmusen.

Colimits (and limits) are among the most fundamental notions in category theory, and also among the most useful of the basic structures. In topology, colimits are used to “glue” spaces together. However, problems arise when we try to work with spaces which continuously deform, because colimits are not invariant under such deformations. In this case, one uses a related notion called a homotopy colimit. But what are these, really? Homotopy colimits do not satisfy a universal property, even in the homotopy category, and are usually defined by the way they are computed in particular types of categories, such as model categories. In joint work, Hess and Johnson identified a list of properties that one would expect homotopy limits to satisfy in any homotopical category. These properties were chosen carefully because they are needed to perform certain constructions in functor calculus. Building on their work, we have identified the categorical structures that govern these properties. A distillation system relates two actions of the category of small categories on the category of categories through a lax linear functor. In two talks, I will review the classical notion of homotopy colimits and define distillation systems, ultimately proposing these as a new model for homotopy colimits.

We discuss a recent string-diagrammatic calculus that is complete for first-order logic. The calculus is based on C.S. Peirce’s Existential Graphs and his work in ‘Note B’, and achieves its results by combining cartesian and linear bicategories. We present the development of the calculus, motivate the inference rules, and suggest future directions. Slides

 Arboreal categories are categories of objects with an intrinsic, tree-like process structure. This gives rise to a well-behaved notion of bisimilarity between objects which can then be transported along an adjunction into an extensional category of interest. The main concrete examples of these so-called arboreal adjunctions recover logical equivalence for various fragments of infinitary first-order logic by operating over an extensional category of relational structures. This abstract framework provides a solid foundation for game comonads and has been used to obtain extensions and variations of substantial resource-sensitive model-theoretic results such as Rossman's equirank preservation theorem. However, a key open question is whether we can systematically chart the landscape of the correspondence between logics and arboreal adjunctions.

  In this talk, we explore this landscape by focusing on arboreal adjunctions obtained from idempotent comonads, which we term idempotent arboreal covers. As is well known, the theory of (co)monads simplifies greatly in the idempotent case and, accordingly, known idempotent game comonads correspond to variants of basic modal logic, which sit on the lower end of the expressive power spectrum. After reviewing the fundamentals of arboreal categories and adjunctions we introduce the concept of an idempotent seed: a full subcategory generating an arboreal coreflective subcategory via colimit closure. We motivate this concept through examples that yield both known and novel idempotent comonads with clear logical interpretations. Finally, we discuss some theoretical results that streamline the search for idempotent seeds and move towards a potential classification theorem. In particular, we leverage density comonads to characterize coreflective subcategories without explicitly constructing the coreflector. Slides

  Graphical formalisms like proof nets and string diagrams are intimately related to coherence results. In the case of symmetric monoidal closed categories (e.g. Set, Cat, Vec), a full solution to the coherence problem was obtained by the mid nineties (Cockett et al., Tan), but since then the development of corresponding graphical formalisms seems not to have been exhausted. In their Rosetta stone paper of 2009, Baez and Stay suggested that an internal hom object could be represented graphically by attaching a ``clasp'' between two wires that stand for the ``input'' and ``output'' objects. This could allow for coherence identities and (di)naturality to be expressed by the same sort of wire deformations and sliding-of-boxes that make string diagram languages so convenient for mathematicians. To the best of our knowledge, the idea has never been fully developed. We present work in progress on a graphical formalism for symmetric monoidal closed categories that we believe captures the spirit of the ``clasp'' idea. The main contribution is the combinatorial gadget we call monoidal dependency graphs, which correspond to certain normal forms of objects with respect to monoidal closed structure. Joint work with Florian Schwarz. Slides

  Categories graded by a monoidal category V generalize both V-enriched categories and V-actegories. Introduced by Wood, V-graded categories admit an elementary definition in terms of graded morphisms, which have not only a domain and a codomain but also a grade that is an object of V, regarded as the type of an auxiliary input variable. On the other hand, Lambek's multicategories (or planar coloured operads) generalize monoidal categories, so that enrichment in a multicategory generalizes enrichment in a monoidal category. Thus there arises a question of whether V-grading generalizes to multicategories V.

In this two-part tutorial talk, we provide an introduction to categories graded by monoidal categories as well as a notion of category (multi)graded by multicategory V, in which graded morphisms can have several auxiliary input variables. Every multicategory V embeds into a strict monoidal category called the monoidal envelope of V, whose definition we review, and we discuss how V-graded categories are equivalently categories graded by the monoidal envelope. Employing terminology of Campbell and Lurie, we also review the Elmendorf-Mandell symmetric monoidal envelope of a symmetric multicategory V (or coloured operad). Using this, we define symmetrically V-graded categories, which carry symmetry data that enable permutation of auxiliary variables. We provide a result that compares categories graded by a monoidal category with categories graded by its underlying multicategory, as well as an analogous result in the symmetric case. Time permitting, we also review further aspects of graded categories originating in the speaker's recent paper on graded functor categories and bifunctors (arXiv:2502.18557).

The Grothendieck construction is usually phrased as a biequivalence of bicategories. Recently, Moser-Sarazola formulated the equivalence as a Quillen equivalence, hence leveraging coherence from model categories. In this talk we will investigate whether an analogous statement for fibrations of bicategories, traditionally presented as a triequivalence of tricategories, can also be framed as a Quillen equivalence. Based on work in progress with C. Bardomiano, M. Sarazola, J. Nickel, S. Toro Oquendo, and P. Verdugo. Slides. or website

This talk will introduce two new structures in the setting of differential categories and algebraic theories, alongside a third, well-established one:

  1. A relative differential category is a differential category (Blute, Cockett, Seely, 2006) in which the monad is replaced by a relative monad (Altenkirch, Chapman, Uustalu, 2015), allowing for more general base categories.

  2. A differential clone is an algebraic theory extending the theory of commutative rings—admitting operations beyond polynomials—while supporting partial derivatives of these operations.

3. A Fermat theory is an algebraic theory extending commutative rings and satisfying an axiom reminiscent of Hadamard’s lemma, which enables a notion of partial derivatives (Dubuc, Kock, 1984).

Differential clones and Fermat theories involve partial derivatives in the algebraic sense, whereas differential categories—and by extension, relative differential categories—use a deriving transformation, a categorical abstraction of differentiation.

We will explain the following relationships among these structures:

- Every relative differential category induces a differential clone, capturing its finite-dimensional algebraic content.

- Every differential clone induces a relative differential category, via its implementation in a broader category of modules.

- Every Fermat theory is a differential clone.

We will conclude with the following open question:

Q. Is every differential clone a Fermat theory? Slides

It is relatively well known that theories of first-order logic and its fragments can be understood in a variety of different category-theoretic ways, the main examples being syntactic categories (e.g regular categories), syntactic bicategories/allegories (e.g. bicategories of relations/unitary pretabular allegories), fibrational doctrines (e.g. elementary existential doctrines), and classifying topoi (e.g. regular topoi). Methods of passing between these different representations are also well-established (see e.g. [2]). However, while a result that seems to allow double categories to be added to this list of examples has existed in the literature for close to two decades ([5], Thm 14.4 opened a doctrine-to-double-category pathway), and while Paré outlined a direct theory-to-double-category interpretation

in a talk in 2009 [4], double categories as representations of first-order theories remains an underdeveloped area of research.

In this talk, we will give a summary of this picture as it is currently understood, highlighting in particular recent developments made by Bonchi et al. in [1] and Nasu in [3], areas that have yet to be explored, and our plans for filling some of those gaps. Slides

References:

[1] Filippo Bonchi, Alessandro Di Giorgio \& Davide Trotta (2024): When Lawvere meets Peirce: an equational presentation of boolean hyperdoctrines, doi:10.48550/arXiv.2404.18795. Available at http://arxiv.org/abs/2404.18795. ArXiv:2404.18795 [math].

[2] Peter T. Johnstone (2002): Sketches of an Elephant: A Topos Theory Compendium, Volume 1. Clarendon Press, Oxford, England.

[3] Hayato Nasu (2025): Logical Aspects of Virtual Double Categories, doi:10.48550/arXiv.2501.17869. Available at http://arxiv.org/abs/2501.17869. ArXiv:2501.17869 [math].

[4] Robert Pare (2009): Coherent Theories as Double Lawvere Theories. Available at https://www.mscs.dal.ca/~pare/CapeTown2009.pdf.

[5] Michael A. Shulman (2009): Framed bicategories and monoidal fibrations. Available at http://arxiv.org/abs/0706.1286. ArXiv:0706.1286 [math].

Bicategories of relations or spans have attracted many category theorists since the 1970s, and the study has been extended to the world of double categories in recent years. In this talk, I will provide an overview of the development of this field, particularly in relation to a condition called the Frobenius axiom, as presented in Walters and Wood's paper ``Frobenius objects in Cartesian bicategories.'' This axiom can be understood as a criterion for a double category to qualify as a ``double category of relations,'' and I will explain some results that support this idea. Slides

There are no Cauchy complete objects in the double category $\mathbb R{\rm ing}$ of commutative rings, homomorphisms, and bimodules, since an $(S,R)$-bimodule $M$ has a right adjoint if and only if it is finitely generated and projective as an $S$-module. To correct this difficiency, Par\'{e} (Outstanding Contributions to Logic 20, Springer, 2021) dropped the unit-preserving condition on ring homomorphisms and used the Kleisli category of a graded monad to obtain  a double category  $\mathbb A\rm mpli$ in which every object is Cauchy complete.

Exploiting the Joyal-Tierney ring/quantale analogy in which  finite sums are replaced by arbitrary suprema,  we established Par\'{e}'s results for the double category $\mathbb Q{\rm uant}$ of quantales,  homomorphisms, and bimodules (TAC 43, 2025). However, we left the contruction of the Kleisli category for a time when we could consider Set-graded monads on $\mathbb Q{\rm uant}$. 

In this talk, we present a definition of the Kleisli double category $\mathbb D_T$ of a graded monad $T$ on a double category $\mathbb D$ which we use to generalize  $\mathbb A\rm mpli$ to the double category $\bim(\cal V)$ of monoids in a suitable symmetic monoidal closed category $\cal V$. Our examples of $\bim({\cal V})$ include $\mathbb R{\rm ing}$  and $\mathbb Q{\rm uant}$. The monad we consider is graded by a double category $\mathbb A$ of sets  and assigns a lax functor ${\rm Rel}_A\colon \bim({\cal V})\to\bim({\cal V})$ to each set $A$.  Moreover, ${\rm Rel}_AQ$ is the  quantale of $Q$-valued relations on $A$, when $\bim({\cal V})=\mathbb Q{\rm uant}$; and ${\rm Rel}_AR$ is isomorphic to the ring ${\rm Mat}_nR$ of $n\times n$ matrices over $R$ for $A=\{1.\dots,n\}$, when $\bim({\cal V})=\mathbb R{\rm ing}$. Slides

10 years ago as I was finishing up my undergrad at UOttawa, Rick introduced me to integrations (in the algebra sense) and Rota-Baxter algebras, the integration analogue of derivations and differential algebras. In particular, where a derivation is axiomatized by the Leibniz rule, an integration is axiomatized by the Rota-Baxter rule, which is integration by parts without using differentiation. Inspired by this, at this year’s FMCS, I will give a tutorial on integrations and Rota-Baxter algebras. We will go over the definition, lots examples, some constructions, how they interact with derivations/differential algebras, and also how they relate to Zinbiel algebras. Slides

A "Model category" is a category with some additional structure that encodes a notion of "homotopy theory" of its objects. For example, the categories of topological spaces, of chain complexes, or of simplicial sets all have such "model structures" that respectively encodes the ordinary homotopy theory of spaces, homological algebras, and simplicial homotopy theory.

Nowadays, the theory of model category mostly serve as the main technical tool that underlies the theory of higher categories: We generally expect any definition of some sort of higher algebraic structures to be organized into a model category, and model categories are also a very effective way to present certain specific $\infty$-categories.

But the notion predates higher category theory and can be studied completely independently of higher category - in fact for a very long time model categories were the main way we had to indirectly talk about $\infty$-categories before the notion was completely formalized.

The goal of the tutorial is to give a quick introduction to model categories from a purely category-theoretic point of view - so that you can get a general idea of how they work, and/or orient yourself in the literature if you ever want to learn the topic more systematically.

If time permits, I will also briefly discuss some more recent developments with the theory of semi and weak model structures.

  Categories graded by a monoidal category V generalize both V-enriched categories and V-actegories. Introduced by Wood, V-graded categories admit an elementary definition in terms of graded morphisms, which have not only a domain and a codomain but also a grade that is an object of V, regarded as the type of an auxiliary input variable. On the other hand, Lambek's multicategories (or planar coloured operads) generalize monoidal categories, so that enrichment in a multicategory generalizes enrichment in a monoidal category. Thus there arises a question of whether V-grading generalizes to multicategories V.

In this two-part tutorial talk, we provide an introduction to categories graded by monoidal categories as well as a notion of category (multi)graded by multicategory V, in which graded morphisms can have several auxiliary input variables. Every multicategory V embeds into a strict monoidal category called the monoidal envelope of V, whose definition we review, and we discuss how V-graded categories are equivalently categories graded by the monoidal envelope. Employing terminology of Campbell and Lurie, we also review the Elmendorf-Mandell symmetric monoidal envelope of a symmetric multicategory V (or coloured operad). Using this, we define symmetrically V-graded categories, which carry symmetry data that enable permutation of auxiliary variables. We provide a result that compares categories graded by a monoidal category with categories graded by its underlying multicategory, as well as an analogous result in the symmetric case. Time permitting, we also review further aspects of graded categories originating in the speaker's recent paper on graded functor categories and bifunctors (arXiv:2502.18557).

Grothendieck duality states, up to adding some correct adjectives, that the derived functor of a sufficiently nice morphism of schemes will admit a right adjoint. We will translate this into the language of dualizing complexes and give a noncommutative analog.

Parameterized functions are ubiquitous in mathematics and physics. For example, the time evolution of a quantum mechanical system is a family of unitary functions parameterized by a time variable. Of course, this parameterization is continuous in the appropriate sense. Upon careful examination, it can be shown that these parameterized functions form a monoidal category, and that continuous reparameterizations induce endofunctors on this category. In this talk, we generalize this construction to show how to construct parameterized maps in arbitrary V-enriched categories. The parameterized maps inherit the morphism structure of V. We show that in order to recover all of the nice properties enjoyed by unitary time evolutions, V must be Cartesian monoidal. In particular, we consider time evolutions characterized by parameterized quantum circuits.

This mini-course will be an introduction to homotopy type theory (HoTT). We will start by reviewing dependent type theory and its original semantics in locally cartesian closed categories, due to Seely. We will show that models in locally cartesian closed categories necessarily satisfy the equality reflection rule, which is syntactically undesirable, as it makes type checking undecidable.

We will then discuss a family of models based on categories equipped with a weak factorization system, a structure studied in abstract homotopy theory since the late 1960s, that remedy this issue. Certain properties of such models, like Voevodsky's univalence axiom, can then be expressed in dependent type theory, yielding what we now know as homotopy type theory.

We will conclude this mini-course with several open problems that organize the work in the field and can be used as entry points by those interested in contributing to the area.

10 years ago as I was finishing up my undergrad at UOttawa, Rick introduced me to integrations (in the algebra sense) and Rota-Baxter algebras, the integration analogue of derivations and differential algebras. In particular, where a derivation is axiomatized by the Leibniz rule, an integration is axiomatized by the Rota-Baxter rule, which is integration by parts without using differentiation. Inspired by this, at this year’s FMCS, I will give a tutorial on integrations and Rota-Baxter algebras. We will go over the definition, lots examples, some constructions, how they interact with derivations/differential algebras, and also how they relate to Zinbiel algebras.

 Principal bundles have three different definitions, depending on the category of geometric objects you study.

In Differential Geometry, a principal bundle is a locally trivial projection map of smooth manifolds with an atlas whose transition maps are given by group multiplication.

In Topology they are G-equivariantly trivial G-spaces. In Algebraic Geometry, they are known as étale locally isotrivial geometric quotients of G-varieties.

The goal of this work is to have an overarching categorical notion that recovers all of them and their properties.

While they are different objects, they all have in common that they are locally isomorphic to the Cartesian product of a base space with a group.

Our categorical principal bundles recover the principal bundles from topology and differential geometry and we hope to also incorporate the principal bundles from algebraic geometry as an example of this in a carefully chosen partial map category of schemes. Slides

Even though, we can usually recognise a type theory when we see one, there si no established definition of type theories in the literature. In this talk, we examine a proposal for the definition of (dependent) type theory by Taichi Uemura that has functorial semantics.

We show that we can freely generate type theories and that the 2-category of type theories admits bicolimits that allow us to create more complicated type theories out of simpler ones. This can be used to provide a bicolimit presentation for various type theories (= constructing them as a bicolimit of free objects).

We also discuss interactions of the constructions from the previous paragraph with semantics. Slides

One of the important problems in formal logic and programming language design is the binder problem. One of the approaches for dealing with name binding is the nominal abstract syntax (introduced by Gabbay and Pitts in 1999), which relies on an infinite set of atoms (names). The notion of nominal sets form a category Nom in which the morphisms are equivariant functions.

Dependent type theory is a form of type theory where types can depend on terms (i.e., values). This contrasts with traditional type systems, where types are independent of the values they describe. In dependent type theory, a type is not just a set of values—it's a logical proposition, and a term of that type is a proof of that proposition. Dependent types are modeled using slice categories. In this presentation, I will discuss the local structure of category Nom. Slides

This mini-course will be an introduction to homotopy type theory (HoTT). We will start by reviewing dependent type theory and its original semantics in locally cartesian closed categories, due to Seely. We will show that models in locally cartesian closed categories necessarily satisfy the equality reflection rule, which is syntactically undesirable, as it makes type checking undecidable.

We will then discuss a family of models based on categories equipped with a weak factorization system, a structure studied in abstract homotopy theory since the late 1960s, that remedy this issue. Certain properties of such models, like Voevodsky's univalence axiom, can then be expressed in dependent type theory, yielding what we now know as homotopy type theory.

We will conclude this mini-course with several open problems that organize the work in the field and can be used as entry points by those interested in contributing to the area.

 Functor calculi associate Taylor-series-like towers of functors to objects in functor categories. They have been used to great effect in algebraic topology and $K$-theory to compare values of functors and to elucidate structures.

  In this talk, I will provide a brief introduction to one type of functor calculus -- the discrete functor calculus -- and discuss ongoing work, inspired by it, to develop a general process for creating new functor calculi and cocalculi. In particular, I will review the distillation systems introduced in Kristine Bauer's talks, explain how they arose from the discrete calculus, and show how they are used to build what we call a monad distillery, a functorial process for transforming a strict monoidal functor $\theta: I\rightarrow B$ and a $B$-actegory $C$ into a monad on $C$. This is joint work with Kristine Bauer, Robyn Brooks, Kathryn Hess, Julie Rasmusen, and Bridget Schreiner.

Intuitively, (∞,1)-categories are categories in which we have n-arrows or n-cells at all levels (similar to 2-categories, n-categories, etc.). In addition, axioms for composition hold up to a higher cell, and the n-arrows for n≥2 are invertible. All this data is subject to coherence conditions.

To solve the intricacies of this definition, dependent type theory has been presented as a strong candidate. In this talk, I will survey the progress of this program in the simplicial homotopy type theory framework of Riehl and Shulman. Recent advances from a number of authors include fibrations of different flavours, limits, directed univalence, and the Yoneda lemma.

How can we build a topos from a C*-algebra?  Our immediate goal is to generalize the approach taken in [1] to all  C*-algebras.  (Familiarity with [1] is not necessary for the purposes of this talk.)  A pseudogroup naturally presents itself as a Grothendieck site:

it has an underlying inverse semigroup just like a Grothendieck site has an underlying

category.  Our approach for a C*-algebra is roughly the same: the algebra ought to present itself as a site for a topos.  But how is this accomplished?  Starting with some basic ring theory we generalize the so-called Karoubi envelope of a ring using (right) principal ideals.  In turn, this generalization suggests how the same idea may be developed for a C*-algebra by `building in' the topological aspect of the algebra using so-called Hilbert modules. Then we are prepared to discuss presheaves, sheaves and topos theory, ultimately developing a way to match concepts between operator theory and topos theory. Slides.

We're all familiar with polynomials. In fact, most of us probably know that, given a ring R, we can form the polynomial ring R[X]: we think of it as taking R, adding an "indeterminate element" X, and generating new elements (polynomials) by addition and multiplication. However, if we think like category theorists, we can describe R[X] using a universal property instead.

In this talk, I'll explain the universal property that corresponds to "adding an indeterminate", show its link to my research, and describe what you get when you add an indeterminate to the category of sets (when viewed as a topos).

Elementary toposes are categories that share many properties of the category of sets. Every elementary topos has an internal language, which is a version of typed intuitionistic higher-order logic obtained from the lattices of subobjects. It thus makes sense to speak of an elementary topos as a local set theory which provides a foundation for mathematics. The notion of elementary $\infty$-topos generalises this concept to $\infty$-categories. It is conjectured that the internal language of an elementary $\infty$-topos is Homotopy Type Theory (HoTT), that is Martin-L\"of Dependent Type theory with $\prod$, $\Sigma$ and intensional identity types satisfying the univalence axiom. Thus, it makes sense to

speak of elementary $\infty$-toposes as univalent dependent type theories, where instead of the lattice of subobjects we have a universal $\infty$-groupoid of all (small) objects with the structure of a space. Thus, elementary $\infty$-toposes provide a semantic framework for HoTT and therefore a univalent foundation of mathematics.

In the talk, I will introduce and motivate the notion of elementary $\infty$-topos, and I will sketch the progress that has been made so far towards proving the conjecture. In particular, I will explain how HoTT presents such an elementary $\infty$-topos via its syntactic category built from the syntax and rules of the type theory. This will be achieved in two steps. First, I will use the fact that the syntactic category of HoTT has the structure of a tribe in the sense of Joyal. I will extend Joyal’s theory of tribes by introducing the notion of a univalent fibration in a tribe. These fibrations exist in particular in the syntactic category of HoTT. In the second step, I will explain how each such tribe presents via its localisation an $\infty$-category and if the tribe has enough univalent fibrations then this $\infty$-category is an elementary $\infty$-topos. Slides.

Categories graded by a monoidal category V generalize both V-actegories and V-enriched categories without requiring any additional properties of V. However, V-graded categories are themselves also categories enriched in a monoidal category $\hat{V}$ whose objects are presheaves on V. In this talk, we define a notion of weighted limit for V-graded categories that specializes to recover the familiar notion of weighted limit for enriched categories. Our V-graded weighted limits involve weights valued in V rather than $\hat{V}$, and they form a special class of $\hat{V}$-enriched weighted limits. This allows us to prove that in the special case where V is biclosed and the V-graded categories involved are V-enriched, we recover precisely the familiar notion of V-enriched weighted limit. When V is an arbitrary monoidal category, V-graded weighted limits again specialize to a notion of weighted limit for V-enriched categories, and they also give rise to a notion of weighted limit in V-actegories that admits a particularly simple description. For arbitrary V-graded categories, we develop both a convenient concrete formulation of weighted limits as well as an equivalent abstract description as certain V-graded representations, and we explore examples of V-graded weighted limits including V-graded powers, conical limits, and weighted pullbacks. This is joint work with Rick Blute and Rory Lucyshyn-Wright. Slides

Different notions of graphs arise in different contexts: are the edges directed, are loops allowed, are multiple edges allowed, etc. We collect these different categories of graphs and investigate the adjoint functors between them, the adjoints that don't exist, along with some sample applications. The goal is to provide a handy reference for users of graphs who also enjoy categories. This is joint work with Pranali Sohoni. Slides.

In this talk, based on joint work, we study epimorphisms of rigs and their relation to a straightforward extension of what it means to be a solid algebra. We ultimately conclude with a theorem giving equivalent conditions on what it means to give an epimorphisms of rigs with commutative domain and a (potentially conjectural based on how the next week goes on my end) connection with Isbell zig-zag theory extended to rigs. We will also conclude that if $A$ is a commutative rig and $f:A \to B$ then $B$ is necessarily commutative. Slides