Dicovering spaces

For a local po-space X and a base point x₀ ∈ X, we define the universal dicovering space Π: X̃_x0 → X. The image of Π is the future ↑ x₀ of x₀ in X and X̃_x0 is a local po-space such that |π^→ ₁ (X̃, [x₀], x₁)| = 1 for the constant dipath [x₀] ∈ Π^-1(x₀) and x₁ ∈ X̃_x0. Moreover, dipaths and dihomotopies of dipaths (with a fixed starting point) in ↑ x₀ lift uniquely to X̃_x0. The fibers Π^-1(x) are discrete, but the cardinality is not constant. We define dicoverings P: X̂ → X _x0 and construct a map φ: X̃_x0 → X̂ covering the identity map. Dipaths and dihomotopies in X̂ lift to X̃_x0, but we give an example where φ is not continuous.