Nuprl Definition : functor-curry
functor-curry(A;B) ==
functor(ob(F) = functor(ob(a) = functor(ob(b) = ob(F) <a, b>;
arrow(x,y,f) = arrow(F) <a, x> <a, y> <cat-id(A) a, f>);
arrow(x,y,f) = b |→ arrow(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 :
pair: <a, b>,
apply: f a,
mk-nat-trans: x |→ T[x],
cat-id: cat-id(C),
functor-arrow: arrow(F),
functor-ob: ob(F),
mk-functor: mk-functor
FDL editor aliases :
functor-curry
Latex:
functor-curry(A;B) ==
functor(ob(F) = functor(ob(a) = functor(ob(b) = ob(F) <a, b>
arrow(x,y,f) = arrow(F) <a, x> <a, y> <cat-id(A) a, f>);
arrow(x,y,f) = b |\mrightarrow{} arrow(F) <x, b> <y, b> <f, cat-id(B) b>);
arrow(F,G,T) = a |\mrightarrow{} b |\mrightarrow{} T <a, b>)
Date html generated:
2017_01_19-PM-02_54_24
Last ObjectModification:
2017_01_13-PM-00_46_00
Theory : small!categories
Home
Index