Nuprl Definition : name-morph-inv
name-morph-inv(I;f) == λx.hd(filter(λi.(isname(f i) ∧b (f i =z x));I))
Definitions occuring in Statement :
isname: isname(z),
hd: hd(l),
filter: filter(P;l),
band: p ∧b q,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
hd: hd(l),
filter: filter(P;l),
lambda: λx.A[x],
band: p ∧b q,
isname: isname(z),
eq_int: (i =z j),
apply: f a
FDL editor aliases :
name-morph-inv
Latex:
name-morph-inv(I;f) == \mlambda{}x.hd(filter(\mlambda{}i.(isname(f i) \mwedge{}\msubb{} (f i =\msubz{} x));I))
Date html generated:
2016_05_20-AM-09_30_39
Last ObjectModification:
2015_09_23-AM-09_29_32
Theory : cubical!sets
Home
Index