### Nuprl Lemma : lift-id-faces-wf

`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[alpha:X(I)]. ∀[box:A-open-box(X;(Id_A a b);I;alpha;J;x;i)].`
`  (lift-id-faces(X;A;I;alpha;box) ∈ A-open-box(X;A;I+;iota'(I)(alpha);J;x;i))`

Proof

Definitions occuring in Statement :  lift-id-faces: `lift-id-faces(X;A;I;alpha;box)` cubical-identity: `(Id_A a b)` A-open-box: `A-open-box(X;A;I;alpha;J;x;i)` cubical-term: `{X ⊢ _:AF}` cubical-type: `{X ⊢ _}` cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` iota': `iota'(I)` add-fresh-cname: `I+` nameset: `nameset(L)` coordinate_name: `Cname` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` A-open-box: `A-open-box(X;A;I;alpha;J;x;i)` and: `P ∧ Q` lift-id-faces: `lift-id-faces(X;A;I;alpha;box)` cand: `A c∧ B` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nameset: `nameset(L)` prop: `ℙ` not: `¬A` implies: `P `` Q` false: `False` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` so_apply: `x[s]` coordinate_name: `Cname` int_upper: `{i...}` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` A-face: `A-face(X;A;I;alpha)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` A-adjacent-compatible: `A-adjacent-compatible(X;A;I;alpha;L)` pairwise: `(∀x,y∈L.  P[x; y])` sq_stable: `SqStable(P)` A-face-compatible: `A-face-compatible(X;A;I;alpha;f1;f2)` spreadn: spread3 lift-id-face: `lift-id-face(X;A;I;alpha;face)` cubical-path: `cubical-path(X;A;a;b;I;alpha)` pi1: `fst(t)` cubical-type-at: `A(a)` cubical-identity: `(Id_A a b)` iff: `P `⇐⇒` Q` true: `True` guard: `{T}` rev_implies: `P `` Q` cubical-type-ap-morph: `(u a f)` pi2: `snd(t)` I-path-morph: `I-path-morph(X;A;I;K;f;alpha;p)` I-path: `I-path(X;A;a;b;I;alpha)` named-path-morph: `named-path-morph(X;A;I;K;z;x;f;alpha;w)` sq_type: `SQType(T)` iota': `iota'(I)` has-value: `(a)↓` add-fresh-cname: `I+` assert: `↑b` bnot: `¬bb` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` named-path: `named-path(X;A;a;b;I;alpha;z)` top: `Top` deq: `EqDecider(T)` A-face-name: `A-face-name(f)` l_exists: `(∃x∈L. P[x])` l_all: `(∀x∈L.P[x])`
Lemmas referenced :  map_wf A-face_wf cubical-identity_wf add-fresh-cname_wf cube-set-restriction_wf iota'_wf lift-id-face_wf nameset_wf subtype_rel_list coordinate_name_wf A-adjacent-compatible_wf l_member_wf istype-void l_subset_wf l_exists_wf equal_wf int_seg_wf A-face-name_wf nameset_subtype subtype-add-fresh-cname l_all_wf2 not_wf subtract_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf decidable__lt istype-le istype-less_than pi1_wf_top subtype_rel_product cubical-type-at_wf list-diff_wf cname_deq_wf cons_wf nil_wf face-map_wf2 top_wf pairwise_wf2 A-open-box_wf I-cube_wf list_wf cubical-term_wf cubical-type_wf cubical-set_wf length-map length_wf select_wf sq_stable__l_member decidable__equal-coordinate_name sq_stable__le A-face-compatible_wf select-map path-eq-equiv path-eq_wf I-path_wf subtype_quotient set-path-name_wf fresh-cname_wf subtype_rel_sets_simple member-list-diff true_wf squash_wf name-morph_wf name-comp_wf subtype_rel_wf list-diff2-sym iff_weakening_equal subtype_rel_self cubical-type-ap-morph_wf list-diff2 cube-set-restriction-comp face-maps-commute cubical-path-same-name I-path-morph_wf named-path-equal-implies fresh-cname-not-member2 subtype_base_sq set_subtype_base le_wf int_subtype_base coordinate_name-value-type set-value-type value-type-has-value set_wf cons_member or_wf member_singleton assert-bnot bool_subtype_base bool_cases_sqequal eqff_to_assert assert-deq-member eqtt_to_assert bool_wf deq-member_wf list-diff-cons and_wf iota_wf subtype_rel-equal iota-face-map cubical-type-ap-rename-one-equal fresh-cname-not-member-list-diff istype-universe list-diff-cons-single list_subtype_base rename-one-name_wf iota-two-face-maps name-comp-assoc rename-one-iota cubical-type-ap-morph-comp int_formula_prop_eq_lemma intformeq_wf deq_wf trivial-equal extend-name-morph_wf extended-face-map bfalse_wf bor_wf deq_member_nil_lemma deq_member_cons_lemma l_subset-l_contains cons-l_contains l_contains_weakening l_contains_transitivity map-length equal_functionality_wrt_subtype_rel2 lelt_wf product_subtype_base nameset_subtype_base decidable__equal_int l_subset_right_cons_trivial length-map-sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality_alt productElimination extract_by_obid isectElimination hypothesisEquality hypothesis lambdaEquality_alt universeIsType independent_pairFormation lambdaFormation_alt because_Cache applyEquality independent_isectElimination sqequalRule productIsType functionIsType productEquality imageElimination independent_pairEquality inhabitedIsType setIsType natural_numberEquality dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality Error :memTop,  voidElimination instantiate cumulativity axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt isectIsTypeImplies imageMemberEquality baseClosed equalityIstype lambdaEquality lambdaFormation universeEquality hyp_replacement setEquality applyLambdaEquality promote_hyp intEquality callbyvalueReduce inrFormation inlFormation addLevel dependent_pairFormation equalityElimination dependent_set_memberEquality equalityIsType1 closedConclusion voidEquality isect_memberEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[a,b:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].
\mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].  \mforall{}[alpha:X(I)].  \mforall{}[box:A-open-box(X;(Id\_A  a  b);I;alpha;J;x;i)].
(lift-id-faces(X;A;I;alpha;box)  \mmember{}  A-open-box(X;A;I+;iota'(I)(alpha);J;x;i))

Date html generated: 2020_05_21-AM-11_12_29
Last ObjectModification: 2020_01_03-PM-06_02_22

Theory : cubical!sets

Home Index