Library nijn.Prelude.Funext
Require
Import
Coq.Logic.FunctionalExtensionality
.
Functional extensionality
In most of this formalization, we assume functional extensionality. For that, we use the following abbreviation.
Definition
funext
{
A
:
Type
}
{
B
:
A
→
Type
}
{
f
g
:
∀
(
a
:
A
),
B
a
}
(
p
:
∀
(
a
:
A
),
f
a
=
g
a
)
:
f
=
g
.
Proof
.
apply
functional_extensionality_dep
.
exact
p
.
Qed
.
UIP
Axiom
UIP
:
∀
{
A
:
Type
} {
a1
a2
:
A
} (
p
q
:
a1
=
a2
),
p
=
q
.