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.