Yoneda as a CPS transformer

cps.v

(* http://m-hiyama.hatenablog.com/entry/20080116/1200468797 *)

Module cps.

(* CPS transformation *)
Definition yoneda (X Y A: Type) (f: X -> Y) : (Y -> A) -> X -> A :=
  fun cont: Y -> A => fun x: X => cont (f x).

Definition yoneda_objpart (X A: Type) (x: X) : (X -> A) -> A :=
  fun cont: X -> A => cont(x).

Definition f (x: nat) : nat := x + 1.
Definition g (x: nat) : nat := x * 2.

Example yoneda_nat: forall A: Type, forall cont: nat -> A, forall a: nat,
  ((yoneda nat nat A f) ((yoneda nat nat A g) cont)) a = (yoneda nat nat A (fun x: nat => g (f x))) cont a.
Proof.
  intros A cont a.
  reflexivity.
Qed.

Theorem yoneda_is_contravariant_functor : forall X Y Z A: Type, forall f: X -> Y, forall g: Y -> Z, forall cont: Z -> A,
  (yoneda X Y A f) ((yoneda Y Z A g) cont) = (yoneda X Z A (fun x: X => g (f x))) cont.
Proof.
  intros X Y Z A f0 g0 cont.
  reflexivity.
Qed.

Definition id (X: Type) x: X := x.

Theorem yoneda_is_contravariant_functor2 : forall X A: Type, forall cont: X -> A, forall x: X,
  yoneda X X A (id X) cont x = (id A (yoneda_objpart X A x cont)).
Proof.
  intros X A cont x.
  reflexivity.
Qed.