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

0 FunExt0 : ((0 _ : a) -> b) -> ((0 _ : a) -> b) -> Type

Totality: total
Visibility: public export

0 funext0 : (f : ((0 _ : a) -> b)) -> (g : ((0 _ : a) -> b)) -> FunExt0 f g -> f = g

Totality: total
Visibility: export

0 DepFunExt : (b : (a -> Type)) -> ((x : a) -> b x) -> ((x : a) -> b x) -> Type

Totality: total
Visibility: public export

0 depfunext : (b : (a -> Type)) -> (f : ((x : a) -> b x)) -> (g : ((x : a) -> b x)) -> DepFunExt b f g -> f = g

Totality: total
Visibility: export

0 DepFunExtI : (b : (a -> Type)) -> b x -> b x -> Type

Totality: total
Visibility: public export

0 depfunexti : (b : (a -> Type)) -> (f : b x) -> (g : b x) -> DepFunExtI b (\{x:5917} => f) (\{x:5921} => g) -> (\{x:5931} => f) = g

Totality: total
Visibility: export

0 DepFunExt0 : (b : (a -> Type)) -> ((0 x : a) -> b x) -> ((0 x : a) -> b x) -> Type

Totality: total
Visibility: public export

0 depfunext0 : (b : (a -> Type)) -> (f : ((0 x : a) -> b x)) -> (g : ((0 x : a) -> b x)) -> DepFunExt0 b f g -> f = g

Totality: total
Visibility: export

0 depcurryfunext : (b : (a -> Type)) -> (c : ((x : a) -> b x -> Type)) -> (f : ((x : a) -> (y : b x) -> c x y)) -> (g : ((x : a) -> (y : b x) -> c x y)) -> DepFunExt (\{lamc:0} => let (x ** y) = {lamc:0} in c x y) (\{lamc:0} => let (x ** y) = {lamc:0} in f x y) (\{lamc:0} => let (x ** y) = {lamc:0} in g x y) -> f = g

Totality: total
Visibility: export