Nuprl Lemma : sq_stable_Kan-A-filler

∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[filler:I:(Cname List)
                                        ⟶ alpha:X(I)
                                        ⟶ J:(nameset(I) List)
                                        ⟶ x:nameset(I)
                                        ⟶ i:ℕ2
                                        ⟶ A-open-box(X;A;I;alpha;J;x;i)
                                        ⟶ A(alpha)].
  SqStable(Kan-A-filler(X;A;filler))


Proof



Definitions occuring in Statement :  Kan-A-filler: Kan-A-filler(X;A;filler),  A-open-box: A-open-box(X;A;I;alpha;J;x;i),  cubical-type-at: A(a),  cubical-type: {X ⊢ _},  I-cube: X(I),  cubical-set: CubicalSet,  nameset: nameset(L),  coordinate_name: Cname,  list: T List,  int_seg: {i..j-},  sq_stable: SqStable(P),  uall: ∀[x:A]. B[x],  function: x:A ⟶ B[x],  natural_number: $n
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  Kan-A-filler: Kan-A-filler(X;A;filler),  member: t ∈ T,  all: ∀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,  implies: P ⇒ Q,  sq_stable: SqStable(P),  squash: ↓T,  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),  so_lambda: λ2x.t[x],  prop: ℙ,  so_apply: x[s],  is-A-face: is-A-face(X;A;I;alpha;bx;f),  spreadn: spread3,  A-face: A-face(X;A;I;alpha)
Lemmas referenced :  list_wf,  coordinate_name_wf,  I-cube_wf,  nameset_wf,  int_seg_wf,  A-open-box_wf,  subtype_rel_list,  cubical-type-at_wf,  cubical-type_wf,  cubical-set_wf,  sq_stable__l_subset,  decidable__equal-coordinate_name,  sq_stable__l_all,  A-face_wf,  l_member_wf,  is-A-face_wf,  sq_stable__all,  all_wf,  fills-A-open-box_wf,  squash_wf,  equal_wf,  list-diff_wf,  cname_deq_wf,  cons_wf,  nil_wf,  cube-set-restriction_wf,  face-map_wf2,  cubical-type-ap-morph_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  functionIsType,  universeIsType,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesis,  hypothesisEquality,  natural_numberEquality,  dependent_functionElimination,  applyEquality,  independent_isectElimination,  lambdaEquality_alt,  setElimination,  rename,  inhabitedIsType,  sqequalRule,  productElimination,  because_Cache,  independent_functionElimination,  lambdaFormation_alt,  imageMemberEquality,  baseClosed,  imageElimination,  setIsType,  closedConclusion,  axiomEquality
Latex:
\mforall{}[X:CubicalSet].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[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;A;I;alpha;J;x;i)
                                                                                {}\mrightarrow{}  A(alpha)].
    SqStable(Kan-A-filler(X;A;filler))


Date html generated: 2019_11_05-PM-00_29_26
Last ObjectModification: 2018_11_14-AM-10_17_25

Theory : cubical!sets


Home Index