Homotopy type theory (HoTT) doesn't seem to say anything about "mutations" of values in type $T$, an important concept in computer science. Mutations occur when you "change a value" of some variable $x\in T$; e.g. from $x=5$ to $x=6$. Is it possible to extend the notion of homotopy type (in the sense of HoTT) to allow for mutations? Perhaps each mutation is a path in some space, and the HoTT notion of 'identity' is given by the "cost-free" paths?

Let ${\mathbb R}_+=\{x\in{\mathbb R}\;|\;x\geq 0\}\cup\{\infty\}$ be the monoid of extended nonnegative real numbers ('numbers'), with the additive monoid structure (e.g. $0+x=x$, and $x+\infty=\infty$). Suppose $X$ is a topological space equipped with a function $Cost\colon Path(X)\to{\mathbb R}_+$, which I'll call the *cost function*, from its set of paths $Path(X)=\text{Hom}_{Top}([0,1],X)$, to the monoid of numbers, such that

- constant paths have cost $0$, and
- the cost of a concatenation of paths is the sum of their costs (i.e. $Cost(P\star Q)=Cost(P)+Cost(Q)$).

Note that this notion is not homotopical because we do not require that homotopic paths have equal costs. However, we can construct the *cost-free* subspace $X_0$ of $X$, given by the union of all paths $P$ with $Cost(P)=Cost(-P)=0$. For a path $P$, let $-P$ denote its composition with $(r\mapsto 1-r)\colon [0,1]\to[0,1]$. Then we construct the space $X_0$ and a continuous map $i_X\colon X_0\to X$ as follows:
$$X_0=\text {colim}_{\{P\colon [0,1]\to X\;|\;Cost(P)=Cost(-P)=0\}}\;(P)\hspace{.5in}i_X(P,r)=P(r),\;\; r\in [0,1].$$
Note that the subset $X_0\subseteq X$, constructed using the above colimit, will not always have the subspace topology inherited from $X$. However, there is a pretty general subcategory of "path-generated spaces" $X$, i.e. where open sets are detected by paths, for which it will. Regardless, the paths in $X_0$ form a groupoid.

Let's define a *mutation space* to be a pair $(X,Cost)$ as above, where $X$ a path-generated space. A * mutation* in $(X,Cost)$ is a path in $X$, and the *underlying HoTT homotopy type* of $(X,Cost)$ is $X_0$, the subspace generated by cost-free mutations. There are many reasonable notions for morphism of mutation spaces, e.g. continuous maps $f\colon X\to Y$ such that for any path $P\colon[0,1]\to X$, we have $Cost_Y(P\circ f)\leq Cost_X(P)$, under which the mutation spaces would form a category $MuSp$. But any good notion for this category should admit a "cost-free subspace" functor $(-)_0\colon MuSp\to Top$.

My question is especially directed to those with background in HoTT and CS:

Q1: is there anything flawed about the idea "mutations are paths and 'identities' are cost-free paths"?

Q2: is there any work being done on this kind of HoTT generalization, or on anything like it?

goingin defining the space $X_0$. Would you still apply this construction if weights were generalized to be maps of an arbitrary category, rather than elements of a monoid? $\endgroup$ – Noam Zeilberger Nov 8 '13 at 17:299more comments