Nuprl Definition : Kan_id_filler
Kan_id_filler(X;A;a;b) == λI,alpha,J,x,i,bx. <fresh-cname(I), filler(x;i;cubical-id-box(X;Kan-type(A);a;b;I;alpha;bx))>
Definitions occuring in Statement :
cubical-id-box: cubical-id-box(X;A;a;b;I;alpha;box),
Kanfiller: filler(x;i;bx),
Kan-type: Kan-type(Ak),
cube-set-restriction: f(s),
iota: iota(x),
fresh-cname: fresh-cname(I),
cons: [a / b],
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
pair: <a, b>,
Kanfiller: filler(x;i;bx),
cube-set-restriction: f(s),
iota: iota(x),
cons: [a / b],
fresh-cname: fresh-cname(I),
cubical-id-box: cubical-id-box(X;A;a;b;I;alpha;box),
Kan-type: Kan-type(Ak)
FDL editor aliases :
Kan_id_filler
Latex:
Kan\_id\_filler(X;A;a;b) ==
\mlambda{}I,alpha,J,x,i,bx. <fresh-cname(I), filler(x;i;cubical-id-box(X;Kan-type(A);a;b;I;alpha;bx))>
Date html generated:
2016_06_16-PM-07_52_16
Last ObjectModification:
2015_09_23-AM-09_34_44
Theory : cubical!sets
Home
Index