Nuprl Definition : path-eta
path-eta(pth) == (pth)p @ q
Definitions occuring in Statement :
cubicalpath-app: pth @ r,
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
cubicalpath-app: pth @ r,
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
path-eta
Latex:
path-eta(pth) == (pth)p @ q
Date html generated:
2016_06_16-PM-01_44_23
Last ObjectModification:
2016_06_07-AM-11_59_10
Theory : cubical!type!theory
Home
Index