Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.
Recall that we defined pointwise equality f ∼ g of functions in the identity type handout.
The principle of function extensionality says that pointwise equal functions are equal and is given by the following type FunExt:
open import identity-type
FunExt = {A : Type} {B : A → Type} {f g : (x : A) → B x} → f ∼ g → f ≡ gUnfortunately, this principle is not provable or disprovable in Agda or MLTT (we say that it is independent). But it is provable in Cubical Agda, which is based on Cubical Type Theory and is outside the scope of these lecture notes. Sometimes we will use function extensionality as an explicit assumption.