### Nuprl Lemma : sigma-box-fst_wf

`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀B:{X.Kan-type(A) ⊢ _(Kan)}. ∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List.`
`∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i).`
`  (sigma-box-fst(bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i))`

Proof

Definitions occuring in Statement :  sigma-box-fst: `sigma-box-fst(bx)` Kan-type: `Kan-type(Ak)` Kan-cubical-type: `{X ⊢ _(Kan)}` A-open-box: `A-open-box(X;A;I;alpha;J;x;i)` cubical-sigma: `Σ A B` cube-context-adjoin: `X.A` I-cube: `X(I)` cubical-set: `CubicalSet` nameset: `nameset(L)` coordinate_name: `Cname` list: `T List` int_seg: `{i..j-}` all: `∀x:A. B[x]` member: `t ∈ T` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` sigma-box-fst: `sigma-box-fst(bx)` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nameset: `nameset(L)` A-open-box: `A-open-box(X;A;I;alpha;J;x;i)` and: `P ∧ Q` A-face: `A-face(X;A;I;alpha)` top: `Top` pi1: `fst(t)` pi2: `snd(t)` cubical-type-at: `A(a)` cubical-sigma: `Σ A B` cand: `A c∧ B` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` implies: `P `` Q` sq_stable: `SqStable(P)` squash: `↓T` coordinate_name: `Cname` int_upper: `{i...}` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` 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])` less_than: `a < b` le: `A ≤ B` A-face-compatible: `A-face-compatible(X;A;I;alpha;f1;f2)` spreadn: spread3 cubical-type-ap-morph: `(u a f)` l_exists: `(∃x∈L. P[x])` A-face-name: `A-face-name(f)` l_all: `(∀x∈L.P[x])` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  A-open-box_wf cubical-sigma_wf Kan-type_wf cube-context-adjoin_wf subtype_rel_list nameset_wf coordinate_name_wf int_seg_wf list_wf I-cube_wf Kan-cubical-type_wf cubical-set_wf map_wf A-face_wf pi1_wf_top subtype_rel_self cubical-type-at_wf list-diff_wf cname_deq_wf cons_wf nil_wf cube-set-restriction_wf face-map_wf2 cc-adjoin-cube_wf A-adjacent-compatible_wf not_wf l_member_wf l_subset_wf all_wf l_exists_wf equal_wf A-face-name_wf nameset_subtype l_all_wf2 subtract_wf int_seg_properties sq_stable__l_member decidable__equal-coordinate_name sq_stable__le decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf 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 lelt_wf pairwise_wf2 length-map length_wf top_wf select_wf cubical-sigma-at A-face-compatible_wf select-map pairwise-map
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution hypothesis introduction extract_by_obid dependent_functionElimination thin hypothesisEquality isectElimination applyEquality independent_isectElimination lambdaEquality setElimination rename because_Cache sqequalRule natural_numberEquality dependent_set_memberEquality productElimination dependent_pairEquality independent_pairEquality isect_memberEquality voidElimination voidEquality spreadEquality productEquality independent_pairFormation cumulativity universeEquality setEquality independent_functionElimination imageMemberEquality baseClosed imageElimination unionElimination dependent_pairFormation int_eqEquality intEquality computeAll instantiate equalityTransitivity equalitySymmetry applyLambdaEquality

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_(Kan)\}.  \mforall{}B:\{X.Kan-type(A)  \mvdash{}  \_(Kan)\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).
\mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}bx:A-open-box(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;J;x;i).
(sigma-box-fst(bx)  \mmember{}  A-open-box(X;Kan-type(A);I;alpha;J;x;i))

Date html generated: 2017_10_05-AM-10_24_18
Last ObjectModification: 2017_07_28-AM-11_22_19

Theory : cubical!sets

Home Index