Control.Category.NatTrans

Definitions

0 NatTrans : Hom obj' -> (obj -> obj') -> (obj -> obj') -> Type

  A *natural transformation* is a kind of mapping between functors
  that's compatible with their behavior.
  
  This is the interface-style definition of a natural transformation.
  For the record-style definition, see `Control.Category.Records.NatTransR`.
  
  Laws (for natural transformation `tr`):
  * `map f . tr = tr . map f`

Totality: total
Visibility: public export