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