Nuprl Definition : poset-cat-dist
poset-cat-dist(I;x;y) == ||filter(λi.((x i =z 0) ∧b (y i =z 1));I)||
Definitions occuring in Statement :
length: ||as||,
filter: filter(P;l),
band: p ∧b q,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
length: ||as||,
filter: filter(P;l),
lambda: λx.A[x],
band: p ∧b q,
eq_int: (i =z j),
apply: f a,
natural_number: $n
FDL editor aliases :
poset-cat-dist
Latex:
poset-cat-dist(I;x;y) == ||filter(\mlambda{}i.((x i =\msubz{} 0) \mwedge{}\msubb{} (y i =\msubz{} 1));I)||
Date html generated:
2016_06_16-PM-06_53_34
Last ObjectModification:
2015_09_23-AM-09_32_56
Theory : cubical!sets
Home
Index