Nuprl Definition : face-maps-comp
face-maps-comp(L) == reduce(λp,f. (let x,i = p in (x:=i) o f);λt.t;L)
Definitions occuring in Statement :
name-comp: (f o g),
face-map: (x:=i),
reduce: reduce(f;k;as),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
reduce: reduce(f;k;as),
name-comp: (f o g),
spread: spread def,
face-map: (x:=i),
lambda: λx.A[x]
FDL editor aliases :
face-maps-comp
Latex:
face-maps-comp(L) == reduce(\mlambda{}p,f. (let x,i = p in (x:=i) o f);\mlambda{}t.t;L)
Date html generated:
2016_05_20-AM-09_35_16
Last ObjectModification:
2015_09_23-AM-09_29_43
Theory : cubical!sets
Home
Index