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 and extensional type theories are well characterized.

I'm interested in how actual implementations and usage of these two flavors of type theories differ. I would speculate that, if UIP and function extensionality is embraced, and the elaborator is smart enough to insert silent coercions along equalities, then ITT would behave exactly the same as ETT. On the other hand, since type checking in ETT is in general undecidable, the user still have to insert some annotations here and there. Are there any notable differences in practical usage between ITT and ETT?

  • 1
    $\begingroup$ What does it mean for two type theories to be "equivalent"? $\endgroup$ Commented Mar 17, 2022 at 7:28
  • $\begingroup$ Perhaps you mean that MLTT with equality reflection is conservative over IMLTT+UIP+FE? $\endgroup$ Commented Mar 18, 2022 at 18:07


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.