Nuprl Definition : path-contraction
path-contraction(X;pth) == <>(((pth)p)p @ (q)p ∧ q)
Definitions occuring in Statement :
term-to-path: <>(a),
cubical-path-app: pth @ r,
interval-meet: r ∧ s,
interval-type: 𝕀,
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s
Definitions occuring in definition :
cc-snd: q,
cc-fst: p,
csm-ap-term: (t)s,
interval-meet: r ∧ s,
cubical-path-app: pth @ r,
interval-type: 𝕀,
cube-context-adjoin: X.A,
term-to-path: <>(a)
FDL editor aliases :
path-contraction
Latex:
path-contraction(X;pth) == <>(((pth)p)p @ (q)p \mwedge{} q)
Date html generated:
2017_01_10-AM-08_58_55
Last ObjectModification:
2016_12_01-PM-00_41_44
Theory : cubical!type!theory
Home
Index