Category of categories #
This file contains the definition of the category
Cat of all categories.
In this category objects are categories and
morphisms are functors between these categories.
Implementation notes #
Cat is not a concrete category, we use
bundled to define
its carrier type.
Functor that gets the set of objects of a category. It is not
forget, because it is not a faithful functor.
- One or more equations did not get rendered due to their size.