### Nuprl Lemma : uniform-Kan-filler_wf

`∀[X:CubicalSet]. ∀[filler:I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I)].`
`  (uniform-Kan-filler(X;filler) ∈ ℙ)`

Proof

Definitions occuring in Statement :  uniform-Kan-filler: `uniform-Kan-filler(X;filler)` open_box: `open_box(X;I;J;x;i)` 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-filler: `uniform-Kan-filler(X;filler)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nameset: `nameset(L)` name-morph: `name-morph(I;J)` uiff: `uiff(P;Q)` and: `P ∧ Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` prop: `ℙ` open_box: `open_box(X;I;J;x;i)` name-morph-domain: `name-morph-domain(f;I)` all: `∀x:A. B[x]` 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 :  list_wf coordinate_name_wf nameset_wf int_seg_wf open_box_wf subtype_rel_list I-cube_wf cubical-set_wf l_member_wf assert_wf isname_wf cube-set-restriction_wf assert-isname open_box_image_wf all_wf name-morph_wf equal_wf filter_wf5 cons_wf cons_member member_filter_2 subtype_base_sq set_subtype_base int_subtype_base and_wf extd-nameset_wf assert_elim bool_wf bool_subtype_base list-subtype map_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry functionEquality extract_by_obid isectElimination thin hypothesisEquality natural_numberEquality applyEquality independent_isectElimination lambdaEquality setElimination rename because_Cache isect_memberEquality functionExtensionality productElimination independent_pairFormation dependent_set_memberEquality setEquality dependent_functionElimination independent_functionElimination unionElimination instantiate applyLambdaEquality cumulativity lambdaFormation

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[filler:I:(Cname  List)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  open\_box(X;I;J;x;i)
{}\mrightarrow{}  X(I)].
(uniform-Kan-filler(X;filler)  \mmember{}  \mBbbP{})

Date html generated: 2017_10_05-AM-10_26_20
Last ObjectModification: 2017_07_28-AM-11_22_49

Theory : cubical!sets

Home Index