### 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: 2019_10_31-AM-07_24_48
Last ObjectModification: 2019_05_07-PM-06_01_20

Theory : small!categories

Home Index