Nuprl Lemma : cubical-type-ap-rename-one-equal
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[x,y:Cname]. ∀[a:X([x / I])]. ∀[u,v:A(a)].
u = v ∈ A(a) ⇐⇒ (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a))
supposing (¬(y ∈ I)) ∧ (¬(x ∈ I))
Proof
Definitions occuring in Statement :
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
cubical-type: {X ⊢ _},
cube-set-restriction: f(s),
I-cube: X(I),
cubical-set: CubicalSet,
rename-one-name: rename-one-name(z1;z2),
coordinate_name: Cname,
l_member: (x ∈ l),
cons: [a / b],
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
and: P ∧ Q,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
squash: ↓T,
cand: A c∧ B,
true: True,
prop: ℙ,
rev_implies: P ⇐ Q,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
guard: {T}
Lemmas referenced :
cubical-type-ap-morph_wf,
cons_wf,
coordinate_name_wf,
rename-one-name_wf,
equal_wf,
cubical-type-at_wf,
cube-set-restriction_wf,
not_wf,
l_member_wf,
I-cube_wf,
rename-one-comp,
name-morph_wf,
id-morph_wf,
rename-one-same,
squash_wf,
true_wf,
iff_weakening_equal,
cube-set-restriction-comp,
cube-set-restriction-when-id,
list_wf,
cubical-type_wf,
cubical-set_wf,
cubical-type-ap-morph-id,
cubical-type-ap-morph-comp
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairFormation,
lambdaFormation,
applyEquality,
lambdaEquality,
imageElimination,
extract_by_obid,
isectElimination,
because_Cache,
hypothesis,
hypothesisEquality,
independent_isectElimination,
equalitySymmetry,
natural_numberEquality,
sqequalRule,
imageMemberEquality,
baseClosed,
independent_pairEquality,
dependent_functionElimination,
axiomEquality,
productEquality,
isect_memberEquality,
equalityTransitivity,
universeEquality,
independent_functionElimination,
applyLambdaEquality,
hyp_replacement,
instantiate
Latex:
\mforall{}[X:CubicalSet]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[I:Cname List]. \mforall{}[x,y:Cname]. \mforall{}[a:X([x / I])]. \mforall{}[u,v:A(a)].
u = v \mLeftarrow{}{}\mRightarrow{} (u a rename-one-name(x;y)) = (v a rename-one-name(x;y))
supposing (\mneg{}(y \mmember{} I)) \mwedge{} (\mneg{}(x \mmember{} I))
Date html generated:
2017_10_05-AM-10_12_39
Last ObjectModification:
2017_07_28-AM-11_18_26
Theory : cubical!sets
Home
Index