Nuprl Lemma : groupoid-edges-commute1

G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀j:nameset(I).
  ((j ∈ J)
   (∀j'∈J.j' j ∈ Cname)
   (∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(cubical-nerve(fst(G));I;J;x;i).
        edge-arrows-commute(fst(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;x;i;j;c;y))))


Proof




Definitions occuring in Statement :  nerve_box_edge1: nerve_box_edge1(G;box;x;i;j;c;y) nerve_box_label: nerve_box_label(box;L) cubical-nerve: cubical-nerve(X) edge-arrows-commute: edge-arrows-commute(C;I;L;E) open_box: open_box(X;I;J;x;i) nameset: nameset(L) coordinate_name: Cname l_all: (∀x∈L.P[x]) l_member: (x ∈ l) list: List int_seg: {i..j-} pi1: fst(t) all: x:A. B[x] implies:  Q lambda: λx.A[x] natural_number: $n equal: t ∈ T groupoid: Groupoid
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q edge-arrows-commute: edge-arrows-commute(C;I;L;E) not: ¬A member: t ∈ T false: False name-morph: name-morph(I;J) uall: [x:A]. B[x] int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B less_than: a < b squash: T respects-equality: respects-equality(S;T) groupoid: Groupoid subtype_rel: A ⊆B uimplies: supposing a nameset: nameset(L) so_lambda: λ2x.t[x] prop: so_apply: x[s] nerve_box_edge1: nerve_box_edge1(G;box;x;i;j;c;y) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) bnot: ¬bb ifthenelse: if then else fi  coordinate_name: Cname int_upper: {i...} sq_type: SQType(T) guard: {T} bfalse: ff exists: x:A. B[x] or: P ∨ Q assert: b rev_implies:  Q iff: ⇐⇒ Q groupoid-cat: cat(G) top: Top decidable: Dec(P) true: True sq_stable: SqStable(P) satisfiable_int_formula: satisfiable_int_formula(fmla) name-morph-flip: flip(f;y) open_box: open_box(X;I;J;x;i) cand: c∧ B pi2: snd(t) pi1: fst(t) face-name: face-name(f) face-direction: direction(f) face-dimension: dimension(f) I-face: I-face(X;I) eq_int: (i =z j) nequal: a ≠ b ∈  cat-square-commutes: x_y1 y1_z x_y2 y2_z rev_uimplies: rev_uimplies(P;Q) subtract: m nerve_box_edge': nerve_box_edge'(box; c; y) less_than': less_than'(a;b)
Lemmas referenced :  istype-void extd-nameset-respects-equality nil_wf coordinate_name_wf int_seg_wf name-morph_wf open_box_wf cubical-nerve_wf pi1_wf_top small-category_wf subtype_rel_list nameset_wf l_all_wf2 equal_wf l_member_wf list_wf groupoid_wf eq-cname_wf eqtt_to_assert assert-eq-cname subtype_base_sq set_subtype_base le_wf istype-int int_subtype_base eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf eq_int_wf extd-nameset_subtype_int name-morph-flip_wf subtype_rel-equal cat-arrow_wf groupoid-cat_wf nerve_box_label_wf decidable__assert null_wf3 top_wf member-implies-null-eq-bfalse assert_elim btrue_neq_bfalse squash_wf true_wf istype-universe or_wf equal-wf-T-base not_wf name-morph-flips-commute subtype_rel_self iff_weakening_equal extd-nameset-nil bor-bfalse bor-btrue assert_of_eq_int neg_assert_of_eq_int l_exists_wf lelt_wf int_formula_prop_less_lemma intformless_wf decidable__lt int_term_value_constant_lemma int_formula_prop_le_lemma itermConstant_wf intformle_wf decidable__le sq_stable__le decidable__equal-coordinate_name sq_stable__l_member int_formula_prop_wf int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int int_seg_properties l_member_subtype same-face-edge-arrows-commute0 equal-wf-base nameset_subtype_base get_face-wf pi2_wf I-face_wf member_wf bnot_wf int_term_value_subtract_lemma itermSubtract_wf bool_cases iff_transitivity assert_of_bnot and_wf name-morph-flip-flip extd-nameset_wf name-morph-ext cat-square-commutes_wf set_wf nerve_box_edge_wf groupoid-square1_wf cat-ob_wf cat-comp_wf nerve_box_edge_wf2 l_exists_iff subtract_wf groupoid-square2_wf int_seg_subtype_special int_seg_cases istype-le istype-less_than nequal_wf istype-assert nsub2-flip groupoid-cube cat-square-commutes-sym get_face_wf same-face-square-commutes2 face-dimension_wf face-direction_wf nerve_box_edge'_wf false_wf equal-wf-base-T same-face-edge-arrows-commute4 face-name_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalRule cut rename setElimination thin hypothesis functionIsType equalityIstype because_Cache hypothesisEquality sqequalHypSubstitution introduction extract_by_obid inhabitedIsType setIsType applyEquality baseClosed isectElimination productElimination imageElimination dependent_functionElimination independent_functionElimination sqequalBase equalitySymmetry universeIsType instantiate independent_pairEquality Error :memTop,  independent_isectElimination lambdaEquality_alt natural_numberEquality unionElimination equalityElimination equalityTransitivity cumulativity intEquality voidElimination dependent_pairFormation_alt promote_hyp isect_memberEquality_alt inlFormation_alt inrFormation_alt universeEquality imageMemberEquality setEquality productEquality dependent_set_memberEquality int_eqEquality approximateComputation applyLambdaEquality dependent_pairFormation independent_pairFormation voidEquality isect_memberEquality lambdaEquality lambdaFormation inrFormation hyp_replacement inlFormation hypothesis_subsumption dependent_set_memberEquality_alt productIsType closedConclusion equalityIsType1 equalityIsType2

Latex:
\mforall{}G:Groupoid.  \mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}j:nameset(I).
    ((j  \mmember{}  J)
    {}\mRightarrow{}  (\mforall{}j'\mmember{}J.j'  =  j)
    {}\mRightarrow{}  (\mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}box:open\_box(cubical-nerve(fst(G));I;J;x;i).
                edge-arrows-commute(fst(G);I;\mlambda{}c.nerve\_box\_label(box;c);\mlambda{}y,c.  ...)))



Date html generated: 2020_05_21-AM-10_56_56
Last ObjectModification: 2019_12_10-PM-06_28_11

Theory : cubical!sets


Home Index