### Nuprl Lemma : face-name-image

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

Proof

Definitions occuring in Statement :  face-image: `face-image(X;I;K;f;face)` face-name: `face-name(f)` I-face: `I-face(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]` I-face: `I-face(X;I)` face-name: `face-name(f)` face-image: `face-image(X;I;K;f;face)` spreadn: spread3 pi1: `fst(t)` pi2: `snd(t)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  I-face_wf top_wf list_wf coordinate_name_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{}I:Cname  List.  \mforall{}K,f:Top.  \mforall{}face:I-face(X;I).
(face-name(face-image(X;I;K;f;face))  \msim{}  (\mlambda{}p.<f  (fst(p)),  snd(p)>)  face-name(face))

Date html generated: 2016_06_16-PM-05_53_56
Last ObjectModification: 2015_12_28-PM-04_29_31

Theory : cubical!sets

Home Index