### Nuprl Lemma : same-face-square-commutes

`∀[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;[])].`
`    ∀a,b:nameset(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 (((¬(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))) `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))`

Proof

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 o y1_z = x_y2 o y2_z` small-category: `SmallCategory` l_exists: `(∃x∈L. P[x])` l_member: `(x ∈ l)` nil: `[]` list: `T List` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` and: `P ∧ Q` apply: `f a` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` or: `P ∨ Q` l_exists: `(∃x∈L. P[x])` exists: `∃x:A. B[x]` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` nameset: `nameset(L)` false: `False` coordinate_name: `Cname` int_upper: `{i...}` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` prop: `ℙ` cons: `[a / b]` bfalse: `ff` cat-square-commutes: `x_y1 o y1_z = x_y2 o y2_z` so_lambda: `λ2x.t[x]` open_box: `open_box(X;I;J;x;i)` subtype_rel: `A ⊆r B` name-morph: `name-morph(I;J)` so_apply: `x[s]` name-morph-flip: `flip(f;y)` uiff: `uiff(P;Q)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)` bool: `𝔹` unit: `Unit` bnot: `¬bb` squash: `↓T` true: `True` decidable: `Dec(P)`
Lemmas referenced :  same-face-edge-arrows-commute3 nameset_wf list-cases stuck-spread base_wf length_of_nil_lemma null_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 not_wf equal_wf equal-wf-T-base 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 int_seg_wf face-direction_wf open_box_wf subtype_rel_list l_exists_wf list_wf small-category_wf subtype_base_sq bool_wf bool_subtype_base eqff_to_assert eq-cname_wf iff_transitivity assert_wf bnot_wf iff_weakening_uiff assert_of_bnot assert-eq-cname set_subtype_base le_wf int_subtype_base extd-nameset-nil eqtt_to_assert bool_cases_sqequal assert-bnot squash_wf true_wf cat-arrow_wf nerve_box_label_wf decidable__assert null_wf3 top_wf or_wf cat-comp_wf nerve_box_edge_wf subtype_rel-equal iff_weakening_equal set_wf cat-ob_wf name-morph-flips-commute
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination dependent_functionElimination lambdaFormation productElimination independent_pairFormation unionElimination sqequalRule baseClosed isect_memberEquality voidElimination voidEquality natural_numberEquality equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename dependent_pairFormation lambdaEquality int_eqEquality intEquality computeAll promote_hyp hypothesis_subsumption independent_functionElimination hyp_replacement comment axiomEquality productEquality because_Cache applyEquality setEquality dependent_set_memberEquality instantiate cumulativity impliesFunctionality equalityElimination imageElimination universeEquality imageMemberEquality inlFormation inrFormation

Latex:
\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;[])].
\mforall{}a,b:nameset(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)))))
supposing  (\mexists{}j1\mmember{}J.  (\mexists{}j2\mmember{}J.  \mneg{}(j1  =  j2)))

Date html generated: 2017_10_05-PM-03_39_28
Last ObjectModification: 2017_07_28-AM-11_26_21

Theory : cubical!sets

Home Index