@totbwf purchasing a bag of NIST Standard Reference Lambda Abstractions

The recording of the POPL 2023 talk “An Order-Theoretic Analysis of Universe Polymorphism” is already on YouTube! 🤩
youtu.be/bp4yvTRM3DQ
Joint work with Carlo Angiuli and @totbwf

The best part about conferences is inventing new type theory crimes over dinner

Is there a notion of "bicategories where all morphisms have left and right adjunctions"?

They have taken us all off the plane, just to put us all back on the plane

Show thread

How did we make the miracle of flight so horrible

the last one from this meeting: it's impossible to prove that the no-eta-equality record with zero fields is an hprop

Show thread

I intentionally spent a lot of time writing about the general principles and constraints governing the design of #ToolsForMathematicalThought without actually writing about the tool that I was creating. I am now ready to proceed from the general to the particular, and am beginning to write about how to use Forester to start your own Stacks Project in ten minutes.

Still can’t believe that Vancouver has a political party called COPE lmao

You have to make the units and counits meet in the middle, which involves this fun bit of snoc list code.

Uphold Snoc List Thought!!

Show thread

The normalization algorithm for adjoints is so much fun

Fun little lemma: If you have a pair of displayed functors `L : E -> F`, `R : F -> E` that are vertically adjoint (unit and counit are vertical natural transformations, both L and R displayed over the identity functor), then R preserves cartesian morphisms, and L preserves cocartesian morphisms.

This is particularly handy for fibred limits/opfibred colimits: we define (co)limits as left/right fibred adjoints to the displayed constant diagram functor, so this lemma allows us to avoid some annoying busywork proving that these left/right adjoints are (op)fibred.

Love it when my set of base types isn't stable under kind substitutions!

Show thread

The definition of a polymorphic signature in Jacobs is so scuffed

Fun little fact about the externalization of an internal category: the Cartesian maps are the *internal* isomorphisms: this really hammers home that externalization is the internalized family fibration!

This time it’s internal categories: we can avoid pullback hell by doing the internal language trick from before, but the naturality conditions for internal functors/natural transformations require PathP!

Show thread

Every time I try and take a break from something that involves a ton of PathP it ends up showing up anyways 🙃​

The TL;DR is that if we have some internal structure in $C$, we can look at it in the internal language and we will get something that looks like the external version of the structure. In this case, we are looking at internal monoids $(M, \mu, \eta)$ in $C$, which implies that every hom set $C(X, M)$ is a monoid.

We can then ask when the converse of this holds, IE: if every hom set $C(X, M)$ is a monoid, is $M$ an internal monoid? This happens when the hom-set monoids are defined naturally; from a type theory POV, this means that the monoid structure in the internal language is stable under substitution.

It turns out that these naturally-defined monoids on hom sets are actually equivalent to the data of a representable functor of monoids, which is pretty compelling!

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.