Library CatSem.AXIOMS.functional_extensionality
Set
Implicit
Arguments
.
Unset
Strict
Implicit
.
Axiom
functional_extensionality
:
forall
(
A
B
:
Type
)(
f
g
:
A
->
B
),
(
forall
x
,
f
x
=
g
x
) ->
f
=
g
.