Nuprl Definition : path-trans
path-trans(G;p) == univ-trans(G;path-eta(p))
Definitions occuring in Statement :
univ-trans: univ-trans(G;T),
path-eta: path-eta(pth)
Definitions occuring in definition :
path-eta: path-eta(pth),
univ-trans: univ-trans(G;T)
FDL editor aliases :
path-trans
Latex:
path-trans(G;p) == univ-trans(G;path-eta(p))
Date html generated:
2017_01_10-PM-00_23_45
Last ObjectModification:
2017_01_02-AM-09_46_37
Theory : cubical!type!theory
Home
Index