0 | module Control.Function.FunExt
 1 |
 2 | %default total
 3 |
 4 | ||| This interface contains a proposition for the function extensionality.
 5 | ||| It is not meant to be ever implemented.
 6 | ||| It can be used to mark properties as requiring function extensionality to hold,
 7 | ||| i.e. its main objective is to provide a universal way to formulate a conditional property
 8 | ||| that holds only in the presence of function extensionality.
 9 | public export
10 | interface FunExt where
11 |   funExt : {0 b : a -> Type} -> {0 f, g : (x : a) -> b x} -> ((x : a) -> f x = g x) -> f = g
12 |
13 | export
14 | funExt0 : FunExt => {0 b : a -> Type} -> {0 f, g : (0 x : a) -> b x} -> ((x : a) -> f x = g x) -> f = g
15 | funExt0 prf = rewrite funExt {f = \x => f x} {g = \y => g y} prf in Refl
16 |
17 | export
18 | funExt1 : FunExt => {0 b : a -> Type} -> {0 f, g : (1 x : a) -> b x} -> ((x : a) -> f x = g x) -> f = g
19 | funExt1 prf = rewrite funExt {f = \x => f x} {g = \y => g y} prf in Refl
20 |