Extensional Type Theory

A kind of type theory with:

• Equality Reflection and
• Uniquieness of Identity Proofs.

“Intuinistic set theory”

See also

Type Theory

Source

https://www.youtube.com/watch?v=u92V0OMgvhM&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z