Control.Category.Functor

Definitions

interface CatFunctor : Hom obj -> Hom obj' -> (obj -> obj') -> Type

  A *functor* is a mapping between categories that preserves their
  structure. Generally, `cat` and `cat'` are categories, though
  this is not enforced by the interface.
  
  This is the interface-style definition of a functor. For the
  record-style definition, see `Control.Category.Records.FunctorR`.
  
  Laws (when `cat`, `cat'` are categories):
  * `map id = id`
  * `map f . map g = map (f . g)`

Parameters: cat, cat', f
Constructor: 

MkCatFunctor

Methods:

map : cat a b -> cat' (f a) (f b)

  Apply the functor to a morphism in `cat`, translating it into `cat'`.

Implementations:

CatMonad cat m -> CatFunctor cat cat m

LaxMonFunctor cat ten i cat' ten' i' f -> CatFunctor cat cat' f

StrongFunctor cat ten f -> CatFunctor cat cat f

CostrongFunctor cat ten f -> CatFunctor cat cat f

CatComonad cat w -> CatFunctor cat cat w

map : CatFunctor cat cat' f => cat a b -> cat' (f a) (f b)

  Apply the functor to a morphism in `cat`, translating it into `cat'`.

Totality: total
Visibility: public export

CatEndofunctor : Hom obj -> (obj -> obj) -> Type

  A type synonym for an *endofunctor*, a functor from a category to
  itself.
  
  This is the interface-style definition of an endofunctor. For the
  record-style definition, see `Control.Category.Records.EndofunctorR`.

Totality: total
Visibility: public export

map' : CatEndofunctor cat f => cat a b -> cat (f a) (f b)

  A synonym of `map` that only works for endofunctors. May help
  typechecking and interface resolution.

Totality: total
Visibility: public export

interface CatBifunctor : Hom objA -> Hom objB -> Hom obj' -> (objA -> objB -> obj') -> Type

  A *bifunctor* is a binary functor, i.e. a functor that maps two
  categories to one. Generally, `catA`, `catB` and `cat'` are
  categories, though this is not enforced by the interface.
  
  This is the interface-style definition of a bifunctor. For the
  record-style definition, see `Control.Category.Records.BifunctorR`.
  
  Laws (when `catA`, `catB`, `cat'` are categories):
  * `bimap id id = id`
  * `bimap f f' . bimap g g' = bimap (f . g) (f' . g')`

Parameters: catA, catB, cat', f
Constructor: 

MkCatBifunctor

Methods:

bimap : catA a b -> catB a' b' -> cat' (f a a') (f b b')

  Apply the bifunctor to morphism in `catA` and `catB`, translating
  them into a combined morphism in `cat'`.

Implementations:

CatEndoBifunctor Morphism Pair

CatEndoBifunctor Morphism Either

Applicative m => EndoBinoidal (Kleislimorphism m) Pair

Applicative m => CatEndoBifunctor (Kleislimorphism m) Either

bimap : CatBifunctor catA catB cat' f => catA a b -> catB a' b' -> cat' (f a a') (f b b')

  Apply the bifunctor to morphism in `catA` and `catB`, translating
  them into a combined morphism in `cat'`.

Totality: total
Visibility: public export

Binoidal : Hom objA -> Hom objB -> Hom obj' -> (objA -> objB -> obj') -> Type

  A type synonym that can be used to mark an operator as merely being
  a binoidal functor, rather than a proper bifunctor. These have the
  same data, but weaker laws.
  
  See https://github.com/tokinanpa/cats-and-arrows/tree/main/docs/CategoricalSins.md
  for more information on when/why this matters.
  
  Laws for a binoidal functor:
  * `bimap id id = id`
  * `bimap id f . bimap id g = bimap id (f . g)`
  * `bimap f id . bimap g id = bimap (f . g) id`
  * `bimap f g = bimap id g . bimap f id` (NOTE: order matters here)

Totality: total
Visibility: public export

mapl : CatBifunctor catA catB cat' f => Category catB => catA a b -> cat' (f a c) (f b c)

  Apply a morphism to a bifunctor only on the left.

Totality: total
Visibility: public export

mapr : CatBifunctor catA catB cat' f => Category catA => catB a b -> cat' (f c a) (f c b)

  Apply a morphism to a bifunctor only on the right.

Totality: total
Visibility: public export

CatEndoBifunctor : Hom obj -> (obj -> obj -> obj) -> Type

  A type synonym for an *endo-bifunctor*, a bifunctor from a category
  to itself.
  
  This is the interface-style definition of an endo-bifunctor. For the
  record-style definition, see `Control.Category.Records.EndoBifunctorR`.

Totality: total
Visibility: public export

EndoBinoidal : Hom obj -> (obj -> obj -> obj) -> Type

  See `Binoidal`.

Totality: total
Visibility: public export

bimap' : CatEndoBifunctor cat f => cat a b -> cat a' b' -> cat (f a a') (f b b')

  A synonym of `bimap` that only works for endo-bifunctors. May help
  typechecking and interface resolution.

Totality: total
Visibility: public export

mapl' : CatEndoBifunctor cat f => Category cat => cat a b -> cat (f a c) (f b c)

  A synonym of `mapl` that only works for endo-bifunctors. May help
  typechecking and interface resolution.

Totality: total
Visibility: public export

mapr' : CatEndoBifunctor cat f => Category cat => cat a b -> cat (f c a) (f c b)

  A synonym of `mapr` that only works for endo-bifunctors. May help
  typechecking and interface resolution.

Totality: total
Visibility: public export

CatBifunctorMorPair : CatEndoBifunctor Morphism Pair

Totality: total
Visibility: public export

CatBifunctorMorEither : CatEndoBifunctor Morphism Either

Totality: total
Visibility: public export

CatBifunctorKleisliPair : Applicative m => EndoBinoidal (Kleislimorphism m) Pair

  WARNING: This is a binoidal functor, not a true bifunctor.

Totality: total
Visibility: public export

CatBifunctorKleisliEither : Applicative m => CatEndoBifunctor (Kleislimorphism m) Either

Totality: total
Visibility: public export