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?
