Other material
CK example, 2.2.ii
This module defines (only) the functor for CK. Proving the functor properties requires extentionality of functions and predicates.
Require
Export
functor
image
.
Section
CK
.
Hypothesis
fun_ext
:
∀
(
A
B
:
Type
)(
f
g
:
A
→
B
),
(
∀
(
a
:
A
),
f
a
=
g
a
) →
f
=
g
.
Hypothesis
pred_ext
:
∀
(
A
:
Type
)(
P
Q
:
A
→
Prop
),
(
∀
(
a
:
A
),
P
a
↔
Q
a
) →
P
=
Q
.
Definition
ck_functor
:
functor
.
End
CK
.