Nuprl Definition : cubical-id-box

cubical-id-box(X;A;a;b;I;alpha;box) ==
  extend-A-open-box(lift-id-faces(X;A;I;alpha;box);term-A-face(a;I;alpha;0);term-A-face(b;I;alpha;1))


Definitions occuring in Statement :  term-A-face: term-A-face(a;I;alpha;i),  lift-id-faces: lift-id-faces(X;A;I;alpha;box),  extend-A-open-box: extend-A-open-box(bx;f1;f2),  natural_number: $n
Definitions occuring in definition :  extend-A-open-box: extend-A-open-box(bx;f1;f2),  lift-id-faces: lift-id-faces(X;A;I;alpha;box),  term-A-face: term-A-face(a;I;alpha;i),  natural_number: $n
FDL editor aliases :  cubical-id-box
Latex:
cubical-id-box(X;A;a;b;I;alpha;box)  ==
    extend-A-open-box(lift-id-faces(X;A;I;alpha;box);term-A-face(a;I;alpha;0);
                                        term-A-face(b;I;alpha;1))


Date html generated: 2016_06_16-PM-07_51_28
Last ObjectModification: 2015_09_23-AM-09_34_40

Theory : cubical!sets


Home Index