Nuprl Definition : contr-path

contr-path(c;x) ==  app(c.2; x)


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 :  contr-path contr-path
Latex:
contr-path(c;x)  ==    app(c.2;  x)


Date html generated: 2016_06_16-PM-01_52_01
Last ObjectModification: 2016_06_03-PM-02_07_29

Theory : cubical!type!theory


Home Index