Nuprl Definition : Kan-groupoid-nerve
Kan-groupoid-nerve(G) == <cubical-nerve(cat(G)), λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)>
Definitions occuring in Statement :
groupoid-nerve-filler: groupoid-nerve-filler(G;I;J;x;i;box),
cubical-nerve: cubical-nerve(X),
groupoid-cat: cat(G),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
cubical-nerve: cubical-nerve(X),
groupoid-cat: cat(G),
lambda: λx.A[x],
groupoid-nerve-filler: groupoid-nerve-filler(G;I;J;x;i;box)
FDL editor aliases :
Kan-groupoid-nerve
Latex:
Kan-groupoid-nerve(G) == <cubical-nerve(cat(G)), \mlambda{}I,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)\000C>
Date html generated:
2016_06_16-PM-07_27_09
Last ObjectModification:
2015_09_23-AM-09_33_55
Theory : cubical!sets
Home
Index