Portability | non-portable (either class-associated types or MPTCs with fundeps) |
---|---|

Stability | experimental |

Maintainer | Edward Kmett <ekmett@gmail.com> |

This module declares the `HasTerminalObject`

and `HasInitialObject`

classes.
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.

- class Category k => HasTerminalObject k t | k -> t where
- terminate :: k a t

- class Category k => HasInitialObject k i | k -> i where
- initiate :: k i a

# Documentation

class Category k => HasTerminalObject k t | k -> t whereSource

The `Category k`

has a terminal object `Terminal k`

such that for all objects `a`

in `k`

,
there exists a unique morphism from `a`

to `Terminal k`

.

class Category k => HasInitialObject k i | k -> i whereSource

The `Category k`

has an initial (coterminal) object `Initial k`

such that for all objects
`a`

in `k`

, there exists a unique morphism from `Initial k `

to `a`

.