Enriched categories

In a category enriched in $([0, \infty], \ge, +, 0)$, the hom-object from $x$ to $y$ is a number $d(x, y)$. What does the composition morphism $X(y, z) \otimes X(x, y) \to X(x, z)$ say?

Directed footpaths between four places take these times (minutes): $A \to B$: 4, $B \to C$: 3, $C \to D$: 5, $A \to C$: 9, $D \to A$: 2, $B \to D$: 10. In the free Lawvere metric space on this weighted graph (shortest-path distance), what is $d(A, D)$?

Replace $+$ by $\max$: let $\mathcal{V} = ([0, \infty], \ge, \max, 0)$. What is a $\mathcal{V}$-category?

Which statement about one-object enriched categories is correct?

The category with abelian groups as objects and all functions as morphisms has an abelian group $B^A$ of morphisms from $A$ to $B$ (pointwise addition). Why is it not an $\mathbf{Ab}$-enriched category?

Let $f, g : X \to Y$ be non-expansive maps between Lawvere metric spaces, viewed as $[0, \infty]$-functors. When is there a $[0, \infty]$-natural transformation $f \Rightarrow g$?

In the Lean file, Dist is the order dual of ℝ≥0∞, so a ⟶ b holds when a ≥ b as distances, and Mathlib writes the composition of an enriched category as comp x y z : Hom x y ⊗ Hom y z ⟶ Hom x z. In lawvereEquivEnriched, what does homOfLE (M.triangle x y z) provide?

Theorem 4 says $d(x, y) = \sup_z \big(d(z, y) \mathbin{\dot-} d(z, x)\big)$ in any Lawvere metric space. Which $z$ attains the supremum, and why is no term larger?

Write free_metric(w): given a square matrix w (list of lists) of direct path lengths, with 0 on the diagonal and float('inf') where there is no path, return the shortest-path distance matrix — the free Lawvere metric. Use repeated min-plus squaring $D \mapsto D \otimes D$, $(D \otimes D)_{ik} = \min_j (D_{ij} + D_{jk})$, until the matrix stops changing.