Nuprl Definition : dcff-inj

dcff-inj(I;w) ==  w I 1


Definitions occuring in Statement :  nh-id: 1,  apply: f a
Definitions occuring in definition :  nh-id: 1,  apply: f a
FDL editor aliases :  dcff-inj
Latex:
dcff-inj(I;w)  ==    w  I  1


Date html generated: 2016_07_09-PM-01_31_14
Last ObjectModification: 2016_07_09-PM-01_01_48

Theory : cubical!type!theory


Home Index