BeTTI.FunExt

Definitions

0 FunExt : (a -> b) -> (a -> b) -> Type

Totality: total
Visibility: public export

0 funext : (f : (a -> b)) -> (g : (a -> b)) -> FunExt f g -> f = g

Totality: total
Visibility: export