Nuprl Definition : path-point
path-point(pth) == (pth)p @ q
Definitions occuring in Statement :
cubical-path-app: pth @ r,
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
cubical-path-app: pth @ r
FDL editor aliases :
path-point
Latex:
path-point(pth) == (pth)p @ q
Date html generated:
2017_01_10-AM-08_58_12
Last ObjectModification:
2016_12_01-PM-03_48_13
Theory : cubical!type!theory
Home
Index