Nuprl Definition : functor-comp

functor-comp(F;G) ==  functor(ob(x) = ob(G) (ob(F) x);arrow(x,y,a) = arrow(G) (ob(F) x) (ob(F) y) (arrow(F) x y a))


Definitions occuring in Statement :  functor-arrow: arrow(F),  functor-ob: ob(F),  mk-functor: mk-functor,  apply: f a
Definitions occuring in definition :  functor-arrow: arrow(F),  apply: f a,  functor-ob: ob(F),  mk-functor: mk-functor
FDL editor aliases :  functor-comp
Latex:
functor-comp(F;G)  ==
    functor(ob(x)  =  ob(G)  (ob(F)  x);
                    arrow(x,y,a)  =  arrow(G)  (ob(F)  x)  (ob(F)  y)  (arrow(F)  x  y  a))


Date html generated: 2017_01_19-PM-02_53_25
Last ObjectModification: 2017_01_13-PM-01_13_36

Theory : small!categories


Home Index