Nuprl Definition : cu-cube-restriction

cu-cube-restriction(alpha;L;J;f;a;T) ==  (snd(fst(alpha))) L J f a T


Definitions occuring in Statement :  pi1: fst(t),  pi2: snd(t),  apply: f a
Definitions occuring in definition :  apply: f a,  pi2: snd(t),  pi1: fst(t)
FDL editor aliases :  cu-cube-restriction cu-cube-restriction
Latex:
cu-cube-restriction(alpha;L;J;f;a;T)  ==    (snd(fst(alpha)))  L  J  f  a  T


Date html generated: 2016_06_16-PM-08_07_27
Last ObjectModification: 2015_09_23-AM-09_35_05

Theory : cubical!sets


Home Index