Nuprl Definition : rev-path
rev-path(G;pth) == <>((pth)p @ 1-(q))
Definitions occuring in Statement :
term-to-path: <>(a),
cubicalpath-app: pth @ r,
interval-rev: 1-(r),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
term-to-path: <>(a),
cubicalpath-app: pth @ r,
csm-ap-term: (t)s,
cc-fst: p,
interval-rev: 1-(r),
cc-snd: q
FDL editor aliases :
rev-path
Latex:
rev-path(G;pth) == <>((pth)p @ 1-(q))
Date html generated:
2017_02_21-AM-10_38_40
Last ObjectModification:
2017_01_26-PM-02_02_01
Theory : cubical!type!theory
Home
Index