The n-Category Café

“Solid ring” sounds self-contradictory, since a ring should have a hole in it. But mathematicians use words in funny ways.

guest post by Nuiok Dicaire and Paul Lessard

Many well-known type theories, Martin-Löf dependent type theory or linear type theory for example, were developed as syntactic treatments of particular forms of reasoning. Constructive mathematical reasoning in the case of Martin-Löf type theory and resource dependent computation in the case of linear type theory. It is after the fact that these type theories provide convenient means to reason about locally Cartesian closed categories or $\star$-autonomous ones. In this post, a long overdue part of the Applied Category Theory Adjoint School (2020!?), we will discuss a then recent paper by Mike Shulman, A Practical Type Theory for Symmetric Monoidal Categories, where the author reverses this approach. Shulman starts with symmetric monoidal categories as the intended semantics and then (reverse)-engineers a syntax in which it is practical to reason about such categories.

The University of San Diego mathematics department is hiring! We have two assistant professor positions open this year; these are starting tenure-track positions. Applications must be through the USD web site; the deadline is November 15, 2021.

The University of San Diego (not to be confused with the University of California, San Diego) is a relatively small private Catholic university. The university as a whole has a few graduate programs in different academic units, but the math department is in the College of Arts and Sciences, which is a purely undergraduate liberal arts college. The standard teaching expectation is 3 courses per semester on average, although internal or external grants can reduce that a bit. It’s not a place to work unless you love undergraduate teaching as well as research. But for those who do, I think it’s a great place that supports both, with an administration and colleagues who care about both.

Because our focus is primarily on teaching, we don’t generally look for any particular research areas when hiring; but of course I would personally be happy to see applications from any $n$-Category Café patrons. In addition, this year all hires in the university are supposed to align with one of three “cluster themes” of “Climate Change & Environmental Justice”, “Technology & the Human Experience”, and “Borders & Social Justice”; applicants must include a cover letter explaining how their work aligns with one or more of these clusters, broadly interpreted.

Feel free to contact me personally with any questions.

guest post by Angeline Aguinaldo and Anna Knörr as part of the Adjoint School for Applied Category Theory 2021

Synthesi and Socrates are back! What have they learnt from Part 2 in our series of blog posts on computing with cospans?

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 $\int_0^2 x^3 \, dx$ and $\int_0^2 t^3 \, dt$ are equal, so are the functions $\lambda x. x^3$ and $\lambda t. t^3$ — 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 “$\alpha$-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.

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!

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 $\pi_4(S^3)$ in homotopy type theory, (arXiv:1710.10307).

But what if we could be more precise about the new boundary of the logical?

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.

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!

• Part I
• Part II

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.

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 $f: X \to Y$ is a function between finite sets, then $|X \times_{f} X| \geq |X|^2/|Y|$.

We were also given a simpler and a more general version:

If $X$ and $Y$ are disjoint sets, then $(X \times X) \cup (Y \times Y)$ is at least as large as $(X \times Y) \cup (Y \times X)$.

If $f: X \to Y$ and $g: Z \to Y$ then $(X \times_Y X) \times (Z \times_Y Z)$ is at least as large as $(X \times_Y Z) \times (Z \times_Y X)$.

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.

Back in 2005 or so, John Baez was giving talks about groupoid cardinality, Euler characteristic, and strange objects with two and a half elements.

I saw a version of this talk at Streetfest in Sydney, called The Mysteries of Counting. It had a big impact on me.

This post makes one simple point: that by thinking along the lines John advocated, we can arrive at the exponential of Shannon entropy — otherwise known as diversity of order $1$.

There was an interesting talk that took place at the Topos Institute recently – Topos theory and measurability – by Asgar Jamneshan, bringing category theory to bear on measure theory.

Jamneshan has been working with Terry Tao on this:

• Asgar Jamneshan, Terence Tao, Foundational aspects of uncountable measure theory: Gelfand duality, Riesz representation, canonical models, and canonical disintegration (arXiv:2010.00681)

The topos aspect is not emphasized in this paper, but it seems to have grown out of a post by Tao – Real analysis relative to a finite measure space – which did.

My new book, Entropy and Diversity: The Axiomatic Approach, is in the shops!

If you live in a place where browsing the shelves of an academic bookshop is possible, maybe you’ll find it there. If not, you can order the paperback or hardback from CUP. And you can always find it on the arXiv.

I posted here when the book went up on the arXiv. It actually appeared in the shops a couple of months ago, but at the time all the bookshops here were closed by law and my feelings of celebration were dampened.

But today someone asked a question on MathOverflow that prompted me to write some stuff about the book and feel good about it again, so I’m going to share a version of that answer here. It was long for MathOverflow, but it’s shortish for a blog post.

Ask around for an example of ordinary mathematics that uses the axiom scheme of replacement in an essential way, and someone will probably say “the Borel determinacy theorem”. It’s probably the most common answer to this question.

As an informal statement, it’s not exactly wrong: there’s a precise mathematical result behind it. But I’ll argue that it’s misleading. It would be at least as accurate, arguably more so, to say that Borel determinacy does not require replacement.

For the purposes of this post, it doesn’t really matter what the Borel determinacy theorem says. I’ll give a lightning explanation, but you can skip even that.

Thanks to David Roberts for putting me onto this. You can read David’s recent MathOverflow question on this point too.