Iowa Type Theory Commute
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Iowa Type Theory Commute
Extensional Martin-Loef Type Theory
•
Aaron Stump
•
Season 4
•
Episode 6
Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.
In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection. This rule says that propositional equality implies definitional equality. Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal. This immediately gives us undecidability of type checking for the theory, at least as usually realized.