Nuprl Lemma : same-face-square-commutes2

[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[f,g,h,k:name-morph(I;[])].
    (nerve_box_edge(box;f;a) nerve_box_edge(box;g;b) nerve_box_edge(box;f;b) nerve_box_edge(box;h;a)) supposing 
       (((((¬(a b ∈ nameset(I))) ∧ ((f a) 0 ∈ ℕ2))
       ∧ ((f b) 0 ∈ ℕ2)
       ∧ (g flip(f;a) ∈ name-morph(I;[]))
       ∧ (h flip(f;b) ∈ name-morph(I;[]))
       ∧ (k flip(flip(f;a);b) ∈ name-morph(I;[])))
       ∧ (∃v:I-face(cubical-nerve(C);I)
           ((v ∈ box)
           ∧ (dimension(v) b ∈ Cname))
           ∧ (dimension(v) a ∈ Cname))
           ∧ (direction(v) (f dimension(v)) ∈ ℕ2)))) and 
       (((∃j1∈J. ¬(j1 a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 b ∈ Cname)))
       ∨ ((¬↑null(J)) ∧ ((f x) i ∈ ℤ) ∧ ((flip(f;a) x) i ∈ ℤ) ∧ ((flip(f;b) x) i ∈ ℕ2))))


Definitions occuring in Statement :  nerve_box_edge: nerve_box_edge(box;c;y) nerve_box_label: nerve_box_label(box;L) cubical-nerve: cubical-nerve(X) open_box: open_box(X;I;J;x;i) face-direction: direction(f) face-dimension: dimension(f) I-face: I-face(X;I) name-morph-flip: flip(f;y) name-morph: name-morph(I;J) nameset: nameset(L) coordinate_name: Cname cat-square-commutes: x_y1 y1_z x_y2 y2_z small-category: SmallCategory l_exists: (∃x∈L. P[x]) l_member: (x ∈ l) null: null(as) nil: [] list: List int_seg: {i..j-} assert: b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] not: ¬A or: P ∨ Q and: P ∧ Q apply: a natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] uimplies: supposing a cat-square-commutes: x_y1 y1_z x_y2 y2_z and: P ∧ Q cand: c∧ B exists: x:A. B[x] prop: name-morph: name-morph(I;J) subtype_rel: A ⊆B so_lambda: λ2x.t[x] open_box: open_box(X;I;J;x;i) nameset: nameset(L) so_apply: x[s] top: Top int_seg: {i..j-} or: P ∨ Q assert: b ifthenelse: if then else fi  btrue: tt l_exists: (∃x∈L. P[x]) select: L[n] nil: [] it: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] guard: {T} lelt: i ≤ j < k false: False coordinate_name: Cname int_upper: {i...} satisfiable_int_formula: satisfiable_int_formula(fmla) implies:  Q not: ¬A true: True cons: [a b] bfalse: ff squash: T decidable: Dec(P) iff: ⇐⇒ Q rev_implies:  Q sq_stable: SqStable(P) nerve_box_edge': nerve_box_edge'(box; c; y) name-morph-flip: flip(f;y) uiff: uiff(P;Q) sq_type: SQType(T)
Lemmas referenced :  same-face-edge-arrows-commute0 not_wf equal_wf equal-wf-T-base int_seg_wf name-morph_wf nil_wf coordinate_name_wf name-morph-flip_wf exists_wf I-face_wf cubical-nerve_wf l_member_wf face-dimension_wf nameset_wf face-direction_wf or_wf l_exists_wf assert_wf null_wf3 subtype_rel_list top_wf extd-nameset_subtype_int open_box_wf list_wf small-category_wf list-cases null_nil_lemma stuck-spread base_wf length_of_nil_lemma int_seg_properties satisfiable-full-omega-tt intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf product_subtype_list null_cons_lemma false_wf squash_wf true_wf cat-arrow_wf nerve_box_label_wf decidable__assert extd-nameset-nil cat-comp_wf cat-ob_wf iff_weakening_equal nerve_box_edge_wf2 decidable__equal_int intformnot_wf intformeq_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma sq_stable__l_member decidable__equal-coordinate_name sq_stable__le decidable__le decidable__lt lelt_wf subtype_rel-equal nerve_box_edge'_wf set_wf subtype_base_sq bool_wf bool_subtype_base eqff_to_assert eq-cname_wf iff_transitivity bnot_wf iff_weakening_uiff assert_of_bnot assert-eq-cname set_subtype_base le_wf int_subtype_base name-morph-flips-commute
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination lambdaFormation productElimination independent_isectElimination independent_pairFormation productEquality because_Cache natural_numberEquality applyEquality setElimination rename sqequalRule baseClosed lambdaEquality setEquality isect_memberEquality voidElimination voidEquality intEquality axiomEquality equalityTransitivity equalitySymmetry unionElimination applyLambdaEquality dependent_pairFormation int_eqEquality computeAll independent_functionElimination promote_hyp hypothesis_subsumption hyp_replacement imageElimination universeEquality inlFormation inrFormation imageMemberEquality dependent_set_memberEquality instantiate cumulativity impliesFunctionality

\mforall{}[C:SmallCategory].  \mforall{}[I:Cname  List].  \mforall{}[J:nameset(I)  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
\mforall{}[box:open\_box(cubical-nerve(C);I;J;x;i)].  \mforall{}[f,g,h,k:name-morph(I;[])].
        (nerve\_box\_edge(box;f;a)  o  nerve\_box\_edge(box;g;b)
          =  nerve\_box\_edge(box;f;b)  o  nerve\_box\_edge(box;h;a))  supposing 
              (((((\mneg{}(a  =  b))  \mwedge{}  ((f  a)  =  0))
              \mwedge{}  ((f  b)  =  0)
              \mwedge{}  (g  =  flip(f;a))
              \mwedge{}  (h  =  flip(f;b))
              \mwedge{}  (k  =  flip(flip(f;a);b)))
              \mwedge{}  (\mexists{}v:I-face(cubical-nerve(C);I)
                      ((v  \mmember{}  box)
                      \mwedge{}  (\mneg{}(dimension(v)  =  b))
                      \mwedge{}  (\mneg{}(dimension(v)  =  a))
                      \mwedge{}  (direction(v)  =  (f  dimension(v))))))  and 
              (((\mexists{}j1\mmember{}J.  \mneg{}(j1  =  a))  \mwedge{}  (\mexists{}j2\mmember{}J.  \mneg{}(j2  =  b)))
              \mvee{}  ((\mneg{}\muparrow{}null(J))  \mwedge{}  ((f  x)  =  i)  \mwedge{}  ((flip(f;a)  x)  =  i)  \mwedge{}  ((flip(f;b)  x)  =  i))))

Date html generated: 2017_10_05-PM-03_39_45
Last ObjectModification: 2017_07_28-AM-11_26_32

Theory : cubical!sets

Home Index