Iowa Type Theory Commute

Basics of subtyping

Aaron Stump Season 4 Episode 11

In this episode, I discuss a few of the basics for what we expect from a subtyping relation on types: reflexivity, transitivity, and the variances for arrow types.