Nuprl Definition : functor-curry

functor-curry(A;B) ==
functor(ob(F) = functor(ob(a) = functor(ob(b) = F <a, b>;

                                          arrow(x,y,f) = F <a, x> <a, y> <cat-id(A) a, f>);

arrow(x,y,f) = b |→ F <x, b> <y, b> <f, cat-id(B) b>);
arrow(F,G,T) = a |→ b |→ T <a, b>)

Definitions occuring in Statement : mk-nat-trans: x |→ T[x], functor-arrow: arrow(F), functor-ob: ob(F), mk-functor: mk-functor, cat-id: cat-id(C), apply: f a, pair: <a, b>
Definitions occuring in definition : mk-functor: mk-functor, functor-ob: ob(F), functor-arrow: arrow(F), cat-id: cat-id(C), mk-nat-trans: x |→ T[x], apply: f a, pair: <a, b>
FDL editor aliases : functor-curry

Latex:
functor-curry(A;B) == functor(ob(F) = functor(ob(a) = functor(ob(b) = F <a, b> arrow(x,y,f) = F <a, x> <a, y> <cat-id(A) a, f>); arrow(x,y,f) = b |\mrightarrow{} F <x, b> <y, b> <f, cat-id(B) b>); arrow(F,G,T) = a |\mrightarrow{} b |\mrightarrow{} T <a, b>) Date html generated: 2020_05_20-AM-07_54_28 Last ObjectModification: 2017_01_13-PM-00_46_00 Theory : small!categories Home Index