Extensional Type Theory

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:

\frac
{\Gamma\vdash p:x≡_Ay}
{\Gamma\vdash x=y}

Where ≡ is propositional equality and = is definitional equality.

It corresponds to locally cartesian closed categories.

References

ETT was introduced by Martin-Loef in the paper ...