Nuprl Definition : uniform-Kan-filler
uniform-Kan-filler(X;filler) ==
∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X;I;J;x;i). ∀K:Cname List. ∀f:name-morph(I;K).
((∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i))))
⇒ (↑isname(f x))
⇒ (f(filler I J x i bx) = (filler K map(f;J) (f x) i open_box_image(X;I;K;f;bx)) ∈ X(K)))
Definitions occuring in Statement :
open_box_image: open_box_image(X;I;K;f;bx),
open_box: open_box(X;I;J;x;i),
cube-set-restriction: f(s),
I-cube: X(I),
name-morph: name-morph(I;J),
isname: isname(z),
nameset: nameset(L),
coordinate_name: Cname,
l_member: (x ∈ l),
map: map(f;as),
list: T List,
int_seg: {i..j-},
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
int_seg: {i..j-},
natural_number: $n,
open_box: open_box(X;I;J;x;i),
list: T List,
name-morph: name-morph(I;J),
all: ∀x:A. B[x],
nameset: nameset(L),
l_member: (x ∈ l),
coordinate_name: Cname,
implies: P ⇒ Q,
assert: ↑b,
isname: isname(z),
equal: s = t ∈ T,
I-cube: X(I),
cube-set-restriction: f(s),
map: map(f;as),
apply: f a,
open_box_image: open_box_image(X;I;K;f;bx)
FDL editor aliases :
uniform-Kan-filler
Latex:
uniform-Kan-filler(X;filler) ==
\mforall{}I:Cname List. \mforall{}J:nameset(I) List. \mforall{}x:nameset(I). \mforall{}i:\mBbbN{}2. \mforall{}bx:open\_box(X;I;J;x;i). \mforall{}K:Cname List.
\mforall{}f:name-morph(I;K).
((\mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i))))
{}\mRightarrow{} (\muparrow{}isname(f x))
{}\mRightarrow{} (f(filler I J x i bx) = (filler K map(f;J) (f x) i open\_box\_image(X;I;K;f;bx))))
Date html generated:
2016_06_16-PM-06_49_22
Last ObjectModification:
2015_09_23-AM-09_32_37
Theory : cubical!sets
Home
Index