Nuprl Definition : map-path
map-path(G;f;pth) == <>(app((f)p; path-eta(pth)))
Definitions occuring in Statement :
term-to-path: <>(a),
path-eta: path-eta(pth),
cubical-app: app(w; u),
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
term-to-path: <>(a),
cubical-app: app(w; u),
csm-ap-term: (t)s,
cc-fst: p,
path-eta: path-eta(pth)
FDL editor aliases :
map-path
Latex:
map-path(G;f;pth) == <>(app((f)p; path-eta(pth)))
Date html generated:
2018_05_23-AM-09_37_06
Last ObjectModification:
2017_11_07-PM-02_05_00
Theory : cubical!type!theory
Home
Index