Nuprl Definition : comma-cat
(S ↓ T) ==
Cat(ob = a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (ob(S) a) (ob(T) b));
arrow(x,y) = let a,b,f = x in
let a',b',f' = y in
{gh:cat-arrow(A) a a' × (cat-arrow(B) b b')|
(cat-comp(C) (ob(S) a) (ob(T) b) (ob(T) b') f (arrow(T) b b' (snd(gh))))
= (cat-comp(C) (ob(S) a) (ob(S) a') (ob(T) b') (arrow(S) a a' (fst(gh))) f')
∈ (cat-arrow(C) (ob(S) a) (ob(T) b'))} ;
id(x) = let a,b,f = x in
<cat-id(A) a, cat-id(B) b>;
comp(u,v,w,fp,gp) = let a,b,x = u in
let a',b',x' = v in
let a'',b'',x'' = w in
let f,g = fp
in let f',g' = gp
in <cat-comp(A) a a' a'' f f', cat-comp(B) b b' b'' g g'>)
Definitions occuring in Statement :
functor-arrow: arrow(F),
functor-ob: ob(F),
mk-cat: mk-cat,
cat-comp: cat-comp(C),
cat-id: cat-id(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
spreadn: spread3,
pi1: fst(t),
pi2: snd(t),
set: {x:A| B[x]} ,
apply: f a,
spread: spread def,
pair: <a, b>,
product: x:A × B[x],
equal: s = t ∈ T
Definitions occuring in definition :
cat-comp: cat-comp(C),
apply: f a,
pair: <a, b>,
spread: spread def,
spreadn: spread3,
cat-id: cat-id(C),
pi1: fst(t),
functor-arrow: arrow(F),
functor-ob: ob(F),
pi2: snd(t),
cat-arrow: cat-arrow(C),
equal: s = t ∈ T,
product: x:A × B[x],
set: {x:A| B[x]} ,
cat-ob: cat-ob(C),
mk-cat: mk-cat
FDL editor aliases :
comma-cat
Latex:
(S \mdownarrow{} T) ==
Cat(ob = a:cat-ob(A) \mtimes{} b:cat-ob(B) \mtimes{} (cat-arrow(C) (ob(S) a) (ob(T) b));
arrow(x,y) = let a,b,f = x in
let a',b',f' = y in
\{gh:cat-arrow(A) a a' \mtimes{} (cat-arrow(B) b b')|
(cat-comp(C) (ob(S) a) (ob(T) b) (ob(T) b') f (arrow(T) b b' (snd(gh))))
= (cat-comp(C) (ob(S) a) (ob(S) a') (ob(T) b') (arrow(S) a a' (fst(gh))) f')\} ;
id(x) = let a,b,f = x in
<cat-id(A) a, cat-id(B) b>
comp(u,v,w,fp,gp) = let a,b,x = u in
let a',b',x' = v in
let a'',b'',x'' = w in
let f,g = fp
in let f',g' = gp
in <cat-comp(A) a a' a'' f f', cat-comp(B) b b' b'' g g'>)
Date html generated:
2017_01_19-PM-02_56_11
Last ObjectModification:
2017_01_13-PM-02_42_05
Theory : small!categories
Home
Index