August 30, 2021
You Could Have Invented De Bruijn Indices
Posted by Mike Shulman
One of the most curious things about formal treatments of type theory is the attention paid to dummy variables. The point is simple enough to explain to a calculus student: just as the integrals and are equal, so are the functions and — the name of the variable doesn’t matter. (In fact, the former statement factors through the latter.) But managing this equality (which goes by the highbrow name of “-equivalence”) turns out to be quite fiddly when actually implementing a typechecker, and people have developed all sorts of different-sounding ways to deal with it, with names like De Bruijn indices, De Bruijn levels, locally named terms, locally nameless terms, and so on.
In this post I want to explain what’s going on from a categorical and/or univalent perspective, and why some of these fancy-sounding things are really quite simple. To cut to the punchline, at bottom what’s going on is just different ways to choose a concrete representative of an object that’s determined only up to unique isomorphism.
August 23, 2021
Cospans and Computation - Part 2
Posted by John Baez
guest post by Angeline Aguinaldo as part of the Adjoint School for Applied Category Theory 2021
In this second part we discuss an application of structured cospans to network security!
August 11, 2021
Logic as Invariant Theory Revisited
Posted by David Corfield
Some years ago I wrote a brief post on Friederich Mautner’s ‘An Extension of Klein’s Erlanger Program: Logic as Invariant-Theory’. Inspired by Weyl’s linkage of the representation theory of classical groups to invariant theory, this 1946 paper marked the first appearance of an idea, later taken up by Tarski and developed by many (nLab), that logic concerns what is invariant under the most general transformations, permutations of the universe of discourse.
With the coming of HoTT/Univalent Foundations, I think it’s worth revisiting this question. In my recent book I claimed, rather vaguely, that we find that “the boundary between logic and mathematics blurs” (MHTT, p. 89). This was inspired by the sight of people working out things like the 4th homotopy group of the 3-sphere in pure HoTT:
Guillaume Brunerie, The James construction and in homotopy type theory, (arXiv:1710.10307).
But what if we could be more precise about the new boundary of the logical?
August 10, 2021
Cospans and Computation - Part 1
Posted by John Baez
guest post by Anna Knörr as part of the Adjoint School for Applied Category Theory 2021
A socratic dialogue on composition! Listen in to what Synthesi has to say about scientific modelling, the programming language AlgebraicJulia and more. Join us on this playful journey towards computing with cospans in a series of blog posts, inspired by conversations at the ACT Adjoint School 2021.
August 7, 2021
Why Aren’t You Making Math(s) Videos?
Posted by Simon Willerton
Over at 3Blue1Brown Grant Sanderson is asking the provocative question “Why aren’t you making math videos?”
Certainly for many of us there are reasons which include things such as lack of time or energy. However, if you have time, energy and desire but lack the encouragement, then perhaps this is for you.
To encourage more people to make videos explaining maths, last month Grant launched a competition: The Summer of Math Exposition. The idea is simply to make a expositional maths video and submit it. The deadline is 22nd August so you’d better get your skates on if you want to do it.
In the video at the link above, Grant gives some good hints and tips on how to get started. The first and foremost of these is the very sensible “Just start!”, certainly that’s what Eugenia and I did with the Catsters – there was no careful planning beforehand. As the story goes, we broke into Tom Bridgeland’s office one evening, ‘borrowed’ his webcam and just started making videos.
Anyway you have two weeks, which doesn’t give too much opportunity for procrastination!
Optimal Transport and Enriched Categories III: Duality Within Pricing
Posted by Simon Willerton
So far in this series I’ve been writing about the optimal transport problem of deciding how many goods to send from suppliers to recievers in order to minimize transport costs whilst satisfying supply and demand constraints. I showed that there is an equivalent dual transport problem which involves fixing ‘prices’ of the goods at the suppliers and receivers subject which maximizes revenue subject to some competitivity constraints.
This time I will show that there is a duality within the dual problem, a duality between prices at suppliers and prices at receivers. I learnt about this from Chapter 5 of Cedric Villani’s Optimal Transport. I will then show that this nicely and naturally fits in to an enriched cateogry framework: the transport cost matrix being viewed as an enriched profunctor and the duality arising via an adjunction associated to the matrix.
My group at this year’s Applied Category Theory Adjoint School was looking at related matters – we should get some blog posts from them here soon – and Elise Catania’s part of the group presentation at ACT2021 was based on this material, but it doesn’t seem as though the videos have gone up for the Adjoint School presentations.
August 3, 2021
The Two Cultures Challenge Revisited
Posted by David Corfield
Since I was reminded of the ‘Two cultures’ discussions (I and II) while replying to John on the other thread, I wonder if with the advantage of 14 more years we can now meet Terry Tao’s challenge to provide a category-theoretic proof of
If is a function between finite sets, then .
We were also given a simpler and a more general version:
If and are disjoint sets, then is at least as large as .
If and then is at least as large as .
Terry’s summary here is handy, pointing out that Robin Houston had got us part of the way, here.
I see back then Urs was wondering if Tom’s new ideas on cardinality were relevant.
Something for the automated theorem provers, perhaps.