Podcasts Technology Iowa Type Theory Commute Equivalence of inductive and parametric naturals in RelTT

Equivalence of inductive and parametric naturals in RelTT

Published: Dec. 28, 2020, 6 a.m.

b'

I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent.\\xa0 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.

'