Nuprl Lemma : Kan-A-filler_wf

∀[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)].
  (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-},  uall: ∀[x:A]. B[x],  prop: ℙ,  member: t ∈ T,  function: x:A ⟶ B[x],  natural_number: $n
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  Kan-A-filler: Kan-A-filler(X;A;filler),  so_lambda: λ2x.t[x],  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),  so_apply: x[s],  and: P ∧ Q,  implies: P ⇒ Q,  sq_stable: SqStable(P),  squash: ↓T
Lemmas referenced :  decidable__equal-coordinate_name,  sq_stable__l_subset,  cubical-set_wf,  cubical-type_wf,  cubical-type-at_wf,  fills-A-open-box_wf,  coordinate_name_wf,  subtype_rel_list,  A-open-box_wf,  int_seg_wf,  nameset_wf,  list_wf,  I-cube_wf,  all_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  sqequalRule,  lemma_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  because_Cache,  lambdaEquality,  hypothesisEquality,  hypothesis,  natural_numberEquality,  dependent_functionElimination,  applyEquality,  independent_isectElimination,  setElimination,  rename,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  functionEquality,  isect_memberEquality,  productElimination,  independent_functionElimination,  lambdaFormation,  imageMemberEquality,  baseClosed,  imageElimination
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)].
    (Kan-A-filler(X;A;filler)  \mmember{}  \mBbbP{})


Date html generated: 2016_06_16-PM-06_43_23
Last ObjectModification: 2016_01_18-PM-04_52_20

Theory : cubical!sets


Home Index