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