Coercive subtyping and coherence

Iowa Type Theory Commute by Aaron Stump

In this episode, I give further arguments in favor of coercive subtyping from a software-engineering perspective. I also explain the critical concept of coherence.