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