Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.

Function extensionality

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 ≡ g

Unfortunately, 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.

Go back to the table of contents