Nuprl Definition : path-elim
path-elim(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-elim
Latex:
path-elim(pth) == (pth)p @ q
Date html generated:
2016_06_16-PM-01_44_40
Last ObjectModification:
2016_06_06-PM-10_04_10
Theory : cubical!type!theory
Home
Index