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