The MIT Categories Seminar is an informal research seminar in category theory and categorical modelling. We meet each **Thursday, 4.30pm to 5.30pm** in **MIT 2-255**. Sometimes notes from the seminar are published here (please feel free to contribute).

** August 2 **: David Spivak

In last week's seminar, we heard from Antwane Mason about Goguen and Burstall's notion of institution, which is a category-theoretic formalism used for software specification and verification. The definition is usually phrased in terms of a satisfaction relation between models and sentences of signatures, and a certain bivariant coherence condition on it.

In this talk I will discuss a few different category-theoretic perspectives on this notion, including from categorical database theory, posetal bifibrations, and topos theory. In the order "signatures, models, sentences, satisfaction", we can view

- databases as an institution via "schemas, instances, embedded dependency constraints, satisfaction",
- any posetal bifibration as an institution via: "base objects, fiber elements, fiber elements, ≤", and
- toposes as an institution via "toposes, points, truth values, satisfaction".

** February 15 **: Brendan Fong

An overview of Coecke, Sadrzadeh, and Clark's *Mathematical foundations for a compositional distributional model of meaning*.

** February 22 **: David Spivak

Fuzzy simplicial sets I.

** March 1 **: David Spivak

Fuzzy simplicial sets II.

** March 8 **: Brendan Fong

An overview of McInnes and Healy's *UMAP: Uniform manifold approximation and projection for dimension reduction.*

** March 29 **: Brendan Fong

The equivalence of hypergraph categories and lax monoidal functors Cospan(FinSet) --> Set.

** April 5 **: Enrique Boroquez (UNAM)

The idea is to explore the concept "Point", to look at it from different perspectives and see the connections given by the Stone Duality and the Gelfand Duality. Starting from a topological perspective, a point as an element of a topological space, we'll see the correspondences with ultrafilters, global elements in the category of Stone Spaces, morphisms that have as codomain the initial algebra 2 and how this morphisms correspond to valuations of a language in classical logic. We'll then go to boolean valued models, see how the points there have a probabilistic behavior and see some interesting consequences given by doing the forcing method through principal ultrafilters vs non-principal ultrafilters.Then we'll see the equivalences given by the Gelfand Duality: global elements in the category of locally compact spaces, characters of commutative C* algebras, maximal ideals, pure states (as positive, normalized functionals) and irreducible representations.

** April 12 **: David Spivak

Videos: Part I, Part II, Part III, Teaser/Addendum

** April 19 **: Remy Tuyeras

How to do genetics with category theory I.

** April 26 **: David Spivak

** May 10 **: Remy Tuyeras

How to do genetics with category theory II: Recognition of biological mechanisms.

** May 17 **: Christoph Dorn (Oxford)

"Higher categories" are algebraic structures which generalise categories, in the same way that categories generalise sets. The theory of these structures is ubiquitous in many areas of application of category theory. In this talk, we will motivate higher structure from applications in logic, type theory and programming languages. Surprisingly, a formulation of higher categories which is amendable to computer implementation has been missing for decades — with homotopy type theory being a notable exception of the special case of “higher groupoids”. Starting from elementary observations about compositionality in higher dimensions, will sketch a combinatorial approach to higher categories that gives rise to a programming language which we call “Globular” and which comes with an elegant geometric model. We will see that programs in Globular can capture complex higher-dimensional geometric deformations, and learn how, for instance, they can capture higher homotopy groups of spheres and other interesting geometric facts.

** May 24 **: Tim Havel

System Dynamics is a moniker coined by Jay Forrester over 50 years ago at MIT, when computers were just beginning to be used to simulate the behaviors of complex models of social and economic processes. Today it has a substantial following in business schools, management consulting firms, and some multinational corporations, with the goal of teaching "Systems Thinking" to their respective stake holders (see "Business Dynamics" by John Sterman). While it has since branched out into more sophisticated agent-based and dynamic network models (see this short article), it was initially based on a diagrammatic language for nonlinear ODEs that continues to play a central role in its applications. This talk will introduce this language and give some examples, with the hope that the audience will discover some analogies, and new applications, for the categorical formalisms it has developed for modeling and analyzing systems in a broader sense.
Slides available here.

** May 31 **: Brendan Fong

Causal theories: a categorical approach to Bayesian networks.

** June 7 **: David Spivak

** June 14 **: Remy Tuyeras

How to do genetics with category theory III.

** June 21 **: Brendan Fong

I'll talk about an algebraic setting (in particular, a category) in which supervised learning algorithms can be composed, and then explain how this articulates the structure underlying backpropagation on a neural network. More details here.

** July 19 **: David Spivak

Decomposition spaces are combinatorial objects that allow one to decompose maps in a natural (co-associative and co-unital) way. All categories are decomposition spaces, but not vice versa. Decomposition spaces form a category, called Decomp, where the maps preserve the decomposition structure. I'll discuss these ideas and recent work (joint with J. Kock) where we show that every slice category of Decomp is a topos. One of them is the topos I discussed recently: that of "discrete temporal type theory".

** July 26 **: David Spivak

** August 2 **: Antwane Mason (Rensselaer Polytechnic Institute)

Formal verification is the process of proving that a system adheres to a specification of its intended behavior. Like programming languages, there exists a variety of specification languages, each suited to describing distinct types of behavior. Some systems may require a combination of specification types and reasoning strategies to verify the whole system. This scenario motivates the need for heterogeneous specification languages. In this talk, we shall explore Farrell et. al.'s 2017 paper entitled "Combining Event-B and CSP: An Institution Theoretic approach to Interoperability". We shall see how the authors use category theory to establish interoperability between two specification languages, Event-B and CSP, focusing particularly on how they develop semantic preserving translations between the two languages.