Nuprl Definition : contractible_comp
contractible_comp(X;A;cA) == sigma_comp(cA;pi_comp(X.A;(A)p;(cA)p;path_comp(X.A.(A)p;((A)p)p;(q)p;q;((cA)p)p)))
Definitions occuring in Statement :
path_comp: path_comp,
pi_comp: pi_comp(X;A;cA;cB),
sigma_comp: sigma_comp(cA;cB),
csm-comp-structure: (cA)tau,
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 :
cc-fst: p,
cube-context-adjoin: X.A,
csm-comp-structure: (cA)tau,
csm-ap-type: (AF)s,
cc-snd: q,
csm-ap-term: (t)s,
path_comp: path_comp,
pi_comp: pi_comp(X;A;cA;cB),
sigma_comp: sigma_comp(cA;cB)
FDL editor aliases :
contractible_comp
Latex:
contractible\_comp(X;A;cA) ==
sigma\_comp(cA;pi\_comp(X.A;(A)p;(cA)p;path\_comp(X.A.(A)p;((A)p)p;(q)p;q;
((cA)p)p)))
Date html generated:
2017_01_10-AM-10_10_17
Last ObjectModification:
2016_12_24-AM-11_22_50
Theory : cubical!type!theory
Home
Index