Comment by pixelpoet
4 years ago
I like the bit at the end giving credit to trains:
> I feel very lucky to have stumbled on this interpretation of differentiation for datatypes with such potential for both utility and fascination, and has been intriguing me since the day I made the connection (whilst changing trains at Shrewsbury). This work has benefited greatly from hours spent on trains, [...]
My favorite is from Bob Atkey's Quantitative Type Theory paper:
> This work is dedicated to Orwell the dog. Orwell was a good dog and knew well the difference between zero, one, and many
https://bentnib.org/quantitative-type-theory.pdf
(zero, one, many was the ring that the paper used.)