Nuprl Definition : cube-set-restriction
f(s) ==  (snd(X)) I J f s
Definitions occuring in Statement : 
pi2: snd(t)
, 
apply: f a
Definitions occuring in definition : 
apply: f a
, 
pi2: snd(t)
FDL editor aliases : 
cube-set-restriction
cube-set-restriction
Latex:
f(s)  ==    (snd(X))  I  J  f  s
Date html generated:
2016_05_18-PM-00_06_21
Last ObjectModification:
2015_10_28-PM-01_13_46
Theory : cubical!type!theory
Home
Index