You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Patrick Nicodemus (Jan 31 2024 at 01:05):In category theory, when teaching the naturality condition for a natural transformation we often say that naturality captures the fact that it is somehow made without reference to any specific properties of the elements involved, in an ad-hoc way that depends somehow on the set or the elements of the set.
However, it is difficult to make this intuition precise and rigorous, it is not obvious how to make it a precise mathematical statement that "no ad hoc choices are involved, it is uniform." I do not think that it should be considered a rigorous proof to say "We have made no ad hoc choices, so it is obviously natural".
Using the axiom of choice we can easily prove the existence of non-natural transformations.
But in type theory, we can actually express the concept of "abstraction" in a way that we cannot in set theory, we can express that a construction is polymorphic in its input type, which is a kind of abstraction away from the details of the type that cannot be expressed in set theory.
I was somewhat shocked to come across the following paper by Wadler where he opens with the following theorem:
Every un-natural endo-transformation of the List functor (free monoid monad) in polymorphic type theory (i.e., prima facie not necessarily having to be coherent with the action on morphisms) is automatically natural.
He then goes on to prove a general class of theorems of this form about polymorphic type constructors. I thought this was incredible, it's insane that I was not aware of it.
https://dl.acm.org/doi/pdf/10.1145/99370.99404
Mike Shulman (Jan 31 2024 at 01:08):Yeah, parametricity is mind-blowing!
Ralph Sarkis (Jan 31 2024 at 04:09):I also just discovered this in yesterday's stream of Binary Operation. I found some interesting complementary discussion here.
Patrick Nicodemus (Jan 31 2024 at 04:23):Oh, I'm sure I must have seen that post and forgotten it but the paper title stuck in my head.