be directed, such that any constant path is directed, the concatenation of two directed paths is still directed, and any subpath of a directed path is directed. D-spaces admit non-constant directed loops and form a category enjoying properties similar to the ones enjoyed by the category of topological spaces. As shown by Sanjeevi Krishnan, the drawbacks of local pospaces can be avoided if we extend the notion of pospaces by means of 'cosheaves'. The notion of stream is defined thus. More precisely one considers preorders on open subsets and one requires that given any open subset U and any open covering Ω of U, the preorder associated with U is 'generated' by the preorders associated with each member of Ω. The resulting category behaves as nicely as the category of d-spaces. Indeed, both of them one can define the directed geometric realization of cubical set (simplicial set) so that its underlying topological space is the (usual) geometric realisation. In fact there is a natural embedding G of the category of streams into the category of d-spaces. This embedding admits a left adjoint functor F. The images of F and G are isomorphic, an isomorphism being obtained by restricting F and G to those images. The category of d-spaces can thus be seen as one of the most general formalisations of the intuitive notion of directed space. Directed homotopies between directed paths Regardless of the kind of directed space on considers (pospaces, local pospaces, d-spaces or streams) there is an obvious forgetful functor to the category of topological spaces. Given two directed paths γ and δ, a directed homotopy from γ to δ is a morphism of directed spaces h whose underlying map U(h) is a homotopy –in the usual sense– between the underlying paths U(γ) and U(δ). In algebraic topology, there is a homotopy from α to β if and only if there is a homotopy from β to α. Due to non-reversibility, this is no longer true for directed homotopies. As a consequence, we define the congruence as the least equivalence relation on the directed paths which is compatible with concatenation and relates γ to δ as soon as there is a directed homotopy from γ to δ. Going back to the computer science motivation where directed paths represent execution traces, directed homotopies provide a way to identify execution traces. Hence, given a directed space X which models some