### 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