Nuprl Definition : uniform-Kan-A-filler
uniform-Kan-A-filler(X;A;filler) ==
∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;A;I;alpha;J;x;i).
∀K:Cname List. ∀f:name-morph(I;K).
((∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i))))
⇒ (↑isname(f x))
⇒ ((filler I alpha J x i bx alpha f)
= (filler K f(alpha) map(f;J) (f x) i A-open-box-image(X;A;I;K;f;alpha;bx))
∈ A(f(alpha))))
Definitions occuring in Statement :
A-open-box-image: A-open-box-image(X;A;I;K;f;alpha;bx),
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
cubical-type-ap-morph: (u a f),
cubical-type-at: A(a),
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 :
I-cube: X(I),
int_seg: {i..j-},
natural_number: $n,
A-open-box: A-open-box(X;A;I;alpha;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,
cubical-type-at: A(a),
cubical-type-ap-morph: (u a f),
cube-set-restriction: f(s),
map: map(f;as),
apply: f a,
A-open-box-image: A-open-box-image(X;A;I;K;f;alpha;bx)
FDL editor aliases :
uniform-Kan-A-filler
Latex:
uniform-Kan-A-filler(X;A;filler) ==
\mforall{}I:Cname List. \mforall{}alpha:X(I). \mforall{}J:nameset(I) List. \mforall{}x:nameset(I). \mforall{}i:\mBbbN{}2.
\mforall{}bx:A-open-box(X;A;I;alpha;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{} ((filler I alpha J x i bx alpha f)
= (filler K f(alpha) map(f;J) (f x) i A-open-box-image(X;A;I;K;f;alpha;bx))))
Date html generated:
2016_06_16-PM-06_43_37
Last ObjectModification:
2015_09_23-AM-09_32_08
Theory : cubical!sets
Home
Index