Nuprl Lemma : cubical-path-same-name
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].
(((fst(p)) = (fst(q)) ∈ Cname) ⇒ (p = q ∈ cubical-path(X;A;a;b;I;alpha)) ⇒ (p = q ∈ I-path(X;A;a;b;I;alpha)))
Proof
Definitions occuring in Statement :
cubical-path: cubical-path(X;A;a;b;I;alpha),
I-path: I-path(X;A;a;b;I;alpha),
cubical-term: {X ⊢ _:AF},
cubical-type: {X ⊢ _},
I-cube: X(I),
cubical-set: CubicalSet,
coordinate_name: Cname,
list: T List,
uall: ∀[x:A]. B[x],
pi1: fst(t),
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
subtype_rel: A ⊆r B,
cubical-path: cubical-path(X;A;a;b;I;alpha),
uall: ∀[x:A]. B[x],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
uimplies: b supposing a,
implies: P ⇒ Q,
prop: ℙ,
I-path: I-path(X;A;a;b;I;alpha),
top: Top,
quotient: x,y:A//B[x; y],
and: P ∧ Q,
cand: A c∧ B,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q
Lemmas referenced :
subtype_quotient,
path-eq_wf,
I-path_wf,
path-eq-equiv,
equal_wf,
cubical-path_wf,
coordinate_name_wf,
pi1_wf_top,
I-cube_wf,
list_wf,
cubical-term_wf,
cubical-type_wf,
cubical-set_wf,
member_wf,
path-eq-same-name
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
hypothesisEquality,
applyEquality,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
because_Cache,
lambdaEquality,
hypothesis,
independent_isectElimination,
isect_memberFormation,
lambdaFormation,
productElimination,
independent_pairEquality,
setElimination,
rename,
isect_memberEquality,
voidElimination,
voidEquality,
dependent_functionElimination,
axiomEquality,
pertypeElimination,
productEquality,
independent_functionElimination
Latex:
\mforall{}[X:CubicalSet]. \mforall{}[A:\{X \mvdash{} \_\}]. \mforall{}[a,b:\{X \mvdash{} \_:A\}]. \mforall{}[I:Cname List]. \mforall{}[alpha:X(I)].
\mforall{}[p,q:I-path(X;A;a;b;I;alpha)].
(((fst(p)) = (fst(q))) {}\mRightarrow{} (p = q) {}\mRightarrow{} (p = q))
Date html generated:
2017_10_05-PM-03_55_16
Last ObjectModification:
2017_07_28-AM-11_28_15
Theory : cubical!sets
Home
Index