September 26, 2018
A Communal Proof of an Initiality Theorem
Posted by Mike Shulman
One of the main reasons I’m interested in type theory in general, and homotopy type theory (HoTT) in particular, is that it has categorical semantics. More precisely, there is a correspondence between (1) type theories and (2) classes of structured categories, such that any proof in a particular type theory can be interpreted into any category with the corresponding structure. I wrote a lot about type theory from this perspective in The Logic of Space. The basic idea is that we construct a particular structured category out of the syntax of the type theory, and prove that it is the initial such category. Then we can interpret any syntactic object in a structured category by regarding as living in and applying the unique structured functor .
Unfortunately, we don’t currently have any very general definitions of what “a type theory” is, what the “corresponding class of structured categories” is, or a very general proof of this “initiality theorem”. The idea of such proofs is easy — just induct over the construction of syntax — but its realization in practice can be long and tedious. Thus, people are understandably reluctant to take the time and space to write out such a proof explicitly, when “everyone knows” how the proof should go and probably hardly anyone would really read such a proof in detail anyway. This is especially true for dependent type theory, which is qualitatively more complicated in various ways than non-dependent type theories; to my knowledge only one person (Thomas Streicher) has ever written out anything approaching a complete proof of initiality for a dependent type theory.
Applied Category Theory Course: Collaborative Design
Posted by John Baez
My online course is now done. We finished the fourth chapter of Fong and Spivak’s book Seven Sketches—my classes at U.C.R. are starting up now, so I had to stop there.
Chapter 4 is about collaborative design: building big projects from smaller parts. This is based on work by Andrea Censi:
- Andrea Censi, A mathematical theory of co-design.
The main mathematical content of this chapter is the theory of enriched profunctors. We’ll mainly talk about enriched profunctors between categories enriched in monoidal preorders. The picture above shows what one of these looks like!
September 21, 2018
A Pattern That Eventually Fails
Posted by John Baez
Sometimes you check just a few examples and decide something is always true. But sometimes even examples is not enough.
September 20, 2018
Cartesian Double Categories
Posted by Mike Shulman
In general, there are two kinds of bicategories: those like and those like . In the -like ones, the morphisms are “categorified functions”, which generally means some kind of “functor” between some kind of “category”, consisting of functions mapping objects and arrows from domain to codomain. But in the -like ones (which includes and ), the morphisms are not “functors” but rather some kind of “generalized relations” (including spans, modules, profunctors, and so on) which do not map from domain to codomain but rather relate the domain and codomain in some way.
In -like bicategories there is usually a subclass of the morphisms that do behave like categorified functions, and these play an important role. Usually the morphisms in this subclass all have right adjoints; sometimes they are exactly the morphisms with right adjoints; and often one can get away with talking about “morphisms with right adjoints” rather than making this subclass explicit. However, it’s also often conceptually and technically helpful to give the subclass as extra data, and arguably the most perspicuous way to do this is to work with a double category instead. This was the point of my first published paper, though others had certainly made the same point before, and I think more and more people are coming to recognize it.
Today a new installment in this story appeared on the arXiv: Cartesian Double Categories with an Emphasis on Characterizing Spans, by Evangelia Aleiferi. This is a project that I’ve wished for a while someone would do, so I’m excited that at last someone has!
September 19, 2018
p-Local Group Theory
Posted by John Baez
I’ve been trying to learn a bit of the theory of finite groups. As you may know, Sylow’s theorems say that if you have a finite group , and is the largest power of a prime that divides the order of , then has a subgroup of order , which is unique up to conjugation. This is called a Sylow -subgroup of .
Sylow’s theorems also say a lot about how many Sylow -subgroups has. They also say that any subgroup of whose order is a power of is contained in a Sylow -subgroup.
I didn’t like these theorems as an undergrad. The course I took whizzed through them in a desultory way. And I didn’t go after them myself: I was into group theory for its applications to physics, and the detailed structure of finite groups doesn’t look important when you’re first learning physics: what stands out are continuous symmetries, so I was busy studying Lie groups.
Since I didn’t really master Sylow’s theorems, and had no strong motive to do so, I didn’t like them — the usual sad story of youthful mathematical distastes.
But now I’m thinking about Sylow’s theorems again, especially pleased by Robert A. Wilson’s one-paragraph proof of all three of these theorems in his book The Finite Simple Groups. And I started wondering if the importance of groups of prime power order — which we see highlighted in Sylow’s theorems and many other results — is all related to localization in algebraic topology, which is a technique to focus attention on a particular prime.
September 18, 2018
What is Applied Category Theory?
Posted by John Baez
Tai-Danae Bradley has a new free book:
- Tai-Danae Bradley, What is Applied Category Theory?
Abstract. This is a collection of introductory, expository notes on applied category theory, inspired by the 2018 Applied Category Theory Workshop, and in these notes we take a leisurely stroll through two themes (functorial semantics and compositionality), two constructions (monoidal categories and decorated cospans) and two examples (chemical reaction networks and natural language processing) within the field.
This book grew out of the workshop Applied Category Theory 2018, which she attended. I think it makes a great complement to Fong and Spivak’s Seven Sketches and my online course.
Check it out!
September 5, 2018
A Categorical Look at Random Variables
Posted by Tom Leinster
guest post by Mark Meckes
For the past several years I’ve been thinking on and off about whether there’s a fruitful category-theoretic perspective on probability theory, or at least a perspective with a category-theoretic flavor.
(You can see this MathOverflow question by Pete Clark for some background, though I started thinking about this question somewhat earlier. The fact that I’m writing this post should tell you something about my attitude toward my own answer there. On the other hand, that answer indicates something of the perspective I’m coming from.)
I’m a long way from finding such a perspective I’m happy with, but I have some observations I’d like to share with other n-Category Café patrons on the subject, in hopes of stirring up some interesting discussion. The main idea here was pointed out to me by Tom, who I pester about this subject on an approximately annual basis.