Extensionality.idr

Function Extensionality

Idris does not feature function extensionality like OTT or HoTT, and because of our use of propositional equality, we have to postulate it to use it.

Postulate

Function extensionality.

0 funExt : {f, g : a -> b} -> ((x : a) -> f x === g x) ->  f === g

Sometimes we need a dependent version of function extensionalty as well.

Postulate

Dependent function extensionality.

0 funExtDep : {a : Type} -> {b : a -> Type} -> {f, g : (x : a) -> b x} ->
              ((x : a) -> f x === g x) ->  f === g

Lemma

Given an equality between two functions $f:a\to b$ and $g:a\to b$ we can obtain the equality $fx\equiv fx$ given a value $x:a$.

applySame : {f, g : a -> b} -> (x : a) -> f === g -> f x === g x
applySame x Refl = Refl