plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.36k stars 307 forks source link

updated extra/Subtyping-phil.lagda.md #1017

Closed wadler closed 2 months ago

wadler commented 2 months ago

Improved the definition of Type and Type*. (After a discussion with Jeremy and Peter.)