Nuprl Definition : singleton-contraction
singleton-contraction(X;pth) == <>(cubical-pair((pth)p @ q;path-contraction(X;pth)))
Definitions occuring in Statement :
path-contraction: path-contraction(X;pth),
term-to-path: <>(a),
cubical-path-app: pth @ r,
cubical-pair: cubical-pair(u;v),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s
Definitions occuring in definition :
path-contraction: path-contraction(X;pth),
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
cubical-path-app: pth @ r,
cubical-pair: cubical-pair(u;v),
term-to-path: <>(a)
FDL editor aliases :
singleton-contraction
Latex:
singleton-contraction(X;pth) == <>(cubical-pair((pth)p @ q;path-contraction(X;pth)))
Date html generated:
2017_01_10-AM-08_59_55
Last ObjectModification:
2016_12_01-PM-02_32_00
Theory : cubical!type!theory
Home
Index