Example 6.1

Let $V$ be a type in universe $u$, equipped with a topology, a commutative additive group structure, and a real module structure. Assume that its topology is compactly generated with respect to compact Hausdorff spaces in universe $u$, meaning that a subset of $V$ is open exactly when its inverse image under every continuous map from such a space is open. Assume also that addition $(x,y)\mapsto x+y$ is continuous from $k(V\times V)$ to $V$, negation $x\mapsto -x$ is continuous on $V$, and scalar multiplication $(r,x)\mapsto r\mathbin{\cdot}x$ is continuous from $k(\mathbb R\times V)$ to $V$. Here $kZ$ denotes the same underlying set as the indicated product space $Z$, with subsets declared open exactly when their inverse images under all continuous compact Hausdorff probes in universe $u$ into $Z$ are open. Then the function $\phi(x,t)=t\mathbin{\cdot}x$, for real $t\in[0,1]$, is continuous from $k(V\times[0,1])$ to $V$ and satisfies $\phi(x,0)=0$, $\phi(x,1)=x$, and $\phi(x+y,t)=\phi(x,t)+\phi(y,t)$ for every $x,y\in V$ and $t\in[0,1]$.