BROADCASTS.com

b'

In this episode, I discuss the basic distinguishing rule of Extensional Martin-Loef Type Theory, namely equality reflection.\\xa0 This rule says that propositional equality implies definitional equality.\\xa0 Algorithmically, it would imply that the type checker should do arbitrary proof search during type checking, to see if two expressions are definitionally equal.\\xa0 This immediately gives us undecidability of type checking for the theory, at least as usually realized.