Nuprl Lemma : set-path-name_wf
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I).
∀[x:{x:Cname| ¬(x ∈ I)} ]
∀p:(Id_A a b)(alpha)
(set-path-name(X;A;I;alpha;x;p) ∈ {q:I-path(X;A;a;b;I;alpha)|
((fst(q)) = x ∈ Cname) ∧ (q = p ∈ (Id_A a b)(alpha))} )
Proof
Definitions occuring in Statement :
set-path-name: set-path-name(X;A;I;alpha;x;p),
cubical-identity: (Id_A a b),
I-path: I-path(X;A;a;b;I;alpha),
cubical-term: {X ⊢ _:AF},
cubical-type-at: A(a),
cubical-type: {X ⊢ _},
I-cube: X(I),
cubical-set: CubicalSet,
coordinate_name: Cname,
l_member: (x ∈ l),
list: T List,
uall: ∀[x:A]. B[x],
pi1: fst(t),
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
false: False,
not: ¬A,
named-path: named-path(X;A;a;b;I;alpha;z),
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
guard: {T},
subtype_rel: A ⊆r B,
true: True,
prop: ℙ,
squash: ↓T,
uimplies: b supposing a,
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
cubical-path: cubical-path(X;A;a;b;I;alpha),
member: t ∈ T,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
pi1: fst(t),
cubical-type-at: A(a),
cubical-identity: (Id_A a b),
set-path-name: set-path-name(X;A;I;alpha;x;p),
path-eq: path-eq(X;A;I;alpha;p;q),
I-path: I-path(X;A;a;b;I;alpha),
quotient: x,y:A//B[x; y],
cand: A c∧ B,
named-path-morph: named-path-morph(X;A;I;K;z;x;f;alpha;w)
Lemmas referenced :
cubical-set_wf,
cubical-type_wf,
cubical-term_wf,
list_wf,
not_wf,
set_wf,
cubical-identity_wf,
iota_wf,
cube-set-restriction_wf,
cons_wf,
cubical-type-at_wf,
subtype_rel_wf,
coordinate_name_wf,
l_member_wf,
named-path_wf,
iff_weakening_equal,
cube-set-restriction-id,
I-cube_wf,
true_wf,
squash_wf,
equal_wf,
path-eq-equiv,
path-eq_wf,
I-path_wf,
subtype_quotient,
equal-wf-base,
name-comp-id-left,
extend-name-morph-iota,
name-morph_wf,
extend-name-morph_wf,
cube-set-restriction-comp,
subtype_rel-equal,
id-morph_wf,
named-path-morph_wf,
equal-named-paths,
ext-eq_weakening,
subtype_rel_weakening,
cubical-type-ap-morph_wf,
cubical-type-ap-morph-comp,
rename-one-name_wf,
istype-universe,
subtype_rel_self,
rename-one-extend-name-morph,
rename-one-iota,
rename-one-extend-id,
quotient-member-eq,
cubical-path_wf
Rules used in proof :
axiomEquality,
dependent_functionElimination,
applyLambdaEquality,
hyp_replacement,
voidElimination,
rename,
setElimination,
independent_functionElimination,
productElimination,
baseClosed,
imageMemberEquality,
natural_numberEquality,
because_Cache,
universeEquality,
equalitySymmetry,
equalityTransitivity,
imageElimination,
applyEquality,
promote_hyp,
independent_isectElimination,
lambdaEquality,
sqequalRule,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
dependent_set_memberEquality,
productEquality,
dependent_pairEquality,
pertypeElimination,
pointwiseFunctionalityForEquality,
independent_pairFormation,
instantiate,
lambdaFormation_alt,
universeIsType,
lambdaEquality_alt,
inhabitedIsType,
levelHypothesis,
equalityUniverse,
addLevel
Latex:
\mforall{}X:CubicalSet. \mforall{}A:\{X \mvdash{} \_\}. \mforall{}a,b:\{X \mvdash{} \_:A\}. \mforall{}I:Cname List. \mforall{}alpha:X(I).
\mforall{}[x:\{x:Cname| \mneg{}(x \mmember{} I)\} ]
\mforall{}p:(Id\_A a b)(alpha)
(set-path-name(X;A;I;alpha;x;p) \mmember{} \{q:I-path(X;A;a;b;I;alpha)| ((fst(q)) = x) \mwedge{} (q = p)\} )
Date html generated:
2020_05_21-AM-11_06_43
Last ObjectModification:
2020_01_15-PM-01_18_51
Theory : cubical!sets
Home
Index