In his lecture, The Categorical Origins of Lebesgue Measure, Professor Tom Leinster mentions the following theorem:
Theorem 1: (Freyd; Leinster) The topological space $[0, 1]$ comes equipped with two distinct basepoints $0$ and $1$, and a map $[0, 1] \rightarrow [0, 1] \amalg [0, 1] / \text{first }1 \sim \text{second } 0$. $[0, 1]$ is terminal as such.
Leinster's theorem is about a universal property of the banach space $L^1 [0, 1]$ and the integration function $\int : L^1 [0, 1] \rightarrow \mathbb{R}$. It goes like this: let $\mathcal{A}$ be the category of Banach spaces, whose objects are banach spaces and whose maps are maps $\phi : X \rightarrow Y$ of banach spaces such that $||\phi(x)|| \leq ||x||$. Let $\mathcal{A}/\mathbb{R}$ be the under-category (objects are maps $\mathbb{R} \rightarrow X$ in $\mathcal{A}$; this is also called the coslice category). There is a functor $T : \mathcal{A} \rightarrow \mathcal{A}$ defined where $T(X) = X \prod X$, where $X$ has measure $||(x, y)|| = \frac{1}{2} (||x|| + ||y||)$ with corresponding map $\mathbb{R} \rightarrow X \prod X$ induced canonically by the map $\mathbb{R} \rightarrow X$. The initial $T$-algebra is $$L^1 [0, 1] = \frac{\text{Lebesgue-integrable functions } [0, 1] \rightarrow \mathbb{R} }{\text{equality almost everywhere}}$$ Note: we can still form $T$-algebras when $T$ is not a monad.
The unique map $\int : L^1 [0, 1] \rightarrow \mathbb{R}$ comes from the universal property now!
My question is this:
Can we rearrange theorem 1 above in terms of continuous functions $C([0, 1]) = [[0, 1], \mathbb{R}]_{\text{Top}}$ and an endofunctor $T$ where $T(A) = A \prod A$, just like in the measure theory case?
From a categorical perspective, this might be nice since we would no longer have to require two distinct points in the topological space.
So the rearrangement of Professor Leinster's theorem would go like this:
Let $\mathcal{B}$ be the category of topological vector spaces (some tweaking might be necessary, maybe topological algebras would be better? Maybe the Lawvere theory of $C^0$-algebras?). Let $\mathcal{B}/\mathbb{R}$ be the under-category (objects are maps $\mathbb{R} \rightarrow X$ in $\mathcal{B}$). There is a functor $T : \mathcal{B} \rightarrow \mathcal{B}$, where $T(X) = X \prod X$, just as before. Perhaps the initial $T$-algebra is $C([0, 1])$!
Now that I think about it, if measure theory and topology have their own versions of this theorem, maybe there is one for differential geometry and $C^{\infty}$-algebras. Just a thought.