The MIT Categories Seminar is an informal teaching seminar in category theory and its applications, with the occasional research talk. We presently meet online each Thursday, 12noon to 1pm Boston time (UTC-4). The talk is broadcast over Zoom and YouTube, with simultaneous discussion on the Category Theory Zulip channel. Talks are recorded and remain available on our YouTube channel. Our Google Calendar is here.
Please email Brendan Fong (bfo (at) mit.edu) or Paolo Perrone (pperrone (at) mit.edu) to join the mailing list.
May 28: David Spivak (MIT)
On March 5 in this seminar, I discussed the category Poly of polynomial functors on Set and its applications to mode-dependent dynamical systems—machines that can change their interface and which other machines they wire to, based on their internal state.
At that time, I didn't know how to think about the composition monoidal structure on Poly in terms of dynamical systems, but it turns out that the story is quite nice. The composition product can be used to model strategies in the sense of game theory, as well as a way to "speed up" dynamical systems. But it comes with lots of other surprises too, both theoretical and applied, e.g. due to Gambino and Kock, Ahman and Uustalu, and Garner. It's a truly remarkable monoidal category.In this talk I'll briefly review the previous one, so no special background is necessary.
June 4: Carmen Constantin (Oxford)
June 11: Paolo Perrone (MIT)
June 18: Christian Williams (UC Riverside)
RChain is a distributed computing system based on a concurrent language with reflection. The ρ calculus, or reflective higher-order π calculus, is a concurrent language with operations that control the distinction between data and code. This gives networks intrinsic structure, which can offer deep knowledge and utility. This can be used to think globally about the web.
To reason about this structure, Namespace Logic [Meredith, Radestock 2005] augments the ρ calculus with first order logic, to create a predicate calculus for denoting subclasses of terms. For example, the predicate for a process to be single-threaded is "not[null] and not[par(not[null],not[null])]" -- like an integer being prime. These predicates provide types for the ρ calculus, which condition programs and enable high-level reasoning in concurrent networks.
We present a categorical formulation of the algorithm (-) + first order logic. A language can be presented as an algebraic theory with binding; we then form its topos of presheaves, and therein construct a polymorphic type system with subtyping. The algorithm extends the idea of namespace logic to a broad class of formal languages, and it is especially powerful in concurrent languages with reflection.A draft paper can be found here.
June 25: Remy Tuyeras (MIT)
July 16: Tobias Fritz (Perimeter Institute)
July 23: Evan Patterson (Stanford)
August 6: Valeria de Paiva (Topos Institute)
August 13: Toby St Clere Smithe (Oxford)
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)
April 12 : David Spivak
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)
May 24 : Tim Havel
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
July 19 : David Spivak
July 26 : David Spivak
August 2 : Antwane Mason (Rensselaer Polytechnic Institute)
August 9 : 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
August 16 : Brendan Fong
August 23 : David Spivak
An introduction to double categories
August 30 : Brendan Fong
2-categories and adjunctions
September 10 : David Spivak
Adjunctions and Mates
September 17 : Remy Tuyeras
October 1 : Reuben Cohn-Gordon (Stanford)
In cooperative conversation, speakers tend to prefer informative utterances, and listeners assume the speaker is being informative in order to draw inferences. For instance, if you hear me say "John liked half of the concert", you infer that he did not like to other half, since as an informative speaker, I would then have said "John liked the concert", were that true. Bayesian models can be used to formalize these inferences.I show that a model of an informative speaker (that says as much as is possible) can be defined as a right Galois connection (right adjoint between posets) to a literal listener, understood as a monotone function (functor between posets) from utterances to possible worlds. Dually, a pragmatic listener (that deduces that no more is meant that is said) is a left adjoint of a literal speaker, understood as a monotone function from possible worlds to utterances. While elementary, this points to a deeper category-theoretic formulation of Gricean pragmatics and more generally, cooperative games.
October 11 : Paolo Perrone (Max Planck Institute for Mathematics in the
Monads are a categorical concept which can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of “evaluating an expression partially”: for example, “2+3” can be obtained as a partial evaluation of “2+2+1”, and conversely, we can view “2+2+1” as a partial decomposition of “2+3”. This construction can be given for all monads on a concrete category, and it is linked to a simplicial object called the bar construction, of which it gives an operational interpretation: the bar construction is a simplicial set, and its 1-cells are partial evaluations.
We study the properties of partial evaluations for general monads on concrete categories. We prove that whenever the multiplication of the monad is weakly cartesian, partial evaluations can be composed via the usual Kan filler property of simplicial sets, of which we give an interpretation in terms of substitution of terms.
For the case of probability monads, partial evaluations correspond to what probabilists call conditional expectation of random variables, which is used to define martingales. It follows that a martingale is equivalently described as a chain of partial decompositions.
This talk is part of a work in progress on a general operational interpretation of the bar construction.This is joint work with Tobias Fritz.
October 15 : David Myers (Johns Hopkins University)
In order to make a model of some system, we have in mind the sort of things in that system we intend to model; we have an ontology of our model, and we hope the things in this ontology correspond to the things in the system. But coming up with such an ontology is more of an art than a science. A model's success is judged on its ability to predict, not how much it matches our intuitive ontology. What things do our best models actually model?
Can we find a "natural ontology" of a model, one that comes from the model itself and contains only the things the model is modelling? What is a thing, anyway? In this talk, we will look at a categorical approach to these problems using the yoga of behavior types.
October 29 : Lee Mondshein
How can category theory be productively applied to extend concepts and techniques of logic and linguistics, so as to elucidate the behavior of biological networks?
I will discuss some concrete initial steps, based upon current categorical constructs in logic and topology, and will explain the relevance of emerging semiotic ideas concerning meaning-making and meaning transformation in biological networks.
November 5 : Remy Tuyeras
November 19 : Ed Wike
November 26 : David Spivak
Brendan and I have been developing a new categorical viewpoint—and graphical calculus for—regular logic. I've recently been thinking about how some of the surrounding ideas might apply to learning and adaptation via something I might call a "theory building" adjunction. Some of these ideas seem to connect to Reuben Cohn-Gordon's recent seminar talk on the "Gricean adjunction" from pragmatics.The ideas I'll present are at an early stage in terms of maturity, and the goal of the talk is to be fun and pictorial. Still, I will certainly make connections to the underlying mathematical abstractions.
December 3 : Alex Kavvos (Wesleyan)
December 10 : Brendan Fong
January 31 : Jules Hedges (Oxford)
February 7 : Brendan Fong
An overview of Ellerman's Partition Logic.
February 14 : Brendan Fong
February 21 : Tobias Fritz (Perimeter Institute)
I will explain how monads often arise as Kan extensions of graded monads. For example, the set of lists over an alphabet is the disjoint union of the sets of lists of each length. I will then show how this leads to a construction of a probability monad similar to the Giry monad. The graded monad approach lets us replace the use of measure theory by the combinatorics of finite sets, and makes precise the idea that a probability measure is an idealized version of a finite sample.Joint work with Paolo Perrone.
February 28 : Sam Tenka
March 7 : Brendan Fong
March 21 : Rúnar Bjarnason (Unison Computing)
March 28 : Anthony Bau
April 4 : Natalie Stewart
A PERT chart is a project management tool used to schedule, organize, and coordinate tasks within a project. The data of a PERT chart is a list of activities, together with their durations and dependencies on each other; the PERT chart formats this data as a certain duration-weighted graph. In this talk we'll discuss how these durations form a preorder R, which in fact has the structure of a quantale. This allows us to see PERT charts simply as R-enriched categories, and think about project scheduling in terms of categorical constructions.This talk is based on the following n-Category Café post by Simon Willerton: https://golem.ph.utexas.edu/category/2013/03/project_planning_parallel_proc.html. No familiarity with enriched categories will be assumed.
April 11 : David Spivak
May 2 : David Spivak
Abelian categories are "convenient places to calculate", e.g. to do homological algebra. One nice feature of abelian categories is that they are regular, meaning that each has a well-working calculus of relations. This calculus can be given a graphical formulation, with a "user interface" of wiring diagrams that we can specify mathematically.I'll present abelian categories from this point of view, with the following compressed mathematical specification: a graphical abelian calculus is a bi-ajax po-functor P: LinRel-->Poset. Unpacking this, I'll explain that there is a graphical syntax of linear relations, which is a mild ("thin") extension of Sobocinski's graphical linear algebra. It forms a po-category LinRel, and functors from LinRel to the po-category of posets provide semantic content to this syntax: they tell us how we can "fill the shells". Any lax monoidal po-functor P: LinRel-->Poset whose laxators have both left and right adjoints gives rise to an abelian category, and all abelian categories (up to equivalence) arise in this way.
May 9 : Alberto Speranzon (Honeywell)
May 16 : Diego Roque
May 23 : David Spivak
Planning in autonomous systems is generally hierarchical. A goal is given to a higher-level planner, which decides on a sequence of actions that will accomplish it given the current conditions. Each of these actions is then handed off as a goal to some lower-level planner. To make dinner, we need to go to the store, get ingredients, bring them home, and cook, but going to the store requires choosing a route, and in turn, each step along the route is accomplished by choosing and executing a certain sequence of muscle movements.We will think of planners as generalized Markov decision processes, where we replace the nondeterminism-and-reward aspect of an MDP by an arbitrary monad M on Set. These will be the objects of a category M-MDP, and we formalize "handing off high-level actions to lower-level planners" as morphisms. If M is monoidal, the result will be a symmetric monoidal category, the idea being that a team of bosses can issue commands to be executed by a team of performers.
May 30 : Mitchell Riley (Wesleyan)
July 30 : Kenneth Harris (UCL)
August 8 : Gershom Bazerman (Awake Security)
August 15 : Daniel Rosiak (DePaul)
Tolerance relations are binary relations where just reflexivity and symmetry, but not transitivity, are assumed to hold. Forcing transitivity is obviously natural (and very useful) in many mathematical contexts, but there are a variety of interesting applications where imposing transitivity simply does not seem appropriate. The category of tolerance spaces (with tolerance-preserving functions) has monoidal closed structures, and I will mostly look closely at a few applications and examples displaying what it looks like to enrich over this category.
I may also look briefly at some connections to t-norms—in particular lattice-valued t-norms (lifting the set of truth-values in a fuzzy logic beyond the real interval [0,1])—and some properties of fuzzy tolerance, in the course of which I will touch on some broader interactions with generalized (Lawvere) metric spaces.Finally, I will make a few connections between all this and sheaves, and possibly indicate some more general ideas on metrics on the category of sheaves.
August 22 : Brendan Fong
August 29 : Ben Sherman
September 26 : Simon Cho (Michigan)
October 3 : David Spivak
In this talk, we'll discuss lenses, which have lately been showing up all over applied category theory: in the theory of functional programming, databases, hierarchical planning, open discrete dynamical systems, open economic games, and supervised learning. Lenses are somewhat peculiar-looking things, but at least they form a symmetric monoidal category, denoted Lens.
I hold the opinion that lenses should really be viewed within the larger, more geometrically-flavored category of bundles—objects in Lens are the trivial bundles—and that the reason lenses look peculiar is because the geometric aspect is obscured when we restrict to the special case.
To explain this, I'll show that Lens embeds into a larger symmetric monoidal category that provides geometric intuition, has better formal properties, and will likely be more familiar to mathematicians, e.g. to algebraic geometers. From this viewpoint, lenses become strongly related to that of polynomial functors, which show up in functional programming as "containers" and in database theory as "functorial data migration". I'll generalize further so that examples of lenses include continuous dynamical systems and a more principled (though still partial) solution to the view-update problem in database theory.
October 10 : Brendan Fong
Morphisms in a symmetric monoidal category can be depicted using string diagrams; this is a celebrated fact that underpins much of applied catgeory theory. It often happens, however, that one wishes to use special, additional icons in a string diagram language; more formally, this means every object is equipped with additional algebraic structure. For example, in a hypergraph category each object is equipped with a notion of wiring, or in a category with products each object has a diagonal map. In these cases, the minimal structure required for a nice string diagram language is a simple compatibility condition between the algebraic structures on each object and the monoidal product. If this condition holds, we say that the category supplies the structure.
In this talk I'll give some examples of supply, and outline a few theorems that show the compatibility condition is really what is necessary for nice diagrams. The material will form an accessible introduction to my paper with David of the above title.
October 17 : John Burnham (Sunshine Cybernetics)
November 21 : Alex Lew
Probabilistic modeling and inference are central tools in multiple fields, including artificial intelligence, statistics, and robotics, but can be tricky for practitioners to apply correctly. To make these techniques more accessible, probabilistic programming languages give users a formal language for expressing probabilistic models, and automate tedious and error-prone aspects of implementing Bayesian inference algorithms. But how can we think formally about what these tools are doing, and whether their inference engines are implemented correctly? And when the default inference algorithms don’t converge quickly enough, how can users tailor inference to the problem at hand without invalidating correctness guarantees?
In this talk, I’ll introduce the core ideas behind probabilistic programming languages and motivate the need for a formal approach to understanding their semantics. I’ll present a brief sketch of the recently introduced category of quasi-Borel spaces , which has been used to validate the correctness of several general-purpose inference algorithms for probabilistic programs . Finally, I’ll present a new extension to that work that allows programmers to customize the behavior of these inference algorithms on a per-model basis in a sound-by-construction manner, ensuring that the resulting inference algorithms are still correct.
 Chris Heunen, Ohad Kammar, Sam Staton and Hongseok Yang, A convenient cateogry for higher-order probability theory, Logic in Computer Science 2017.
 Ścibior, Adam, et al. "Denotational validation of higher-order Bayesian inference." Proceedings of the ACM on Programming Languages 2.POPL (2017): 60.
December 5 : Tai-Danae Bradley (CUNY)
January 16: Evan Patterson (Stanford)
The emerging field of applied category theory studies mathematical models of compositional processes in a unified, systematic way. However, going from a mathematical model, written on paper, to an operational method, realized in practice, is a challenge demanding significant effort. In particular, the computational tools supporting applied category theory are immature. Over the past several years, we have developed Catlab.jl, an early programming library and computer algebra system for applied category theory, written in Julia. Catlab provides data structures and algorithms for defining, manipulating, serializing, and visualizing symbolic expressions and wiring diagrams for different flavors of categories. In this talk, we introduce the design and some of the features of Catlab. We also discuss lessons learned along the way and how we hope to improve the system in the future.Slides available here.
January 23: Andrea Censi (ETH Zurich)
Category theory can be very useful for many domains of engineering, because the synthetic and rigorous language it provides can help describe and analyze complex systems. In this talk I will describe a categorical theory of “co-design” (collaborative, compositional, computational, continuous design) to be used to describe and solve formal engineering design problems. I will discuss the design and implementation of a formal co-design language. Finally, I will discuss the work to be done to achieve the representation power necessary to fully capture the domain of engineering design.Slides available here.
January 30: David Jaz Myers (Johns Hopkins)
A (closed) dynamical system is a notion of how things can be, together with a notion of how they may change given how they are. The idea and mathematics of closed dynamical systems has proven incredibly useful in those sciences that can isolate their object of study from its environment. But many changing situations in the world cannot be meaningfully isolated from their environment -- a cell will die if it is removed from everything beyond its walls. To study systems that interact with their environment, and to design such systems in a modular way, we need a robust theory of open dynamical systems.In this talk, I'll present a general definition of open dynamical system based on the idea of generaliz ed lenses due to Spivak. Given a particular notion of generalized lens (with a small bit of extra data), we'll construct a symmetric monoidal category of open dynamical systems and show how these systems can be connected using wiring diagrams. We'll see a handful of examples -- discrete, non-deterministic, probabilistic, continuous -- and show how a class of these, the discrete-time monadic open dynamical systems, can be implemented in Haskell.
February 6: James Fairbanks (Georgia Tech)
February 13: James Koppel and Cody Roux
James Koppel: Pushouts in Software Engineering -- You build something. Then Alice extends it one way. Then Bob extends it another way. Now you want to use both of their extensions, but they might not interoperate. How to reconcile? If you're a category theorist, you know the answer: pushouts! In this talk, we'll survey uses of pushouts in three domains: graph-rewriting (used in software modeling), specification refinement, and the generalization of equational rules.Cody Roux: Running with Cats -- We present a method, developed in the late 90s, to use properties of the category of presheaves/sheaves to give an operational semantics to various free categorical theories. This method has both theoretical and practical applications, not least of which is the ability to prove decidability of conversion, and build normalization algorithms, without messy considerations of rewriting theory.
February 20: David Jaz Myers (Johns Hopkins)
March 5: David Spivak (MIT)
The category Poly of polynomial functors on Set has excellent formal properties: it's a distributive category in two ways, it's tensored and cotensored over Set, etc. But its objects are simply polynomials P(x) in one variable, e.g. x^2+2x+1, and its morphisms are given by a very workable combinatorial structure.It turns out that there is a strong connection between polynomial functors and mode-dependent networks of dynamical systems, i.e. interacting dynamical systems that change who they wire to based on their internal state. The simpler mode-independent interfaces are the monomials Bx^A, where A is input and B is output. A dynamical system with state set S and mode-dependent interface P(x) is a morphism in Poly of the form Sx^S --> P(x). For example, a programmer might define a stream of B's to consist of a carrier set S and functions S->S and S->B; this is exactly the data of a map Sx^S --> Bx in Poly.
March 12: Alessandro Gianola (Free University of Bozen-Bolzano)
During the last two decades, a huge body of research has been dedicated to the challenging problem of reconciling data and process management within contemporary organizations. This requires to move from a purely control-flow understanding of business processes to a more holistic approach that also considers how data are manipulated and evolved by the process. In parallel, a flourishing series of results has been dedicated to the formalization of such integrated models, and to the study of the boundaries of decidability for their analysis and verification. However, in these integrated models a compositional description of the control-flow is still missing: indeed, it is not clear in the literature how to define the process component so as to guarantee the availability of significant semantic compositional operations. The lack of an algebra formalizing the control-flow makes very challenging the problem of describing and also verifying the combined models.
In this talk, I will present a categorical way for expressing fully compositional workflows, relying on the algebra of CospanSpan(Graph). In this model, the algebras employed to formalize finite-state control-flows are equipped with a plethora of algebraic operations: some of them can semantically be interpreted as sequential or parallel (with and without communication) composition of automata. However, the integration with data here is not supported yet.
Then, I will introduce the verification problem for DABs --- a data-aware extension of BPMN (Business Process Model and Notation), the standard language for modeling business processes --- to assess (parameterized) safety properties. Such integrated model exploits the model-theoretic framework of array-based systems, which allows to adapt the well-known backward reachability procedure in a full-fledged SMT (Satisfiability Modulo Theories) setting. By using suitable forms of quantifier elimination, backward reachability can be proved to be sound and complete for checking (un)safety, and interesting fragments where backward reachability is a full decision procedure can be isolated. Moreover, the SMT technology can be exploited in implementations, building on the well-known MCMT model checker for array-based system.Finally, I will argue why the DAB model seems to be the right candidate to incorporate the compositional description of control-flows provided by CospanSpan(Graph).
March 19: Paolo Perrone (MIT)
We all know that the sum 1+2+4 can be evaluated to 7. What is less known, but just as easy, is that 1+2+4 can be also *partially* evaluated to 3+4. We say that the formal expressions 1+2+4 and 3+4 are related by a partial evaluation. This notion can be generalized from natural numbers to algebras over an arbitrary monad, and sometimes it gives known constructions (such as the factorization of natural numbers, and conditional expectations in measure theory).
A more difficult problem is the following. Given three formal expressions s, t and u, suppose that s and t are related by a partial evaluation, and that t and u are as well. Can we conclude that s and u are directly related by a "composite" partial evaluation? Perhaps surprisingly, the answer is not always positive, and almost never easy to get.
We can solve this problem in a number of cases borrowing methods from homotopy theory. Partial evaluations can be seen as edges between formal expressions, forming the 1-dimensional skeleton of a canonical simplicial set called the bar construction. The geometry of this simplicial set can say a lot about when and how partial evaluations compose.
This way we can show, for example, that a composite partial evaluation always exists for the case of cartesian and weakly cartesian monads.This is a joint work with my ACT 2019 group (Tobias Fritz, Carmen Constantin, Martin Lundfall, Brandon Shapiro)
March 26: David Jaz Myers (Johns Hopkins University)
Homotopy Type Theory is a new foundations of mathematics which starts by asking what what it means to identify two mathematical objects. It depends on what type of objects they are: to identify the tangent space of the sphere at (0,0,1) with R^2, we need to choose a basis; to identify H^n(S^n; Z) with Z, we need to choose an orientation of the n-sphere; and to identify the smallest perfect number n with 6, we must prove that n = 6. So, type theory concerns itself with what type of thing everything is. As a result, we can derive what it means to identify two objects just from knowing what type of things they are.This later property is very useful in category theory, where one is often tempted to say "...and with the obvious morphisms". In this talk, we will see how the HoTT point of view influences categorical practice. We'll see that universal properties give a unique way to identify an object, and therefore there are no issues with choosing functorial representatives of limits, or constructing an inverse to an essentially surjective, fully faithful functor -- even if one does not assume any choice principles.
April 2: Todd Trimble (Western Connecticut State University)
April 9: John Baez (UC Riverside)
April 16: Joachim Kock (Universitat Autònoma de Barcelona)
Starting from any operad P, one can consider on one hand the free operad on P, and on the other hand the Baez--Dolan construction on P. These two new operads have the same space of operations, but with very different notions of arity and substitution. The main result is that the incidence bialgebras of the two-sided bar constructions of the two operads constitute together a comodule bialgebra. The motivating example is the Calaque--Ebrahimi-Fard--Manchon comodule bialgebra of trees from numerical analysis. The purpose of the talk is to explain all the concepts mentioned in the abstract, and also some background on polynomial monads, simplicial groupoids, and homotopy combinatorics.Reference: http://arxiv.org/abs/1912.11320
April 23: Joe Moeller (UC Riverside)
April 30: Sophie Libkind (Stanford)
Dynamical systems describe the evolution of physical and computational processes. Although they are traditionally studied as changing systems in a static environment, applied category theorists have been interested in studying open dynamical systems whose evolution both affects and depends on other systems in its environment. Two flavors of open dynamical systems include (1) Spivak's input/output machines which compose by feeding the output of one machine into the input of another, and (2) the input/output agnostic systems defined by Baez and Pollard to describe chemical reaction networks and which compose by sharing resources.In this talk, we will examine the differences between these two approaches to the "openness" of open dynamical systems and define an algebra which unifies these perspectives. We will consider in detail two examples: continuous flows on a manifold induced by a vector field and non-deterministic finite state automata.
May 7: Bob Coecke (CQC & Oxford Uni)
Recently we performed quantum natural language processing on an IBM quantum computer . What got us to the point is the observation that quantum theory and natural language are governed by much of the same category-theoretic structure . From a ML perspective, QNLP is arguably the first form of compositional machine learning where composition embodies a fundamental structure of the data involved, and which is moreover also native to the hardware it is implemented on.
The talk requires no background in quantum theory, nor in natural language theory, nor in machine learning. All relevant references are in [1, 2], where there are also the names of the people involved in getting to this point.
 B. Coecke, G. De Felice, K. Meichanetzidis & A. Toumi (2020) Quantum Natural Language Processing: We did it! https://medium.com/cambridge-quantum-computing/quantum-natural-language-processing-748d6f27b31d. B. Coecke (2016) From quantum foundations via natural language meaning to a theory of everything. arXiv:1602.07618.
May 14: Mike Shulman (San Diego)
Dual objects in monoidal categories have many applications, including channels in parallel programming, input-output modes in logic programming, and string diagrams for internal-homs. Thus, it is natural to ask whether duals intrinsically strengthen the theory, i.e. whether monoidal categories with duals are "conservative", in a suitable sense, over monoidal categories without duals. While "compact closed" duals are not generally conservative, we show that "∗-autonomous" duals frequently are: in particular, the free extension of any closed symmetric monoidal category to a ∗-autonomous category is a fully faithful embedding. Thus, "richer" languages with ∗-autonomous duals can be unambiguously used to reason about "poorer" languages that lack them.This talk is about the same paper as my talk at ACT@UCR (video, slides), but the talks will be complementary, with no expectation that anyone attending this talk has seen the other one.
May 21: Jade Master (UC Riverside)