
  0 | module Control.Category.Records.NatTrans
  1 | 
  2 | import Control.Category
  3 | import Control.Category.Records.Category
  4 | import Control.Category.Records.Functor
  5 | 
  6 | %default total
  7 | %prefix_record_projections off
  8 | 
  9 | ||| A *natural transformation* is a kind of mapping between functors
 10 | ||| that's compatible with their behavior.
 11 | |||
 12 | ||| See `NatTrans` for required laws.
 13 | public export
 14 | record NatTransR (f,g : FunctorR cat cat') where
 15 |   constructor MkNatTransR
 16 |   fun : NatTrans cat'.hom f.fun g.fun
 17 | 
 18 | namespace NatTransR
 19 |   ||| The identity natural transformation.
 20 |   public export
 21 |   id : {cat' : _} -> {f : FunctorR cat cat'} ->
 22 |        NatTransR {cat'} f f
 23 |   id = MkNatTransR cat'.id
 24 | 
 25 |   ||| Binary right-to-left composition of natural transformations.
 26 |   public export
 27 |   (.) : {cat' : _} -> {f,g,h : FunctorR cat cat'} ->
 28 |         NatTransR g h -> NatTransR f g -> NatTransR f h
 29 |   MkNatTransR tr . MkNatTransR tr' = MkNatTransR (cat'.comp tr tr')
 30 |