### Nuprl Lemma : equal-named-paths

`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname].`
`  ∀[p:named-path(X;A;a;b;I;alpha;z)]. ∀[q:A(iota(z)(alpha))].`
`    p = q ∈ named-path(X;A;a;b;I;alpha;z) supposing p = q ∈ A(iota(z)(alpha)) `
`  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` named-path: `named-path(X;A;a;b;I;alpha;z)` prop: `ℙ`
Lemmas referenced :  name-path-endpoints_wf equal_wf cubical-type-at_wf cons_wf coordinate_name_wf cube-set-restriction_wf iota_wf named-path_wf not_wf l_member_wf I-cube_wf list_wf cubical-term_wf cubical-type_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality hypothesis lemma_by_obid isectElimination hypothesisEquality independent_isectElimination 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:named-path(X;A;a;b;I;alpha;z)].  \mforall{}[q:A(iota(z)(alpha))].    p  =  q  supposing  p  =  q
supposing  \mneg{}(z  \mmember{}  I)

Date html generated: 2016_06_16-PM-07_28_02
Last ObjectModification: 2015_12_28-PM-04_14_29

Theory : cubical!sets

Home Index