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.