Nuprl Lemma : csm-I-path
∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:Delta(I).
(I-path(Delta;(A)s;(a)s;(b)s;I;alpha) = I-path(X;A;a;b;I;(s)alpha) ∈ Type)
Proof
Definitions occuring in Statement :
I-path: I-path(X;A;a;b;I;alpha),
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:AF},
csm-ap-type: (AF)s,
cubical-type: {X ⊢ _},
csm-ap: (s)x,
I-cube: X(I),
cube-set-map: A ⟶ B,
cubical-set: CubicalSet,
coordinate_name: Cname,
list: T List,
all: ∀x:A. B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
so_apply: x[s],
prop: ℙ,
so_lambda: λ2x.t[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
I-path: I-path(X;A;a;b;I;alpha),
all: ∀x:A. B[x],
csm-ap-type: (AF)s,
cubical-type: {X ⊢ _},
pi1: fst(t),
cubical-type-at: A(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},
uimplies: b supposing a,
subtype_rel: A ⊆r B,
true: True,
squash: ↓T,
name-path-endpoints: name-path-endpoints(X;A;a;b;I;alpha;z;omega),
csm-ap-term: (t)s,
cubical-term: {X ⊢ _:AF},
int_seg: {i..j-},
coordinate_name: Cname,
int_upper: {i...},
lelt: i ≤ j < k,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False
Lemmas referenced :
cubical-set_wf,
cube-set-map_wf,
cubical-term_wf,
list_wf,
I-cube_wf,
l_member_wf,
not_wf,
coordinate_name_wf,
set_wf,
csm-ap-type_wf,
iff_weakening_equal,
csm-ap-restriction,
iota_wf,
cube-set-restriction_wf,
csm-ap_wf,
true_wf,
squash_wf,
equal_wf,
cons_wf,
csm-cubical-type-ap-morph,
cubical-type-at_wf,
subtype_rel_self,
istype-universe,
cube-set-restriction-comp,
face-map_wf,
decidable__le,
full-omega-unsat,
intformnot_wf,
intformle_wf,
itermConstant_wf,
istype-int,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_formula_prop_wf,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
istype-le,
istype-less_than,
iota-identity,
cube-set-restriction-id,
cubical-type-ap-morph_wf,
subtype_rel-equal
Rules used in proof :
because_Cache,
hypothesisEquality,
lambdaEquality,
sqequalRule,
hypothesis,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
productEquality,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
productElimination,
rename,
setElimination,
setEquality,
independent_functionElimination,
independent_isectElimination,
baseClosed,
imageMemberEquality,
natural_numberEquality,
dependent_functionElimination,
universeEquality,
equalitySymmetry,
equalityTransitivity,
imageElimination,
functionExtensionality,
applyEquality,
Error :memTop,
lambdaEquality_alt,
universeIsType,
instantiate,
independent_pairFormation,
inhabitedIsType,
lambdaFormation_alt,
dependent_set_memberEquality_alt,
unionElimination,
approximateComputation,
dependent_pairFormation_alt,
voidElimination,
productIsType,
equalityIstype,
hyp_replacement,
applyLambdaEquality
Latex:
\mforall{}X,Delta:CubicalSet. \mforall{}s:Delta {}\mrightarrow{} X. \mforall{}A:\{X \mvdash{} \_\}. \mforall{}a,b:\{X \mvdash{} \_:A\}. \mforall{}I:Cname List. \mforall{}alpha:Delta(I).
(I-path(Delta;(A)s;(a)s;(b)s;I;alpha) = I-path(X;A;a;b;I;(s)alpha))
Date html generated:
2020_05_21-AM-11_13_28
Last ObjectModification:
2020_01_15-PM-01_14_19
Theory : cubical!sets
Home
Index