Nuprl Definition : is-A-face

is-A-face(X;A;I;alpha;bx;f) == let y,b,w = f in (bx alpha (y:=b)) = w ∈ A((y:=b)(alpha))

Definitions occuring in Statement : cubical-type-ap-morph: (u a f), cubical-type-at: A(a), cube-set-restriction: f(s), face-map: (x:=i), cname_deq: CnameDeq, list-diff: as-bs, cons: [a / b], nil: [], spreadn: spread3, equal: s = t ∈ T
Definitions occuring in definition : spreadn: spread3, equal: s = t ∈ T, cubical-type-at: A(a), cube-set-restriction: f(s), cubical-type-ap-morph: (u a f), list-diff: as-bs, cname_deq: CnameDeq, cons: [a / b], nil: [], face-map: (x:=i)
FDL editor aliases : is-A-face

Latex:
is-A-face(X;A;I;alpha;bx;f) == let y,b,w = f in (bx alpha (y:=b)) = w Date html generated: 2016_06_16-PM-05_50_46 Last ObjectModification: 2015_09_23-AM-09_31_29 Theory : cubical!sets Home Index