Nuprl Definition : contractible-comp

contractible-comp(X;A;cA) == cfun-to-cop(X;Contractible(A);contractible_comp(X;A;cop-to-cfun(cA)))

Definitions occuring in Statement : contractible_comp: contractible_comp(X;A;cA), comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp), comp-op-to-comp-fun: cop-to-cfun(cA), contractible-type: Contractible(A)
Definitions occuring in definition : comp-op-to-comp-fun: cop-to-cfun(cA), contractible_comp: contractible_comp(X;A;cA), contractible-type: Contractible(A), comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp)
FDL editor aliases : contractible-comp

Latex:
contractible-comp(X;A;cA) == cfun-to-cop(X;Contractible(A);contractible\_comp(X;A;cop-to-cfun(cA))) Date html generated: 2017_01_10-AM-10_10_59 Last ObjectModification: 2016_12_24-AM-11_46_18 Theory : cubical!type!theory Home Index