From the previous proposition and Theorem REF , one can deduce
that, for dipaths between any two points which are realizations of vertices
of \(C\) , homotopy coincides with dihomotopy in \({C}\) . Variants of this
properties have been shown in the literature: in the case of geometric semantics
of “simple” programs with mutexes [1]}, in the case of cube
complexes [2]} (see also next section). A similar observation has
been made for spaces which are hypercontinuous lattices equipped with their
Lawson topology, such that their underlying space has connected CW
type [3]}. In that case also, increasing paths that are homotopic
are in fact dihomotopic.
