### Nuprl Lemma : groupoid-nerve-filler-fills

`∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(cubical-nerve(cat(G));I;J;x;i).`
`  fills-open_box(cubical-nerve(cat(G));I;bx;(λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)) I J x i bx)`

Proof

Definitions occuring in Statement :  groupoid-nerve-filler: `groupoid-nerve-filler(G;I;J;x;i;box)` cubical-nerve: `cubical-nerve(X)` fills-open_box: `fills-open_box(X;I;bx;cube)` open_box: `open_box(X;I;J;x;i)` nameset: `nameset(L)` coordinate_name: `Cname` groupoid-cat: `cat(G)` groupoid: `Groupoid` list: `T List` int_seg: `{i..j-}` all: `∀x:A. B[x]` apply: `f a` lambda: `λx.A[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nameset: `nameset(L)` groupoid-nerve-filler: `groupoid-nerve-filler(G;I;J;x;i;box)` top: `Top` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` cons: `[a / b]` prop: `ℙ` ge: `i ≥ j ` int_seg: `{i..j-}` lelt: `i ≤ j < k` sq_stable: `SqStable(P)` squash: `↓T` coordinate_name: `Cname` int_upper: `{i...}` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` true: `True` I-face: `I-face(X;I)` face-name: `face-name(f)` pi1: `fst(t)` pi2: `snd(t)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` fills-open_box: `fills-open_box(X;I;bx;cube)` fills-faces: `fills-faces(X;I;bx;L)` l_all: `(∀x∈L.P[x])` select: `L[n]` groupoid-nerve-filler0: `groupoid-nerve-filler0(I;x;box)` cubical-nerve: `cubical-nerve(X)` is-face: `is-face(X;I;bx;f)` face-cube: `cube(f)` face-direction: `direction(f)` face-dimension: `dimension(f)` cube-set-restriction: `f(s)` le: `A ≤ B` open_box: `open_box(X;I;J;x;i)` l_exists: `(∃x∈L. P[x])` nil: `[]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` I-cube: `X(I)` cand: `A c∧ B` less_than: `a < b` name-morph: `name-morph(I;J)` face-map: `(x:=i)` name-comp: `(f o g)` compose: `f o g` uext: `uext(g)` isname: `isname(z)` le_int: `i ≤z j` lt_int: `i <z j` less_than': `less_than'(a;b)` functor-ob: `ob(F)` cat-functor: `Functor(C1;C2)` groupoid-nerve-filler2: `groupoid-nerve-filler2(C;I;J;box)` poset-functor: `poset-functor(J;K;f)` functor-comp: `functor-comp(F;G)` mk-functor: mk-functor cat-ob: `cat-ob(C)` poset-cat: `poset-cat(J)` nat: `ℕ` subtract: `n - m` listp: `A List+` groupoid-nerve-filler1: `groupoid-nerve-filler1(G;I;J;x;i;box)`
Lemmas referenced :  open_box_wf cubical-nerve_wf groupoid-cat_wf subtype_rel_list nameset_wf coordinate_name_wf int_seg_wf list_wf groupoid_wf null_wf3 top_wf istype-void eqtt_to_assert assert_of_null eqff_to_assert bool_subtype_base bool_cases_sqequal subtype_base_sq bool_wf assert-bnot iff_weakening_uiff assert_wf equal-wf-T-base list-cases product_subtype_list open_box-nil subtype_rel_weakening nil_wf I-face_wf equal-wf-base equal_wf face-name_wf hd_wf int_seg_properties sq_stable__l_member decidable__equal-coordinate_name sq_stable__le decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformeq_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_var_lemma int_formula_prop_eq_lemma int_formula_prop_wf length_of_nil_lemma int_subtype_base length_of_cons_lemma reduce_hd_cons_lemma pi1_wf_top nameset_subtype_base set_subtype_base lelt_wf cubical-nerve-I-cube decidable__equal_int int_seg_subtype_special int_seg_cases intformless_wf int_formula_prop_less_lemma length_wf cat-functor_wf poset-cat_wf list-diff_wf cname_deq_wf cons_wf iota-wf poset-functor_wf face-map_wf2 squash_wf true_wf istype-universe functor-comp-assoc functor-comp_wf small-category_wf poset-functor-comp subtype_rel_self iff_weakening_equal iota-identity poset-id-functor functor-comp-id cons_member l_member_wf member-list-diff non_neg_length itermAdd_wf int_term_value_add_lemma null_nil_lemma btrue_wf null_cons_lemma bfalse_wf btrue_neq_bfalse lt_int_wf assert_of_lt_int less_than_wf istype-less_than length-open_box-ge-3 stuck-spread istype-base ob_pair_lemma poset-functor-extends-box-faces select_wf decidable__lt not_wf subtract_wf itermSubtract_wf int_term_value_subtract_lemma istype-le decidable__equal_int_seg name-comp_wf name-morph_wf nerve_box_label_wf member_singleton le_wf extd-nameset-nil eq_int_wf assert_of_eq_int neg_assert_of_eq_int isname-name name-morph-flip_wf nerve_box_edge_wf subtype_rel-equal cat-arrow_wf or_wf name-morph-flip-face-map1 eq_int_eq_true istype-false poset-extend-unique groupoid-nerve-filler2_wf poset_functor_extend-extends poset-functor-extends_wf cat-ob_wf cat-id_wf cat-comp_wf arrow_pair_lemma cat_ob_pair_lemma cat_arrow_triple_lemma poset_functor_extend-face-map assert_of_le_int extd-nameset_subtype_int length-open_box-le-3 istype-assert poset-functor-extends-box-faces-1 nerve_box_edge1_wf listp_properties length_wf_nat not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel list-subtype groupoid-nerve-filler1_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality independent_isectElimination lambdaEquality_alt setElimination rename inhabitedIsType sqequalRule natural_numberEquality isect_memberEquality_alt voidElimination unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation_alt equalityIsType3 promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination because_Cache baseClosed equalityIsType1 hypothesis_subsumption setEquality productEquality closedConclusion imageMemberEquality imageElimination approximateComputation int_eqEquality independent_pairFormation independent_pairEquality intEquality applyLambdaEquality universeEquality hyp_replacement inlFormation_alt productIsType functionIsType dependent_set_memberEquality_alt equalityIsType4 inrFormation_alt equalityIsType2 setIsType dependent_pairEquality_alt functionEquality addEquality minusEquality

Latex:
\mforall{}G:Groupoid.  \mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.
\mforall{}bx:open\_box(cubical-nerve(cat(G));I;J;x;i).
fills-open\_box(cubical-nerve(cat(G));I;bx;(\mlambda{}I,J,x,i,box.  groupoid-nerve-filler(G;I;J;x;i;box))  I  J\000C  x  i  bx)

Date html generated: 2019_11_05-PM-00_39_15
Last ObjectModification: 2018_11_08-PM-11_57_37

Theory : cubical!sets

Home Index