Nuprl Lemma : uniform-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)].
  (uniform-Kan-A-filler(X;A;filler) ∈ ℙ)


Proof



Definitions occuring in Statement :  uniform-Kan-A-filler: uniform-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,  uniform-Kan-A-filler: uniform-Kan-A-filler(X;A;filler),  so_lambda: λ2x.t[x],  all: ∀x:A. B[x],  subtype_rel: A ⊆r B,  implies: P ⇒ Q,  prop: ℙ,  nameset: nameset(L),  uimplies: b supposing a,  name-morph: name-morph(I;J),  so_apply: x[s],  uiff: uiff(P;Q),  and: P ∧ Q,  A-open-box: A-open-box(X;A;I;alpha;J;x;i),  name-morph-domain: name-morph-domain(f;I),  iff: P ⇐⇒ Q,  or: P ∨ Q,  rev_implies: P ⇐ Q,  cand: A c∧ B,  coordinate_name: Cname,  int_upper: {i...},  sq_type: SQType(T),  guard: {T},  assert: ↑b,  ifthenelse: if b then t else f fi ,  btrue: tt,  true: True,  l_subset: l_subset(T;as;bs)
Lemmas referenced :  all_wf,  list_wf,  coordinate_name_wf,  I-cube_wf,  nameset_wf,  int_seg_wf,  A-open-box_wf,  name-morph_wf,  l_member_wf,  subtype_rel_list,  assert_wf,  isname_wf,  cubical-type-at_wf,  cubical-type_wf,  cubical-set_wf,  assert-isname,  cons_member,  member_filter_2,  subtype_base_sq,  set_subtype_base,  int_subtype_base,  and_wf,  equal_wf,  extd-nameset_wf,  assert_elim,  bool_wf,  bool_subtype_base,  filter_wf5,  cons_wf,  list-subtype,  map_wf,  cube-set-restriction_wf,  cubical-type-ap-morph_wf,  A-open-box-image_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesis,  sqequalRule,  lambdaEquality,  hypothesisEquality,  natural_numberEquality,  dependent_functionElimination,  applyEquality,  because_Cache,  functionEquality,  setElimination,  rename,  independent_isectElimination,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  isect_memberEquality,  productElimination,  dependent_set_memberEquality,  independent_functionElimination,  unionElimination,  setEquality,  instantiate,  independent_pairFormation,  applyLambdaEquality,  cumulativity,  lambdaFormation,  functionExtensionality
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)].
    (uniform-Kan-A-filler(X;A;filler)  \mmember{}  \mBbbP{})


Date html generated: 2017_10_05-AM-10_23_25
Last ObjectModification: 2017_07_28-AM-11_21_54

Theory : cubical!sets


Home Index