Nuprl Definition : cubical-id-fun

cubical-id-fun(X) ==  cubical-lam(X;q)


Definitions occuring in Statement :  cubical-lam: cubical-lam(X;b),  cc-snd: q
Definitions occuring in definition :  cc-snd: q,  cubical-lam: cubical-lam(X;b)
FDL editor aliases :  cubical-id-fun
Latex:
cubical-id-fun(X)  ==    cubical-lam(X;q)


Date html generated: 2017_01_09-AM-09_16_08
Last ObjectModification: 2016_11_30-PM-05_04_23

Theory : cubical!type!theory


Home Index