Nuprl Definition : contractible-to-prop
contractible-to-prop(X;A;cA;c) == (λ(λrev-path(X.A.(A)p;contr-path(((c)p)p;(q)p)) + contr-path(((c)p)p;q)))
Definitions occuring in Statement :
comp-path: pth_a_b + pth_b_c,
csm-comp-structure: (cA)tau,
contr-path: contr-path(c;x),
rev-path: rev-path(G;pth),
cubical-lambda: (λb),
cc-snd: q,
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s
Definitions occuring in definition :
cubical-lambda: (λb),
comp-path: pth_a_b + pth_b_c,
csm-comp-structure: (cA)tau,
rev-path: rev-path(G;pth),
cube-context-adjoin: X.A,
csm-ap-type: (AF)s,
contr-path: contr-path(c;x),
csm-ap-term: (t)s,
cc-fst: p,
cc-snd: q
FDL editor aliases :
contractible-to-prop
Latex:
contractible-to-prop(X;A;cA;c) ==
(\mlambda{}(\mlambda{}rev-path(X.A.(A)p;contr-path(((c)p)p;(q)p)) + contr-path(((c)p)p;q)))
Date html generated:
2017_02_21-AM-10_54_16
Last ObjectModification:
2017_01_26-PM-03_09_55
Theory : cubical!type!theory
Home
Index