On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual type for Church-encoded natural numbers implies induction. RelTT uses a generalization of these ideas to derive induction for any positive type family.
The podcast Iowa Type Theory Commute is embedded on this page from an open RSS feed. All files, descriptions, artwork and other metadata from the RSS-feed is the property of the podcast owner and not affiliated with or validated by Podplay.