Nuprl Definition : A-face
A-face(X;A;I;alpha) == x:nameset(I) × i:ℕ2 × A((x:=i)(alpha))
Definitions occuring in Statement :
cubical-type-at: A(a),
cube-set-restriction: f(s),
face-map: (x:=i),
nameset: nameset(L),
cname_deq: CnameDeq,
list-diff: as-bs,
cons: [a / b],
nil: [],
int_seg: {i..j-},
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
nameset: nameset(L),
product: x:A × B[x],
int_seg: {i..j-},
natural_number: $n,
cubical-type-at: A(a),
cube-set-restriction: f(s),
list-diff: as-bs,
cname_deq: CnameDeq,
cons: [a / b],
nil: [],
face-map: (x:=i)
FDL editor aliases :
A-face
Latex:
A-face(X;A;I;alpha) == x:nameset(I) \mtimes{} i:\mBbbN{}2 \mtimes{} A((x:=i)(alpha))
Date html generated:
2016_06_16-PM-05_49_01
Last ObjectModification:
2015_09_23-AM-09_31_09
Theory : cubical!sets
Home
Index