@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! 🤩

https://youtu.be/bp4yvTRM3DQ

Joint work with Carlo Angiuli and @totbwf

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

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.

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!!

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.

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!

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!

- Pronouns
- He/Him

Type Theory/Category Theory

I like proof assistants and make them too!

Joined Sep 2021