Nuprl Definition : cubical-subst
cubical-subst(G;f;pth;x) == app(PathTransport(map-path(G;f;pth)); x)
Definitions occuring in Statement :
path-trans: PathTransport(p),
map-path: map-path(G;f;pth),
cubical-app: app(w; u)
Definitions occuring in definition :
cubical-app: app(w; u),
path-trans: PathTransport(p),
map-path: map-path(G;f;pth)
FDL editor aliases :
cubical-subst
Latex:
cubical-subst(G;f;pth;x) == app(PathTransport(map-path(G;f;pth)); x)
Date html generated:
2018_05_23-PM-01_57_34
Last ObjectModification:
2017_11_22-AM-10_43_42
Theory : cubical!type!theory
Home
Index