Single-exponential mixed complexity conjecture for the semi-algebraic image functor

Let $\opcat{SA}$ be the category whose objects are embedded semi-algebraic sets and whose morphisms are restrictions of polynomial mappings. Let $\cA$ consist of scalar multiplication, addition, multiplication, the inclusion $[0,\infty)\hookrightarrow\mathbb{R}$, and the morphism $\mathbb{R}\to 0$. Write C_{c^{\op{mixed}}_{\opcat{SA}^{\raisebox{0.009cm}{\scalebox{0.5}{\bullet}} \to \raisebox{0.009cm}{\scalebox{0.5}{\bullet}}},\cA}}(\op{im}_{\opcat{SA}}) for the mixed computational complexity of the image functor on $\opcat{SA}$. Single-exponential mixed complexity conjecture. The function

$$C_{c^{\op{mixed}}_{\opcat{SA}^{\raisebox{0.009cm}{\scalebox{0.5}{$\bullet$}} \to \raisebox{0.009cm}{\scalebox{0.5}{$\bullet$}}},\cA}}(\op{im}_{\opcat{SA}})$$

is bounded singly exponentially. This is presented as a categorical analogue of the P versus NP question for semi-algebraic sets; the surrounding text says that mixed computation is more powerful than limit computation and that the authors are unable to resolve the corresponding polynomial-boundedness question, so the conjectured single-exponential bound remains open.