Equivalence of inductive and parametric naturals in RelTT
I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent. This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.
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.