Extensional type theory (ETT) is a system of Martin-Loef type theory that features extensional identity types. It is summarized by the equality reflection rule:
Where is propositional equality and is definitional equality.
It corresponds to locally cartesian closed categories.
ETT was introduced by Martin-Loef in the paper ...