Nuprl Lemma : equal-I-paths
∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].
p = q ∈ I-path(X;A;a;b;I;alpha)
supposing ((fst(p)) = (fst(q)) ∈ Cname) ∧ ((snd(p)) = (snd(q)) ∈ A(iota(fst(p))(alpha)))
Proof
Definitions occuring in Statement :
I-path: I-path(X;A;a;b;I;alpha),
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,
cons: [a / b],
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
I-path: I-path(X;A;a;b;I;alpha),
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
not: ¬A,
implies: P ⇒ Q,
false: False,
member: t ∈ T,
prop: ℙ,
named-path: named-path(X;A;a;b;I;alpha;z),
subtype_rel: A ⊆r B,
top: Top,
squash: ↓T,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
iota: iota(x)
Lemmas referenced :
l_member_wf,
coordinate_name_wf,
not_wf,
equal-named-paths,
named-path_wf,
equal_wf,
cubical-type-at_wf,
cons_wf,
cube-set-restriction_wf,
iota_wf,
subtype_rel-equal,
pi1_wf_top,
iff_weakening_equal,
I-path_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,
sqequalHypSubstitution,
productElimination,
thin,
sqequalRule,
dependent_pairEquality,
cut,
setElimination,
rename,
lambdaFormation,
hypothesis,
independent_functionElimination,
voidElimination,
introduction,
extract_by_obid,
isectElimination,
hypothesisEquality,
because_Cache,
dependent_set_memberEquality,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
productEquality,
applyEquality,
independent_pairEquality,
isect_memberEquality,
voidEquality,
lambdaEquality,
imageElimination,
imageMemberEquality,
baseClosed,
universeEquality
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)].
p = q supposing ((fst(p)) = (fst(q))) \mwedge{} ((snd(p)) = (snd(q)))
Date html generated:
2017_10_05-PM-03_54_41
Last ObjectModification:
2017_07_28-AM-11_27_44
Theory : cubical!sets
Home
Index