Nuprl Definition : functor-uncurry
functor-uncurry(C) ==
functor(ob(f) = functor(ob(p) = ob(ob(f) (fst(p))) (snd(p));
arrow(x,y,p) = cat-comp(C) (ob(ob(f) (fst(x))) (snd(x))) (ob(ob(f) (fst(y))) (snd(x)))
(ob(ob(f) (fst(y))) (snd(y)))
(arrow(f) (fst(x)) (fst(y)) (fst(p)) (snd(x)))
(arrow(ob(f) (fst(y))) (snd(x)) (snd(y)) (snd(p))));
arrow(f,g,T) = ab |→ T (fst(ab)) (snd(ab)))
Definitions occuring in Statement :
mk-nat-trans: x |→ T[x],
functor-arrow: arrow(F),
functor-ob: ob(F),
mk-functor: mk-functor,
cat-comp: cat-comp(C),
pi1: fst(t),
pi2: snd(t),
apply: f a
Definitions occuring in definition :
pi2: snd(t),
pi1: fst(t),
apply: f a,
mk-nat-trans: x |→ T[x],
functor-ob: ob(F),
functor-arrow: arrow(F),
cat-comp: cat-comp(C),
mk-functor: mk-functor
FDL editor aliases :
functor-uncurry
Latex:
functor-uncurry(C) ==
functor(ob(f) = functor(ob(p) = ob(ob(f) (fst(p))) (snd(p));
arrow(x,y,p) = cat-comp(C) (ob(ob(f) (fst(x))) (snd(x)))
(ob(ob(f) (fst(y))) (snd(x)))
(ob(ob(f) (fst(y))) (snd(y)))
(arrow(f) (fst(x)) (fst(y)) (fst(p)) (snd(x)))
(arrow(ob(f) (fst(y))) (snd(x)) (snd(y)) (snd(p))));
arrow(f,g,T) = ab |\mrightarrow{} T (fst(ab)) (snd(ab)))
Date html generated:
2017_01_19-PM-02_54_52
Last ObjectModification:
2017_01_13-PM-00_47_31
Theory : small!categories
Home
Index