Nuprl Definition : path-term

path-term(phi;w;a;b;r) ==  (w @ r ∨ (a ∨ b))


Definitions occuring in Statement :  cubical-path-app: pth @ r,  case-term: (u ∨ v),  face-zero: (i=0)
Definitions occuring in definition :  face-zero: (i=0),  case-term: (u ∨ v),  cubical-path-app: pth @ r
FDL editor aliases :  path-term
Latex:
path-term(phi;w;a;b;r)  ==    (w  @  r  \mvee{}  (a  \mvee{}  b))


Date html generated: 2016_06_16-PM-02_16_51
Last ObjectModification: 2016_06_09-AM-11_53_27

Theory : cubical!type!theory


Home Index