Nuprl Definition : cubical-lambda

b) ==  λI,a,J,f,u. (b (f(a);u))



Wellformedness Lemmas :  cubical-lambda_wf
Definitions occuring in Statement :  cc-adjoin-cube: (v;u) cube-set-restriction: f(s) apply: a lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x] apply: a cc-adjoin-cube: (v;u) cube-set-restriction: f(s)
FDL editor aliases :  cubical-lambda

Latex:
(\mlambda{}b)  ==    \mlambda{}I,a,J,f,u.  (b  J  (f(a);u))



Date html generated: 2016_06_16-PM-05_43_04
Last ObjectModification: 2015_09_23-AM-09_30_42

Theory : cubical!sets


Home Index