|Portability||non-portable (either class-associated types or MPTCs with fundeps)|
|Maintainer||Edward Kmett <email@example.com>|
This module declares the
These are defined in terms of class-associated types rather than functional dependencies
because most of the time when you are manipulating a category you don't care about them;
this gets them out of the signature of most functions that use the category.
Both of these are special cases of the idea of a (co)limit.
Category k has a terminal object
Terminal k such that for all objects
there exists a unique morphism from