Nuprl Definition : comma-cat
(S ↓ T) ==
Cat(ob = a:cat-ob(A) × b:cat-ob(B) × (cat-arrow(C) (S a) (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) (S a) (T b) (T b') f (T b b' (snd(gh))))
= (cat-comp(C) (S a) (S a') (T b') (S a a' (fst(gh))) f')
∈ (cat-arrow(C) (S a) (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 :
mk-cat: mk-cat,
cat-ob: cat-ob(C),
set: {x:A| B[x]} ,
product: x:A × B[x],
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
pi2: snd(t),
functor-ob: ob(F),
functor-arrow: arrow(F),
pi1: fst(t),
cat-id: cat-id(C),
spreadn: spread3,
spread: spread def,
pair: <a, b>,
apply: f a,
cat-comp: cat-comp(C)
FDL editor aliases :
comma-cat
Latex:
(S \mdownarrow{} T) ==
Cat(ob = a:cat-ob(A) \mtimes{} b:cat-ob(B) \mtimes{} (cat-arrow(C) (S a) (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) (S a) (T b) (T b') f (T b b' (snd(gh))))
= (cat-comp(C) (S a) (S a') (T b') (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:
2020_05_20-AM-07_56_24
Last ObjectModification:
2017_01_13-PM-02_42_05
Theory : small!categories
Home
Index