Nuprl Definition : equiv-contr

equiv-contr(f;a) ==  app(f.2; a)


Definitions occuring in Statement :  cubical-snd: p.2,  cubical-app: app(w; u)
Definitions occuring in definition :  cubical-app: app(w; u),  cubical-snd: p.2
FDL editor aliases :  equiv-contr equiv-contr
Latex:
equiv-contr(f;a)  ==    app(f.2;  a)


Date html generated: 2016_06_16-PM-01_57_04
Last ObjectModification: 2016_06_03-PM-02_11_43

Theory : cubical!type!theory


Home Index