Nuprl Definition : cube-

cube-(I;i) ==  λA,f. <f, f i>


Definitions occuring in Statement :  apply: f a,  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  lambda: λx.A[x],  pair: <a, b>,  apply: f a
FDL editor aliases :  cube-
Latex:
cube-(I;i)  ==    \mlambda{}A,f.  <f,  f  i>


Date html generated: 2016_05_19-AM-08_23_18
Last ObjectModification: 2016_03_21-AM-01_36_37

Theory : cubical!type!theory


Home Index