Nuprl Definition : functor-uncurry
functor-uncurry(C) ==
functor(ob(f) = functor(ob(p) = f (fst(p)) (snd(p));
arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x))) (f (fst(y)) (snd(y)))
(f (fst(x)) (fst(y)) (fst(p)) (snd(x)))
(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 :
mk-functor: mk-functor,
cat-comp: cat-comp(C),
functor-arrow: arrow(F),
functor-ob: ob(F),
mk-nat-trans: x |→ T[x],
apply: f a,
pi1: fst(t),
pi2: snd(t)
FDL editor aliases :
functor-uncurry
Latex:
functor-uncurry(C) ==
functor(ob(f) = functor(ob(p) = f (fst(p)) (snd(p));
arrow(x,y,p) = cat-comp(C) (f (fst(x)) (snd(x))) (f (fst(y)) (snd(x)))
(f (fst(y)) (snd(y)))
(f (fst(x)) (fst(y)) (fst(p)) (snd(x)))
(f (fst(y)) (snd(x)) (snd(y)) (snd(p))));
arrow(f,g,T) = ab |\mrightarrow{} T (fst(ab)) (snd(ab)))
Date html generated:
2020_05_20-AM-07_54_33
Last ObjectModification:
2017_01_13-PM-00_47_31
Theory : small!categories
Home
Index