### Nuprl Lemma : named-path-equal-implies

`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname].`
`  ∀[p,q:named-path(X;A;a;b;I;alpha;z)].  p = q ∈ A(iota(z)(alpha)) supposing p = q ∈ named-path(X;A;a;b;I;alpha;z) `
`  supposing ¬(z ∈ I)`

Proof

Definitions occuring in Statement :  named-path: `named-path(X;A;a;b;I;alpha;z)` cubical-term: `{X ⊢ _:AF}` cubical-type-at: `A(a)` cubical-type: `{X ⊢ _}` cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` iota: `iota(x)` coordinate_name: `Cname` l_member: `(x ∈ l)` cons: `[a / b]` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` guard: `{T}` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  named-path-subtype equal_functionality_wrt_subtype_rel2 named-path_wf cubical-type-at_wf cons_wf coordinate_name_wf cube-set-restriction_wf iota_wf equal_wf not_wf l_member_wf I-cube_wf list_wf cubical-term_wf cubical-type_wf cubical-set_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality introduction independent_isectElimination independent_functionElimination sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[alpha:X(I)].  \mforall{}[z:Cname].
\mforall{}[p,q:named-path(X;A;a;b;I;alpha;z)].    p  =  q  supposing  p  =  q  supposing  \mneg{}(z  \mmember{}  I)

Date html generated: 2016_06_16-PM-07_27_56
Last ObjectModification: 2015_12_28-PM-04_14_09

Theory : cubical!sets

Home Index