Nuprl Definition : Kan-cubical-set
KanCubicalSet ==
{p:X:CubicalSet × (I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I))|
let X,filler = p
in Kan-filler(X;filler) ∧ uniform-Kan-filler(X;filler)}
Definitions occuring in Statement :
uniform-Kan-filler: uniform-Kan-filler(X;filler),
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-},
and: P ∧ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
product: x:A × B[x],
cubical-set: CubicalSet,
coordinate_name: Cname,
list: T List,
nameset: nameset(L),
int_seg: {i..j-},
natural_number: $n,
function: x:A ⟶ B[x],
open_box: open_box(X;I;J;x;i),
I-cube: X(I),
spread: spread def,
and: P ∧ Q,
Kan-filler: Kan-filler(X;filler),
uniform-Kan-filler: uniform-Kan-filler(X;filler)
FDL editor aliases :
Kan-cubical-set
Latex:
KanCubicalSet ==
\{p:X:CubicalSet \mtimes{} (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))|
let X,filler = p
in Kan-filler(X;filler) \mwedge{} uniform-Kan-filler(X;filler)\}
Date html generated:
2016_06_16-PM-06_49_36
Last ObjectModification:
2015_09_23-AM-09_32_40
Theory : cubical!sets
Home
Index