0 | module Control.Category.NatTrans
 1 |
 2 | import Control.Category.Core
 3 |
 4 | %default total
 5 |
 6 | ------------------------------------------------------------
 7 | -- Interface
 8 | ------------------------------------------------------------
 9 |
10 | ||| A *natural transformation* is a kind of mapping between functors
11 | ||| that's compatible with their behavior.
12 | |||
13 | ||| This is the interface-style definition of a natural transformation.
14 | ||| For the record-style definition, see `Control.Category.Records.NatTransR`.
15 | |||
16 | ||| Laws (for natural transformation `tr`):
17 | ||| * `map f . tr = tr . map f`
18 | public export
19 | 0 NatTrans : {obj : _} -> (cat : Hom obj') -> (f,g : obj -> obj') -> Type
20 | NatTrans cat f g = {a : _} -> cat (f a) (g a)
21 |