-
Poly: a category of remarkable abundance
David Spivak (4th of February)
The category Poly, of polynomial functors in one variable, is striking. From a purely theoretical standpoint, its comonoids are exactly categories and its monoids generalize operads. Consider: categories and generalized operads falling out of a single setting as the comonoids and monoids is already striking.
But Poly is also impressive from an applications-oriented standpoint. Indeed, it naturally contains database schemas, database instances, and data migration functors; cellular automata like Conway's Game of Life; many kinds of dynamical systems — discrete-time, real-time, etc. — and very general sorts of interactions between them.
In this talk I'll explain all these ideas as well as some of the many avenues for future work. I'll start with the basics but move quickly, with the talk acting more as a calling card — saying "reach out if this interests you" — rather than as a full-fledged explanation of any particular aspect. My goal is simply to show off the remarkable elegance and applicability of this abundant category.
-
Comodels of an algebraic theory
Richard Garner (11th of February)
In 1991 Eugenio Moggi introduced the monadic approach to computational effects; this is the mechanism by which purely functional programming languages such as Haskell can express computations with side-effects such as output, input, or interaction with an external store.
Around 2000, Plotkin and Power refined the Moggi perspective by looking not at monads, but the equational algebraic theories which generate them: this amounts to specifying not just a kind of side-effect, but a set of primitive operations by which one can program with these side-effects.
Algebraic theories have models, not only in the category of sets, but also in any category with finite products. In particular, one can look at comodels of a theory: a model in the opposite of the category of sets. A crucial insight of Power and Shkaravska is that, if T is a theory encoding interaction with an environment, then a T-comodel is a state machine providing an instance of the environment with which T interacts.
The objective of this talk is to explain this history, and to prove a new result: the category of comodels of any algebraic theory T is a presheaf category [B,Set], where B is a small category, which can be computed explicitly, that encodes the static and dynamic properties of the side-effects encoded by T.
-
Relative topology, motion planning, and coverage problems
Gunnar E. Carlsson (18th of February)
Algebraic topology produces invariants that capture aspects of the shape of a space, or in the case of topological data analysis. Although these invariants are in general quite rich, they are somewhat sparse in low dimensions. On the other hand, it is possible to consider comma categories of spaces, for example the category of spaces with reference to a fixed base space and morphisms respecting the reference map. When one does this, one obtains a much richer set of invariants. I will discuss how to apply this kind of construction in the setting of evasion problems for sensor nets and more general motion planning problems.
-
The logic of contextuality
Samson Abramsky (11th of March)
Contextuality is a key signature of quantum non-classicality, which has been shown to play a central role in enabling quantum advantage for a wide range of information-processing and computational tasks. We study the logic of contextuality from a structural point of view, in the setting of partial Boolean algebras introduced by Kochen and Specker in their seminal work. These contrast with traditional quantum logic a la Birkhoff–von Neumann in that operations such as conjunction and disjunction are partial, only being defined in the domain where they are physically meaningful.
We study how this setting relates to current work on contextuality such as the sheaf-theoretic and graph-theoretic approaches. We introduce a general free construction extending the commeasurability relation on a partial Boolean algebra, i.e. the domain of definition of the binary logical operations. This construction has a surprisingly broad range of uses. We apply it in the study of a number of issues, including:
- establishing the connection between the abstract measurement scenarios studied in the contextuality literature and the setting of partial Boolean algebras;
- formulating various contextuality properties in this setting, including probabilistic contextuality as well as the strong, state-independent notion of contextuality given by Kochen–Specker paradoxes, which are logically contradictory statements validated by partial Boolean algebras, specifically those arising from quantum mechanics;
- investigating a Logical Exclusivity Principle, and its relation to the Probabilistic Exclusivity Principle widely studied in recent work on contextuality as a step towards closing in on the set of quantum-realisable correlations;
- developing some work towards a logical characterisation of the Hilbert space tensor product, using logical exclusivity to capture some of its salient quantum features.
Mathematics in the 21st century
John Baez (25th of March)
The climate crisis is part of a bigger transformation in which humanity realizes that the Earth is a finite system and that no physical quantity can grow exponentially forever. This transformation may affect mathematics — and be affected by it — just as dramatically as the agricultural and industrial revolutions did. After a review of the problems, we discuss how mathematicians can help make this transformation a bit easier, and some ways in which mathematics may change.
April
Reasoning in an infinity-topos with homotopy type theory
Dan Christensen (1st of April)
This talk will be an introduction to homotopy type theory that will explain how it can be used to prove theorems that hold in any ∞-topos. I will introduce the basic ideas of type theory and give some intuition for what these mean homotopically. I will end by giving examples of results proved in homotopy type theory that tell us new results in any ∞-topos. No prior knowledge of type theory or ∞-category theory will be assumed.
Noncrossing hyperchords and free probability
Joachim Kock (8th of April)
Free probability is a noncommutative probability theory introduced by Voiculescu in the 1980s, motivated by operator algebras and free groups, and useful in random matrix theory. Where classical independence relates to the tensor product of algebras, free independence relates to the free product of algebras. Speicher discovered the combinatorial substrate of the theory: noncrossing partitions. He derived the free cumulant-moment relations from Möbius inversion in the incidence algebra of the lattice of noncrossing partitions, and used it, via two reduction procedures, to model free multiplicative convolution. A crucial ingredient, which has no analogue in the classical setting, is the notion of Kreweras complement of a noncrossing partition. In this talk, after a long introduction to these topics, I will explain some more categorical viewpoints. A first step is an operad of noncrossing partitions. A second step is a decomposition space (2-Segal space) Y of noncrossing hyperchords, whose simplicial structure encodes higher versions of Kreweras complementation. The incidence bialgebra of Y is a direct combinatorial model for free multiplicative convolution. It is related to the previous models by the standard simplicial notion of decalage: the first decalage of Y gives the (two-sided bar construction of the) operad, and the second decalage gives the lattice. These two decalages encode precisely Speicher's two reductions.
This is joint work with Kurusch Ebrahimi-Fard, Loïc Foissy, and Frédéric Patras.Topos theory and measurability
Asgar Jamneshan (15th of April)
In point-free (or abstract) measure theory measurable spaces are replaced by σ-complete Boolean algebras, measurable functions by Boolean homomorphisms, and measure spaces by measure algebras. This more general perspective has some advantages over the traditional pointwise approach to measure theory. For example, it facilitates the use of topos-theoretic techniques to study measurability. To this effect, a translation process between the internal language/ logic of certain Boolean topoi and the "usual" external language/ logic is required which we can accomplish by using the formalism of conditional analysis. We illustrate this with some recent applications in ergodic theory.
Proofs as programs: challenges and strategies for program synthesis
Shaowei Lin (22nd of April)
The Curry-Howard correspondence between proofs and programs suggests that we can exploit proof assistants for writing software. I will discuss the challenges behind a naïve execution of this idea, and some preliminary strategies for overcoming them. As an example, we will organize higher-order information in knowledge graphs using dependent type theory, and automate the answering of queries using a proof assistant. In another example, we will explore how decentralized proof assistants can enable mathematicians or programmers to work collaboratively on a theorem or application. If time permits, I will outline connections to canonical structures, reflection (ssreflect), transport, unification and universe management.
Fast Diagrammatic Reasoning and Compositional Approaches to Fundamental Physics
Jonathan Gorard (29th of April)
The Wolfram Model — a discrete spacetime model based upon hypergraph rewriting — can be naively formalized as a conventional double-pushout rewriting system over a partial adhesive category of (directed) hypergraphs. However, the abstract rewriting structure of the model also permits an elegant interpretation in terms of dagger compact categories, with considerable formal analogies to FdHilb and the foundations of categorical quantum mechanics, yet with an additional causal semantics definable in terms of a second symmetric strict partial monoidal structure (such that the entire system can be formalized, for instance, in terms of a double category or a weak 2-category). In addition to potentially defining a general categorical semantics for discrete models of quantum gravity, this formalism presents a fundamentally new approach to performing efficient diagrammatic reasoning over combinatorial structures, by suggesting various generalizations of the standard deductive inference rules of resolution, superposition, paramodulation and factoring in the Knuth-Bendix completion approach to automated theorem-proving, and by making more explicit use of the causal structure of the abstract rewriting system in the choice of which inference rules to apply. We show how this approach can be applied to the problem of enacting fast diagrammatic simplification of circuits in quantum information theory, as well as (time-permitting) the problem of efficiently discretizing the Cauchy problem in numerical general relativity, showcasing comparisons against some existing software frameworks and algorithms.
May
Contractibility as uniqueness
Emily Riehl (6th of May)
What does it mean for something to exist uniquely? Classically, to say that a set A has a unique element means that there is an element x of A and any other element y of A equals x. When this assertion is applied to a space A, instead of a mere set, and interpreted in a continuous fashion, it encodes the statement that the space A is contractible, i.e., that A is continuously deformable to a point. This talk will explore this notion of contractibility as uniqueness and its role in generalizing from ordinary categories to infinite-dimensional categories.
Quotient completions for topos-like structures
Maria Emilia Maietti (13th of May)
In this talk we report fundamental results concerning free completions with quotients of specific Lawvere doctrines for building toposes, quasi-toposes and predicative versions of them. Our final goal is to use such completions for modelling foundations of constructive and classical mathematics which are predicative in the sense of Poincaré, Weyl and Feferman, including that in [M09]. We first recall how the tool of completing an elementary existential Lawvere doctrine with exact quotients is the fundamental construction behind the tripos-to-topos construction in [HJP80] beside including as instances both the exact completion of a regular category and that of a weakly lex finite product category, as reported in [MR15]. We then describe recent work with Fabio Pasquali and Pino Rosolini where we show how the elementary quotient completion of an elementary Lawvere doctrine in [MR13] is the fundamental construction behind a tripos-to-quasi-topos construction including toposes as exact completions of a left exact category in [Me03] as instances. We also mention a joint work with Davide Trotta where we extend results in [MPR17] about tripos-to-topos constructions coinciding with exact completions of a left exact category. We end by applying the elementary quotient completion to build examples of predicative toposes including the Effective Predicative Topos in [MM21].
- [HJP80] J.M. Hyland, P. T. Johnstone and A.M.Pitts. Tripos theory. Math. Proc. Cambridge Philos. Soc. 88, 205-232, 1980
- [M09] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3): 319-354, 2009
- [MR13] M.E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17): 445–463, 2013
- [MR15 ] M.E. Maietti and G. Rosolini. Unifying Exact Completions. Applied Categorical Structures 23(1): 43-52, 2015
- [MPR17] M.E. Maietti, F. Pasquali and G. Rosolini. Triposes, exact completions, and Hilbert's ε-operator. Tbilisi Mathematical Journal. 10(3): 141-66, 2017
- [Me03] M. Menni. A characterization of the left exact categories whose exact completions are toposes. Journal of Pure and Applied Algebra, 3(177): 287-301, 2003
- [MM21] M.E. Maietti, S. Maschio. A predicative variant of Hyland's Effective Topos. To appear in The Journal of Symbolic Logic
The law of large numbers in categorical probability
Tobias Fritz (20th of May)
The law of large numbers (in its various guises) can be regarded as the most central result of probability theory, and any serious axiomatic system for probability must reproduce it in some form. After a general introduction to categorical probability in terms of Markov categories, I will explain how to formulate a form of the strong law of large numbers within this framework, namely the Glivenko-Cantelli theorem on the convergence of the empirical distribution. I will also sketch how to use this statement in order to derive other laws of large numbers from it.
Two-dimensional semantics of homotopy type theory
Michael Shulman (27th of May)
The general higher-categorical semantics of homotopy type theory involves (∞,1)-toposes and Quillen model categories. However, for many applications it suffices to consider (2,1)-toposes, which are reasonably concrete categorical objects built out of ordinary groupoids. In this talk I'll describe how to interpret homotopy type theory in (2,1)-toposes, and some of the applications we can get from such an interpretation. I will assume a little exposure to type theory, as in Dan Christensen's talk from April, but no experience with higher toposes or homotopy theory. This talk will also serve as an introduction to some basic notions of Quillen model categories.
June
Model Structures from Models of HoTT
Steve Awodey (3rd of June)
Homotopical models of Martin-Löf type theory often make use of the notion of a Quillen model category, even if only implicitly. From the interpretation of identities between terms as paths in an abstract space, to the univalence principle identifying identities of types with homotopy equivalences of spaces, the standard tools of abstract homotopy theory provide the means to make rigorous the basic intuition behind the homotopical interpretation of the formal logical system. So good is this kind of model that it turns out to be possible to invert the process, in a certain sense; given a categorical model of HoTT of an appropriate kind, one can construct from it a full Quillen model structure on the underlying category. This can be seen as a further strengthening of the idea of HoTT as the internal language of an ∞-topos.
A category of hybrid systems
Eugene Lerman (10th of June)
Hybrid systems are dynamical systems that exhibit both continuous time evolution and abrupt transitions. Examples include mechanical systems (e.g., a ball bouncing off a floor) and cyber-physical systems (e.g., a room with a thermostat). Definitions of a hybrid dynamical systems vary widely in literature but they usually include directed graphs, spaces with vector fields attached to the nodes of graphs and partial maps or, more generally, relations attached to the edges of graphs. The vector fields are used to model continuous evolution and the relations the abrupt transitions.
I wanted to understand if analogues of coupled cell networks of Golubitsky, Stewart and their collaborators (these are highly structured coupled systems of ODEs) make sense for hybrid dynamical systems. In order to do that I needed to make sense of open hybrid systems, their interconnection, networks of hybrid systems and maps between networks of hybrid systems.
Proceeding by analogy with continuous time systems I introduced the notion of a hybrid phase space and its underlying manifold. A hybrid phase space can be succinctly defined as double functor. Hybrid phase spaces form a category HyPh with morphisms coming from vertical natural transformations. A hybrid dynamical system is a pair (A,X) where A is a hybrid phase space and X is a vector field on the manifold U(A) underlying A. I then constructed a category HyDS of hybrid dynamical system. The definition of HyDS passes a couple of sanity checks.
Using the foundation laid out above James Schmidt and I showed that one can also define hybrid surjective submersions, hybrid open systems, their interconnections and networks of hybrid systems. This way one can model systems of bouncing balls and several interconnected rooms with separate thermostats.
References: arXiv:1612.01950 [math.DS] and arXiv:1908.10447 [math.DS] (DOI: 10.1016/j.geomphys.2019.103582).
Sheaf representation of monoidal categories
Chris Heunen (17th of June)
Wouldn't it be great if monoidal categories were nice and easy? They are! We will discuss how a monoidal category embeds into a "nice" one, and how a "nice" monoidal category consists of global sections of a sheaf of "easy" monoidal categories. This theorem cleanly separates "spatial" and "temporal" directions of monoidal categories.
More precisely, "nice" means that certain morphisms into the tensor unit have joins that are respected by tensor products, namely those morphisms that are central and idempotent with respect to the tensor product. By "easy" we mean that the topological space of which these central idempotents form the opens is a lot like a singleton space, namely local.
Categorifying flabby sheaves in the appropriate way makes the representation functorial from monoidal categories to schemes of local monoidal categories. The representation respects many properties of monoidal categories: if a monoidal category is closed/traced/complete/Boolean, then so are its local stalks. As instances we recover the Lambek-Moerdijk-Awodey sheaf representation for toposes, the Stone representation of Boolean algebras, the representation by germs of open subsets of a topological space, and the Takahashi representation of Hilbert modules as continuous fields of Hilbert spaces.
From comonads to calculus
Kathryn Hess (24th of June)
Abstracting the framework common to most flavors of functor calculus, one can define a calculus on a category M equipped with a distinguished class of weak equivalences to be a functor that associates to each object x of M a tower of objects in M that are increasingly good approximations to x, in some well defined, Taylor-type sense. Such calculi could be applied, for example, to testing whether morphisms in M are weak equivalences.
In this talk, after making the definition above precise, I will describe a machine for creating calculi on functor categories Fun (C,M) that is natural in both the source C and the target M. Our calculi arise by comparison of the source category C with a tower of test categories, equipped with cubical structure of progressively higher dimension, giving rise to sequences of resolutions of functors from C to M, built from comonads derived from the cubical structure on the test categories. The stages of the towers of functors that we obtain measure how far the functor we are analyzing deviates from being a coalgebra over each of these comonads. The naturality of this construction makes it possible to compare both different types calculi on the same functor category, arising from different towers of test categories, and the same type of calculus on different functor categories, given by a fixed tower of test categories.
(Joint work with Brenda Johnson)
July
Formalising Contemporary Mathematics in Simple Type Theory
Lawrence Paulson (1st of July)
A long-standing question in mathematics is the relevance of formalisation to practice. Rising awareness of fallibility among mathematicians suggests formalisation as a remedy. But are today's proof assistants up to the task? And what is the right formalism?
A wide variety of mathematical topics have been formalised in simple type theory using Isabelle/HOL. The partition calculus was introduced by Erdös and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. Highly technical results were obtained by Erdös-Milner, Specker and Larson (among many others) for the case of ordinal partition relations, which is concerned with countable ordinals and order types. Much of this material was formalised last year (with the assistance of Džamonja and Koutsoukou-Argyraki).
Grothendieck's Schemes have also been formalised in Isabelle/HOL. This achievement is notable because some prominent figures had conjectured that schemes were beyond the reach of simple type theory.
Some highlights of this work will be presented along with general observations about role of type theory in the formalisation of mathematics.
Categorical differential structures and their role in abstract machine learning
Geoffrey Cruttwell (8th of July)
A fundamental component of many machine learning algorithms is differentiation. Thus, if one wishes to abstract and generalize aspects of machine learning, it is useful to have an abstract perspective on differentiation. There has been much work on categorical differential structures in the past few years with the advent of differential categories, Cartesian differential categories, and tangent categories. In this talk I'll focus on Cartesian reverse differential categories, a recent variant of Cartesian differential categories, and touch on how they can be used in abstract machine learning.
What is monoidal topology?
Walter P Tholen (22nd of July)
Monoidal topology may be seen as being inspired by some visionary remarks in Hausdorff‘s „Grundzüge der Mengenlehre“ of 1914, and it takes its modern lead from two distinct seminal contributions of the early 1970s: the Manes-Barr presentation of topological spaces in terms of ultrafilter convergence axioms, and Lawvere’s presentation of metric spaces as small categories enriched in the extended non-negative half-line of the reals. Both types of spaces become instances of small so-called (T,V)-categories, where T is a Set-monad and V a (commutative) quantale, i.e. a small, thin and (symmetric) monoidal-closed category. The setting therefore allows for a general study of „spaces“ that combines geometric and numerical aspects in a natural way.
In this talk we present some key elements of the theory and its applications, showing in particular how the strictification and inversion of some naturally occurring inequalities in this lax-monoidal setting leads to interesting topological properties and unexpected connections. Time permitting, we will also point to some on-going and future work in the area.
Topological Inspiration for Infinity Modular Operads
Marcy Robertson (29th of July)
A modular operad can be thought of as an undirected network which allows for feedback “loops”. An infinity modular operad is such a network where operations can be continuously varied with respect to time. The goal of this talk is to give a gentle introduction to a Segal model for infinity modular operads, focusing on the topological origins of the idea. The audience is not expected to be familiar with operads or topology. This talk will cover snippets of joint work with Luci Bonatto, Pedro Boavida, Philip Hackney , Geoffroy Horel and Donald Yau.
August
From 2-rigs to lambda-rings
Todd Trimble (5th of August)
This talk will summarize some aspects of recent work with John Baez and Joe Moeller, which aims to tie together representations of symmetric groups, Schur functors, and lambda rings from the point of view of 2-rigs, which are a categorification of ordinary 'rigs' or rings without negatives. A common theme in this area is the notion of 'plethory'. We sketch how the archetypal plethory of lambda rings arises simply and naturally from the simplest possible '2-plethory', and applying decategorification to it.
What is the point of Lean's maths library?
Kevin Buzzard (12th of August)
Lean is a computer proof checker developed by Microsoft Research. Over the last four years I have been part of a team of mathematicians and computer scientists who have got it into their heads that it is somehow "obviously" a good idea to build a formally verified library of modern mathematics in Lean. You can think of it as a 21st century Bourbaki if you like, although our plans are actually far grander than Bourbaki's. I will talk about two things: (1) how it's going and (2) why we're doing it. No background in computer proof checkers will be necessary to follow the talk.
Categorical Explicit Substitutions
Valeria de Paiva (19th of August)
The advantages of functional programming are well-known: programs are easier to write, understand and verify than their imperative counterparts. However, functional languages tend to be more memory intensive and these problems have hindered their wider use in industry. The xSLAM project tried to address these issues by using *explicit substitutions* to construct and implement more efficient abstract machines, proved correct by construction.
In this talk I recap two results from the xSLAM project which haven't been sufficiently discussed. First, we provided categorical models for the calculi of explicit substitutions (linear and cartesian) that we are interested in. No one else seems to have provided categorical models for explicit substitutions calculi, despite the large number of explicit substitutions systems available in the literature. Indexed categories provide models of cartesian calculi of explicit substitutions. However, these structures are inherently non-linear and hence cannot be used to model *linear* calculi of explicit substitutions. Our work replaces indexed categories with pre-sheaves, thus providing a categorical semantics covering both the linear and cartesian cases. Our models satisfy soundness and completeness, as expected.
Secondly, we recall a different linear-non-linear type theory, built from Barber and Plotkin DILL ideas, which, like DILL, is better for implementations. Unlike DILL, this type theory, called ILT, satisfies an internal language theorem. Thus we describe ILT, show categorical semantics for it and sketch the proof of its internal language theorem, thus justifying its use in implementations. These results are examples of `(categorically) structured deep syntax', to borrow Hyland's characterization.
Cats and Types: Best Friends?
Conor McBride (26th of August)
Intensional Type Theory and Category Theory ought to fit well together, but the current practical experience of representing concepts from one with the tools of the other is often quite strained. On the one hand, fibrational approaches to dependency often seem heavy. On the other hand, definitional equality in type systems often falls way short of delivering even the simplest of coherences. In this talk, I shall reflect on the problems and search for opportunities. What has to change to make type theoretic proof assistants a good medium for categorical approaches to programming and proof? I wish I knew the answer to that question! I can at least offer a few clues. For example, I shall exhibit a universe of indexed inductively defined datatypes which exhibit nontrivial presheaf structure by construction.
September
MMT: A UniFormal Approach to Knowledge Representation
Florian Rabe (2nd of September)
UniFormal is the idea of representing all aspects of knowledge uniformly, including narration, deduction, computation, and databases. Moreover, it means to abstract from the multitude of individual systems, which not only often focus on just one aspect but are doing so in mutually incompatible ways, thus creating a universal framework of formal knowledge.
MMT is a concrete representation language to that end. It systematically abstracts from assumptions typically inherent in the syntax and semantics of concrete systems, and focuses on language-independence, modularity, and system interoperability. While constantly evolving in order to converge towards UniFormal, its design and implementation have become very mature. It is now a readily usable high-level platform for the design, analysis, and implementation of formal systems.
This talk gives an overview of the current state of MMT, its existing successes and its future challenges.
Tensor products, multimaps and internal homs
John Bourke (9th of September)
The notions of monoidal category, multicategory and closed category are closely related, with each having their own advantages. Considering the relationship between them leads naturally to skew variants — skew monoidal categories, skew multicategories and skew closed categories — and I will explore some of these variants in this talk.
Understanding free infinity-categories
Jamie Vicary (16th of September)
Infinity-categories have a reputation for being difficult algebraic objects to define and work with. In this talk I will present a new definition of free infinity-category that demystifies them, and makes them easy to understand from an algebraic perspective. The definition is given as a sequence of inductive-recursive data structures, and we explore how this relates to Grothendieck's original ideas on infinity-categories. No knowledge of infinity-categories is required to follow this talk!
This is joint work with Christopher Dean, Eric Finster, Ioannis Markakis and David Reutter.
Abstract homotopy theory for topological data analysis
Andrew J. Blumberg (23rd of September)
A starting point for the modern perspective on algebraic topology is the Eilenberg-Steenrod axioms characterizing homology theories. More generally, there has been a great deal of work starting from insights of Verdier, Quillen, and Dwyer-Kan that gives abstract characterizations of the structures of homotopy theory in terms of formal cylinder and suspension objects or mapping spaces. This talk will be about efforts to understand the invariants of topological data analysis from an abstract perspective. There will be many more questions than answers.
Algebraic theories with string diagrams
Pawel Sobocinski (30th of September)
In Lawvere theories the central role is played by categories with finite products. The free category with finite products on one object (FinSet^op) is the Lawvere theory of the empty algebraic theory, and the free category with finite products on a signature (of an algebraic theory) has a concrete description as a category of classical syntactic terms. But, using a theorem due to Thomas Fox, we can also capture these categories nicely using string diagrams.
The string diagrammatic approach gets you further than ordinary syntax. In a POPL 21 paper with Ivan Di Liberti, Fosco Loregian and Chad Nester, we developed a Lawvere-style approach to algebraic theories with partially defined operations. It turns out that in this setting, instead of categories with finite products, the relevant concept is discrete cartesian restriction categories (dcrc). And string diagrams are the right syntax for this setting: they let us describe the free dcrc on an object and the free dcrc on a signature. I will sketch some of our results and talk about some of the ramifications, including a string diagrammatic description of categories with free finite limits.
October
Cubical Methods in Homotopy Type Theory and Univalent Foundations
Anders Mortberg (7th of October)
One of the aims of Homotopy Type Theory and Univalent Foundations (HoTT/UF) is to provide a practical foundation for computer formalization of mathematics by building on deep connections between type theory, homotopy theory and (higher) category theory. Some of the key inventions of HoTT/UF include Voevodsky's univalence axiom relating equality and equivalence of types, the internal stratification of types by the complexity of their equality, as well as higher inductive types which allow synthetic reasoning about spaces in type theory. In order to provide computational support for these notions various cubical type theories have been invented. In particular, the Agda proof assistant now has a cubical mode which makes it possible to work and compute directly with the concepts of HoTT/UF. In the talk I will discuss some of the mathematical ideas which motivate these developments, as well as show examples of how computer mechanization of mathematics looks like in Cubical Agda. I will not assume expert knowledge of HoTT/UF and key concepts will be introduced throughout the talk.
A topos view of axioms of choice for finite sets
Andreas Blass (14th of October)
Tarski proved (in set theory without choice) that if one assumes that all families of 2-element sets have choice functions then one can prove that all families of 4-element sets have choice functions. Mostowski (1937) investigated similar implications, giving number-theoretic and group-theoretic conditions, some necessary and some sufficient for such implications. But some questions remained unsolved, in particular: Do choice from 3-element sets, from 5-element sets, and from 13-element sets together imply choice from 15-element sets. Gauntt (1970) resolved those remaining questions, using group-theoretic criteria. I plan to describe some of this work and to explain what it has to do with topos theory.
Cubical setting for Discrete Homotopy Theory
Chris Kapulkin (21st of October)
Discrete homotopy theory, developed by H. Barcelo and collaborators, is a homotopy theory of (simple) graphs. Homotopy invariants of graphs have found numerous applications, for instance, in the theory of matroids, hyperplane arrangements, and time series analysis. Discrete homotopy theory is also a special instance of a homotopy theory of simplicial complexes, developed by R. Atkin, to study social and technological networks.
In the talk, I will introduce the main concepts and open problems of discrete homotopy theory. I will also report on the joint work with D. Carranza on developing a new foundation for discrete homotopy theory in the category of cubical sets, which offers solutions to a number of long standing open problems in the field.
Doubly Lax Colimit of Double Categories with Applications
Dorette Pronk (28th of October)
Thus far, lax and oplax pseudo colimits of double categories have been considered in two flavours [2]: horizontally lax and vertically lax, based on the notions of horizontal and vertical transformations (respectively) between double functors. Also, the diagrams of double categories have typically been indexed by a 2-category.
In this work we introduce diagrams indexed by a double category; in order to make sense of this we will map into a version of the quintets of the category of double categories, because this category itself is only enirched in double categories and is often taken as a 2-category. Between the new indexing functors we introduce a new notion of transformation, namely doubly lax transformation. We then introduce a double categorical version of the Grothendieck construction and show that it has a universal property as doubly lax colimit of the diagram; i.e., a colimit that is lax with respect to the new transformations.
As applications we obtain:
- a universal property as lax colimit for the Grothendieck construction for bicategories described in [1];
- a universal property for the elements construction for double categories;
- a notion of fibration for double categories, different from the internal one described by Street and others;
- a double categorical generalization of the classical tom Dieck fundamental groupoid for a space with an action by a topological group.
This is joint work with Marzieh Bayeh (University of Ottawa) and Martin Szyld (Dalhousie University).
November
Formal mathematics, dependent type theory, and the Topos Institute
Jeremy Avigad (4th of November)
Modern logic tells us that mathematics can be formalized, in principle. Computational proof assistants, developed over the last half century, make it possible to do so in practice. In this talk, I will briefly survey the state of the field today and discuss some of the reasons that formalization is desirable. I will discuss one particular proof assistant, Lean, and its library, mathlib. I will explain why dependent type theory, Lean's underlying logical framework, provides an attractive platform for formalization. Finally, I will consider ways that formal mathematics can support and enhance the Topos Institute's missions.
The rise of quantitative category theory
Paolo Perrone (18th of November)
In several domains of applications, category theory can be useful to add conceptual clarity and scalability to mathematical models. However, ordinary categories often fail to grasp some quantitative aspects: the total cost of a certain strategy, the number of composite steps, the discrepancy between a concrete construction and its ideal model, and so on.
In order to incorporate these aspects, it is helpful to switch to a "quantitative" version of categories: weighted categories. These are particular enriched categories where each arrow carries a number, or "weight", as in a weighted graph. The composition of paths comes with a triangle inequality, analogous to the one of metrics and norms, which equips universal properties with quantitative bounds. Most results in category theory have a weighted analogue, which often carries additional geometric or analytic significance. Weighted categories have been around since early work of Lawvere, but only in the last few years researchers are starting to recognize their importance. More and more recent papers are using them in fields as diverse as topological data analysis, geometry, and probability theory, some times even rediscovering the concepts independently.
In this talk we are going to see what it's like to work with weighted categories, their relationship with graphs, and the quantitative aspects about limits and colimits. We will also define a weighted analogue of lenses, and use it to express liftings of transport plans between probability measures.
Relevant literature: arXiv:2110.06591, and additional work in preparation.
December
Categories of diagrams in data migration and computational physics
Evan Patterson (2nd of December)
Diagrams are among the most fundamental and ubiquitous concepts of category theory. Less appreciated are the several notions of morphism between diagrams in a category. After reviewing the resulting categories of diagrams, this talk will explain their central role in two recent projects by the author and collaborators. First, due to their close connections with limits and colimits, the categories of diagrams provide a natural syntax for defining flexible data migrations between categorical databases. We describe a prototype implementation of this system in Catlab.jl. In the second part of the talk, we explain how "Tonti diagrams," diagrammatic presentations of physics equations expressed in vector calculus or exterior calculus, can be formalized using category-theoretic diagrams. When combined with a suitable discretization scheme, such as the discrete exterior calculus (DEC), the result is a diagrammatic and compositional approach to building numerical simulators of physical systems.
Phase Distinctions in Type Theory
Robert Harper (9th of December)
(Joint work with Jon Sterling and Yue Niu)
The informal phase distinction between compile-time and run-time in programming languages is formally manifested by the distinction between kinds, which classify types, and types, which classify code. The distinction underpins standard programming methodology whereby code is first type-checked for consistency before being compiled for execution. When used effectively, types help eliminate bugs before they occur.
Program modules, in even the most rudimentary form, threaten the distinction, comprising as they do both types and programs in a single unit. Matters worsen when considerating "open" modules, with free module variables standing for its imports. To maintain the separation in their presence it is necessary to limit the dependency of types, the static parts of a module, to their imported types. Such restrictions are fundamental for using dependent types to express modular structure, as originally suggested by MacQueen.
To address this question Moggi gave an "analytic" formulation of program modules in which modules are explicitly separated into their static and dynamic components using tools from category theory. Recent work by Dreyer, Rossberg, and Russo develops this approach fully in their account of ML-like module systems. In this talk we consider instead a "synthetic" formulation using a proposition to segregate the static from the dynamic, in particular to define static equivalence to manage type sharing and type dependency.
File icons made by Smartline from www.flaticon.com