Library CT.Instance.Functor.Endofunctor

Require Import CT.Category.
Require Import CT.Functor.

F : A → A. An endofunctor maps a category to itself.

Program Definition Endofunctor (C : Category) := Functor C C.