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

Proof

Definitions occuring in Statement :  Kan-filler: `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` Kan-filler: `Kan-filler(X;filler)` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` nameset: `nameset(L)` open_box: `open_box(X;I;J;x;i)` so_apply: `x[s]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  decidable__equal-coordinate_name sq_stable__l_subset cubical-set_wf I-cube_wf fills-open_box_wf subtype_rel_list open_box_wf int_seg_wf nameset_wf coordinate_name_wf list_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality hypothesisEquality because_Cache natural_numberEquality applyEquality independent_isectElimination setElimination rename axiomEquality equalityTransitivity equalitySymmetry functionEquality isect_memberEquality productElimination dependent_functionElimination independent_functionElimination lambdaFormation imageMemberEquality baseClosed imageElimination

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)].
(Kan-filler(X;filler)  \mmember{}  \mBbbP{})

Date html generated: 2016_06_16-PM-06_49_17
Last ObjectModification: 2016_01_18-PM-04_51_49

Theory : cubical!sets

Home Index