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 both special cases of the idea of a (co)limit.

- class Category ~> => HasTerminalObject (~>) where
- class Category ~> => HasInitialObject (~>) where

# Documentation

class Category ~> => HasTerminalObject (~>) whereSource

The `Category (~>)`

has a terminal object `Terminal (~>)`

such that for all objects `a`

in `(~>)`

,
there exists a unique morphism from `a`

to `Terminal (~>)`

.