Nuprl Definition : groupoid-map
groupoid-map(G;H) ==
{F:Functor(cat(G);cat(H))|
∀x,y:cat-ob(cat(G)). ∀f:cat-arrow(cat(G)) x y.
((F y x groupoid-inv(G;x;y;f)) = groupoid-inv(H;F x;F y;F x y f) ∈ (cat-arrow(cat(H)) (F y) (F x)))}
Definitions occuring in Statement :
groupoid-inv: groupoid-inv(G;x;y;x_y),
groupoid-cat: cat(G),
functor-arrow: arrow(F),
functor-ob: ob(F),
cat-functor: Functor(C1;C2),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
cat-functor: Functor(C1;C2),
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
groupoid-cat: cat(G),
groupoid-inv: groupoid-inv(G;x;y;x_y),
functor-ob: ob(F),
apply: f a,
functor-arrow: arrow(F)
FDL editor aliases :
groupoid-map
Latex:
groupoid-map(G;H) ==
\{F:Functor(cat(G);cat(H))|
\mforall{}x,y:cat-ob(cat(G)). \mforall{}f:cat-arrow(cat(G)) x y.
((F y x groupoid-inv(G;x;y;f)) = groupoid-inv(H;F x;F y;F x y f))\}
Date html generated:
2020_05_20-AM-07_55_24
Last ObjectModification:
2019_05_07-PM-06_01_20
Theory : small!categories
Home
Index