Hom : Type -> Type A type synonym for `obj -> obj -> Type` to simplify definitions.
Totality: total
Visibility: public export(~~>) : Type -> Type -> Type A type synonym for (non-dependent) functions.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 0interface Category : Hom obj -> Type A *category* is a generalized function type with a notion of
composition and of identity. The elements of this type are
typically called *morphisms*.
This is the interface-style definition of a category. For the
record-style definition, see `Control.Category.Records.CategoryR`.
Laws:
* `id . f = f`
* `f . id = f`
* `(f . g) . h = f . (g . h)`
Parameters: cat
Constructor: MkCategory
Methods:
id : cat a a The identity morphism of an object `a`.
(.) : cat b c -> cat a b -> cat a c Binary right-to-left composition of morphisms.
Fixity Declaration: infixr operator, level 9
Implementations:
Category MorphismMonad m => Category (Kleislimorphism m)Monad m => Category (Star m)
id : Category cat => cat a a The identity morphism of an object `a`.
Totality: total
Visibility: public export(.) : Category cat => cat b c -> cat a b -> cat a c Binary right-to-left composition of morphisms.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9(<<<) : Category cat => cat b c -> cat a b -> cat a c A synonym for right-to-left category composition that may be easier
to read. The arrow shows the direction the morphisms are composed.
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5(>>>) : Category cat => cat a b -> cat b c -> cat a c A synonym for left-to-right category composition that may be easier
to read. The arrow shows the direction the morphisms are composed.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 5compose : Category cat => TransClosure cat a b -> cat a b Compose a list of morphisms left-to-right.
Totality: total
Visibility: public export