Skip to main content

All Questions

Tagged with
10 votes
0 answers
175 views

What are the practical differences between intensional and extensional type theories?

It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
Trebor's user avatar
  • 4,025