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