record NatTransR : FunctorR cat cat' -> FunctorR cat cat' -> Type A *natural transformation* is a kind of mapping between functors
that's compatible with their behavior.
See `NatTrans` for required laws.
Totality: total
Visibility: public export
Constructor: MkNatTransR : NatTrans (cat' .hom) (f .fun) (g .fun) -> NatTransR f g
Projection: .fun : NatTransR f g -> NatTrans (cat' .hom) (f .fun) (g .fun)
.fun : NatTransR f g -> NatTrans (cat' .hom) (f .fun) (g .fun)- Totality: total
Visibility: public export id : NatTransR f f The identity natural transformation.
Totality: total
Visibility: public export(.) : NatTransR g h -> NatTransR f g -> NatTransR f h Binary right-to-left composition of natural transformations.
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9