### Nuprl Lemma : A-face-name-image

`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I). ∀K,f:Top. ∀face:A-face(X;A;I;alpha).`
`  (A-face-name(A-face-image(X;A;I;K;f;alpha;face)) ~ (λp.<f (fst(p)), snd(p)>) A-face-name(face))`

Proof

Definitions occuring in Statement :  A-face-image: `A-face-image(X;A;I;K;f;alpha;face)` A-face-name: `A-face-name(f)` A-face: `A-face(X;A;I;alpha)` cubical-type: `{X ⊢ _}` I-cube: `X(I)` cubical-set: `CubicalSet` coordinate_name: `Cname` list: `T List` top: `Top` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` apply: `f a` lambda: `λx.A[x]` pair: `<a, b>` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` A-face: `A-face(X;A;I;alpha)` A-face-name: `A-face-name(f)` A-face-image: `A-face-image(X;A;I;K;f;alpha;face)` spreadn: spread3 pi1: `fst(t)` pi2: `snd(t)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  A-face_wf top_wf I-cube_wf list_wf coordinate_name_wf cubical-type_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin sqequalRule cut lemma_by_obid isectElimination hypothesisEquality hypothesis because_Cache

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).  \mforall{}K,f:Top.  \mforall{}face:A-face(X;A;I;alpha).
(A-face-name(A-face-image(X;A;I;K;f;alpha;face))  \msim{}  (\mlambda{}p.<f  (fst(p)),  snd(p)>)  A-face-name(face))

Date html generated: 2016_06_16-PM-05_54_01
Last ObjectModification: 2015_12_28-PM-04_29_16

Theory : cubical!sets

Home Index