Nuprl Lemma : Kan_sigma_filler_wf

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

Proof

Definitions occuring in Statement :  Kan_sigma_filler: `Kan_sigma_filler(A;B)` Kan-type: `Kan-type(Ak)` Kan-cubical-type: `{X ⊢ _(Kan)}` Kan-A-filler: `Kan-A-filler(X;A;filler)` A-open-box: `A-open-box(X;A;I;alpha;J;x;i)` cubical-sigma: `Σ A B` cube-context-adjoin: `X.A` cubical-type-at: `A(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` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` Kan_sigma_filler: `Kan_sigma_filler(A;B)` uall: `∀[x:A]. B[x]` nameset: `nameset(L)` uimplies: `b supposing a` subtype_rel: `A ⊆r B` squash: `↓T` sq_stable: `SqStable(P)` implies: `P `` Q` and: `P ∧ Q` A-open-box: `A-open-box(X;A;I;alpha;J;x;i)` top: `Top` let: let Kan-A-filler: `Kan-A-filler(X;A;filler)` fills-A-open-box: `fills-A-open-box(X;A;I;alpha;bx;cube)` fills-A-faces: `fills-A-faces(X;A;I;alpha;bx;L)` l_all: `(∀x∈L.P[x])` spreadn: spread3 is-A-face: `is-A-face(X;A;I;alpha;bx;f)` A-face: `A-face(X;A;I;alpha)` less_than: `a < b` prop: `ℙ` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` or: `P ∨ Q` decidable: `Dec(P)` int_upper: `{i...}` coordinate_name: `Cname` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` sigma-box-snd: `sigma-box-snd(bx)` sigma-box-fst: `sigma-box-fst(bx)` pi1: `fst(t)` pi2: `snd(t)` respects-equality: `respects-equality(S;T)` cc-adjoin-cube: `(v;u)` cube-context-adjoin: `X.A` cube-set-restriction: `f(s)` cubical-type-ap-morph: `(u a f)` cubical-sigma: `Σ A B` true: `True` cubical-type-at: `A(a)`
Lemmas referenced :  Kan-cubical-type_wf cube-context-adjoin_wf Kan-type_wf cubical-set_wf I-cube_wf list_wf int_seg_wf coordinate_name_wf nameset_wf subtype_rel_list cubical-sigma_wf A-open-box_wf cubical-type-at_wf sigma-box-snd_wf cc-adjoin-cube_wf sigma-box-fst_wf Kanfiller_wf decidable__equal-coordinate_name sq_stable__l_subset istype-void cubical-sigma-at length_wf A-face_wf cubical-type-ap-morph_wf face-map_wf2 cube-set-restriction_wf nil_wf cons_wf cname_deq_wf list-diff_wf sq_stable__equal int_formula_prop_less_lemma intformless_wf decidable__lt int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma istype-int itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le sq_stable__le sq_stable__l_member int_seg_properties select_wf fills-A-open-box_wf length-map select-map top_wf subtype-respects-equality equal_functionality_wrt_subtype_rel2 subtype_rel_self subtype_rel-equal cc-adjoin-cube-restriction is-A-face_wf Kan-A-filler_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut dependent_set_memberEquality_alt sqequalHypSubstitution hypothesis universeIsType introduction extract_by_obid isectElimination thin hypothesisEquality natural_numberEquality sqequalRule inhabitedIsType rename setElimination independent_isectElimination applyEquality dependent_functionElimination lambdaEquality_alt equalitySymmetry equalityTransitivity equalityIsType1 dependent_pairEquality_alt imageElimination baseClosed imageMemberEquality because_Cache independent_functionElimination productElimination voidElimination isect_memberEquality_alt applyLambdaEquality independent_pairFormation int_eqEquality dependent_pairFormation_alt approximateComputation unionElimination equalityIstype hyp_replacement spreadEquality productEquality productIsType

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

Date html generated: 2019_11_05-PM-00_30_26
Last ObjectModification: 2018_12_10-AM-09_29_41

Theory : cubical!sets

Home Index