Chapter 18: Extensionality in Type Theory
In type theory, function extensionality is the principle
equating two functions at (for a simple version) type A arrow B iff they map inputs that are equal at type A to outputs equal at type B.
In this chapter, I discuss some of the results others have obtained on extensionality.