On the separation axiom in a Lawvere or "generalized" metric space According to the nLab, Lawvere metric spaces occur rather naturally (that is as certain enriched categories). A Lawvere metric space is a set $X$ equipped with a function $d : X\times X \to [0,\infty]$, such that:


*

*$d(x,x) = 0$

*$d(x,y) + d(y,z) \geq d(x,z)$


I don't have any background in enriched category theory, so can only see the theory of Lawvere metric spaces on an elementary level.
Omitting the separation axiom, that is:
$$d(x,y) = 0 \Rightarrow x = y$$
seems to cause some weird things. Consider the category of Lawvere metric spaces, where a morphism $f : X \to Y$ is a function such that:
$$d(x,y) \geq d(fx,fy)$$
It is well known, that if it also an isometry, then $f$ is injective. But it appears that for Lawvere metric spaces you cannot prove that every isometry is even mono in the category of Lawvere spaces. I can only show that these maps are "almost" injective in the sense that:
$$fx \cong fy \Rightarrow x \cong y$$
where $x\cong y \Leftrightarrow d(x,y) = d(y,x) = 0$.

How can I view this "situation" (of isometries being "almost" mono / injective), such that it seems natural instead of "weird" and unwanted? 

 A: I assume you are looking for some real world examples of pseudo-metric spaces (that correspond to what you call Lawvere-metric spaces).
Well a family of examples is given by the $\mathcal L^p$-spaces (where $p$ is real number in $[1,\infty]$).
In general for $(\Omega,\mathcal F, \mu)$ a measured space, we have the vector space $\mathcal L^p(\Omega)$ whose elements are measurable functions $f \colon \Omega \to \mathbb R$ such that 
$$\int |f(x)|^p d\mu(x) < \infty\ .$$
To be exact $\mathcal L^p(\Omega)$ is a sub-space of the vector space $\mathbb R^\Omega$ of the real valued function defined over $\Omega$.
What's more is that the mapping 
$$d \colon \mathcal L^p(\Omega)\times\mathcal L^p(\Omega) \to \mathbb [0,\infty)$$
defined by 
$$d(f,g) = \left(\int |f(x)-g(x)|^pd\mu(x)\right)^{\frac{1}{p}}$$
gives this space the structure of pseudo-metric space.
It is not a metric space because there are many functions in $\mathcal L^p(\Omega)$ that make null the integral 
$$\int |f(x)|^pd\mu(x)$$
while being not null. 
Of course one can quotient these spaces to obtain some metric spaces, nonetheless it is important to consider these spaces at some point if one what to establish precise results for the $L^p(\Omega)$ spaces: the spaces obtained by the $\mathcal L^p(\Omega)$ identifying functions whose distance is zero.
Take a look to the link above for more informations.
Edit: I see that my answer didn't address your real question, allow me to make amend.
Let $p$ be as above and let $p' \in [1,\infty]$ be the only number such that $\frac{1}{p}+\frac{1}{p'}=1$.
By $\mathcal L^{p'}(\Omega)^*$ we will denote the space of continuous linear functionals defined over the space $\mathcal L^{p'}(\Omega)$.
Results on $\mathcal L^p$-spaces ensure that there is a linear map 
$$i \colon \mathcal L^p(\Omega) \to \mathcal L^{p'}(\Omega)^*$$
defined as 
$$i(f)=g \mapsto \int f(x)g(x)d\mu(x)\ .$$
This map is an isometry in your sense, still it is pretty important. 
Again if you pass this isometry to the quotient spaces ($L^p(\Omega)$ and 
$L^{p'}(\Omega)^*$ respectively) the you get a real-isometry between metric-spaces.
Another example of this strange isometry is the projection to the quotient 
$$\mathcal L^p(\Omega) \to L^p(\Omega)$$
as pointed out by Kevin Carlson below in the comments. 
Hope this helps.
A: This is another example of "equivalence instead of equality".
Monic maps "ought" not be characterized by $f(x) = f(y) \implies x=y$: the right characterization ought to be $f(x) \cong f(y) \implies x \cong y$.
(note: the following was written around the symmetric version; where we further assume $d(x,y) = d(y,x)$. Without this assumption the details are more complex)

The right underlying collection of points here is not the set $X$: it is instead the setoid consisting of $X$ along with the equivalence relation that $x \sim y$ iff $d(x,y) = 0$.
This can be viewed as an ordinary category whose objects are the elements of $X$ and $\hom(x,y)$ has exactly one element if $x \sim y$, and is empty otherwise.
Every small setoid $S$ is equivalent to a set $S_s$ (e.g its set of equivalence classes), and the usual point is that working with $S$ should be basically the same thing as working with $S_s$, and so we need to adapt our definitions appropriately. ($S_s$ is not a standardized notation)
e.g. given a morphism $S \to T$, the corresponding morphism $S_s \to T_s$ is monic iff and only if the original morphism is a full functor (it will automatically be faithful). Consequently, the right notion of "monic map" between setoids is "full functor".
This agrees with the characterization given at the beginning.

Similarly, every Lawvere metric space $X$ is equivalent to one $X_s$ with the property that $d(x,y) = 0$ iff $x=y$. The same construction works: take the objects of $X_s$ to be the set of equivalence classes.
And just as for setoids, we need to adapt our notion of monic; it should be that $d(fx,fy)=0 \implies d(x,y)=0$.
A: Jean Goubeault-Larrecq has written a detailed textbook-level introduction to "Lawvere" metric spaces from a topological point of view in Chapter 6 of his book Non-Hausdorff Topology and Domain Theory. He defines a hemi-metric space to be a set $X$ equipped with a set-function $d\colon X\times X\to[0,\infty]$ such that


*

*$d(x,x)=0$

*$d(x,y)\leq d(x,z)+d(z,y)$


Recall that a topological space is satisfies the $T_0$ separation axiom, i.e., is Kolmogoroff, if and only if for any pair $x\neq y\in X$, there is an open $U$ so that either $x\in U,y\not\in Y$, or $x\not\in U,y\not\in U$. In other words, a topological space is Kolmogoroff if and only if points are "topologically distinguishable".
Any quasi-metric space $(X,d)$ has a topology with a basis given by open balls $B_{x,<\epsilon}^d=\{y\in X:d(x,y)<\epsilon\}$ for $\epsilon\in(0,\infty)$. A quasi-metric space $(X,d)$ is $T_0$ if and only if it satisfies


*$d(x,y)=0=d(y,x)\implies x=y$


in which case Goubeault-Larrecq calls it a quasi-metric space. If $(X,d)$ is a quasi-metric space and $(X',d)$ is a hemi-metric space, then isometric embeddings $(X,d)\to(X',d')$ are also topological embeddings. In other words, metric embeddings are topological embeddings if the topology associated topology to the domain distinguishes points. In fact, the converse holds because $d(x,y)=0=d(y,x)$ implies $d(x,z)\leq d(x,y)+d(y,z)=d(y,z)\leq d(y,x)+d(x,z)=d(x,z)$ and $d(z,x)\leq d(z,y)+d(y,x)=d(z,y)\leq d(z,x)+d(x,y)=d(z,x)$, hence the quotient $X\twoheadrightarrow X/\sim$ by the relation $x\sim y$ if $d(x,y)=0=d(y,x)$ is an isometry $(X,d)\to (X/\sim,d)$ from a hemi-metric space to its "quasi-metrication".

The above relationship between isometries and injections, and particularly why isometries are not always injections can be understood using the theory of topological categories. A quick reference is Section 11 of Oswald Wyler's Lecture Notes on Topoi and Quasitopoi; a more detailed treatment can be found in The Joy of Cats. What I'm writing below is an example application of the theory to hemi-metric spaces.
Consider the category $\mathcal Hem$ of hemi-metric spaces and $1$-Lipschitz functions between them, i.e. functions $(X,d)\xrightarrow{f}(X',d')$ such that $d'(f(x),f(y))\leq d(x,y)$. 


*

*The forgetful functor $\mathcal Set\xleftarrow{U}\mathcal Hem$ is faithful, that is, injective on morphisms, hence establishes establishes $\mathcal Hem$ as a concrete category.

*$U$ is transportable in the sense that for any bijection $X\overset f\cong X'$ and a hemi-metric structure $(X',d')$ there exists a unique hemi-metric structure $(X,d)$ with $(X,d)\overset f\cong (X',d')$ an isomorphism in $\mathcal Hem$. This is the categorical version of the statement that if $f$ is an isomorphism in $\mathcal Hem$, then $f$ is an isometry.

*Given a collection of hemi-metric spaces $(X'_i,d'_i)$ and a collection of set functions $X\xrightarrow{f_i}X'_i$ (i.e. a source for $\mathcal Set\xleftarrow{U}\mathcal Hem$), the hemi-metric structure $(X,d)$ given by $d(x,y)=\sup_id_i'(f_i(x),f_i(y))$ is an initial lift in the sense that a set function $X''\xrightarrow{g}X$ is $1$-Lipschitz for $(X'',d'')\xrightarrow{g}(X,d)$ if and only if each $(X'',d'')\xrightarrow{f_i\circ g}(X',d')$ is $1$-Lipschitz. Indeed $d'(f_i(g(x''),f_i(g(y''))\leq d''(x'',y''))$ for each $i$ if and only if $d(g(x''),g(y''))\leq d''(x'',y'')$. You should think of this as analogous to having a weakest topology on a set so that a certain collection of set functions to topological spaces will be continuous.

*Given a collection of hemi-metric spaces $(X_i,d_i)$ and a collection of set functions $X_i\xrightarrow{g_i}X'$ (i.e. a sink for $\mathcal Set\xleftarrow{U}\mathcal Hem$), consider the source consisting of all set-functions $X'\xrightarrow{f_j}(X''_j,d''_j)$ such that $(X_i,d_i)\xrightarrow{f_j\circ g_i}(X''_j,d''_j)$ is $1$-Lipschitz for each $i$. The initial lift $(X',d')$ of this source given by $d'(x',y')=\sup_jd''_j(f_j(x'),f_j(y'))$ is also a final lift of the sink under consideration. This is an analog of the strongest topology on a set so that a certain collection of set functions from topological spaces will be continuous. Note that the best explicit computation of the hemi-metric of the final lift is the inequality $d'(x',y')\leq\inf_{i,x,y:g_i(x)=x',g_i(y)=y'}d_i(x,y)$. 
Since $\mathcal Set\xleftarrow{U}\mathcal Hem$ is faithful, transportable, and has initial lifts of all sources, it gives $\mathcal Hem$ the structure of a topological category over $\mathcal Set$. Given a set $X$, the initial lift $(X,d)$ of the empty source from $X$ is the indiscrete or trivial hemi-metric space given by $d(x,y)=0$: any set-function from a hemi-metric space to the trivial space is $1$-Lipschitz. Dually, the final lift $(X,d)$ of the empty sink to $X$ is the discrete hemi-metric space given by $d(x,y)=\begin{cases}\infty&x\neq y\\0&x=y\end{cases}$: any set-function out of it to a hemi-metric space is $1$-Lipschitz.
We therefore have explicit discrete and trivial functors $D,T\colon \mathcal Set\to\mathcal Hem$ which are by definition the left and right adjoints to the forgetful functor $\mathcal Set\xleftarrow{U}\mathcal Hem$, i.e. $D\dashv U\dashv T$. Since $U$ is faithful, it follows that a $1$-Lipschitz function is a monomorphism (resp. epimorphism) in $\mathcal Hem$ if and only if it is a monomorphism (resp. epimorphism) in $\mathcal Set$, i.e. if and only if it is injective or surjective.
Furthermore, a $1$-Lipschitz function $(X,d)\xrightarrow{f}(X',d')$ is a strong monomorphism (i.e an embedding) if and only if the set function $X\xrightarrow{f}X'$ is a strong monomorphism and $(X,d)\xrightarrow{f}(X',d')$ is coarse in the sense that $(X,d)$ is the initial lift for the source $X\xrightarrow{f}X'$. Since all injective functions in $\mathcal Set$ are strong monomorphisms, the first condition is just the requirement that $(X,d)\xrightarrow{f}(X',d')$ be injective, while the second requirement is that $d(x,y)=d(f(x),f(y))$, i.e. that $f$ is an isometry.
Thus one way to answer your question is to say that in a topological category over $\mathcal Set$, coarse maps do not have to be embeddings. The analogy with $\mathcal Top$ is that a continuous map $X\xrightarrow{f} Y$ is a topological embedding if and only if it is injective and $X$ has the weakest topology for which $f$ is continuous (if $f$ is injective, this is the subspace topology). A $1$-Lipschitz map $(X,d)\xrightarrow{f}(X',d')$ is thus an isometry if $(X,d)$ has the "weakest" hemi-metric for which $(X,d)\xrightarrow{f}(X',d')$ is $1$-Lipschitz map; being injective is a completely separate condition.

The $T_0$ separation axiom comes into play not from the isometries, i.e from the coarse morphisms but from "computable" "co-isometries". 
Dual to the previous result, a $1$-Lipschitz function $(X,d)\xrightarrow{f}(X',d')$ is a quotient in $\mathcal Hem$, i.e. a strong epimorphism, if and only if the set-function $X\xrightarrow{f}X'$ is a strong epimorphism and $(X,d)\xrightarrow{f}(X',d')$ is fine, i.e. $(X',d')$ is the final lift of the sink $X\xrightarrow{f}X'$. Since every epimorphism in $\mathcal Set$ is strong, the first condition just says that $X\xrightarrow{f}X'$ is surjective, but the second condition remains in general uncomputable because at best we can say $d'(x',y')\leq\inf_{x,y: f(x)=x',f(y)=y'}d(x,y)$.
Let's say a fine morphism $(X,d)\xrightarrow{f}(X',d')$ is computably fine if equality holds, i.e. $d'(x',y')=\begin{cases}0&x'=y'\\\inf_{x,y: f(x)=x',f(y)=y'}d(x,y)&x'\neq y'\end{cases}$. Then a function $X\xrightarrow{f}X'$ to a hemi-metric space $(X',d')$ has a computably fine lift if and only if $\inf_{x,y: f(x)=x',f(y)=y'}d(x,y)$ satisfies the triangle inequality.
But the triangle inequality fails if and only if there exist $x_0,y_0,z_1,z_2\in X$ with $f(z_1)=f(z_2)$ and $\inf_{x,y: f(x)=f(x_0),f(y)=f(y_0)}d(x,y)>d(x_0,z_1)+d(z_2,y_0)$. On the other hand, we always have $d(x,y)\leq d(x,x_0)+d(x_0,z_1)+d(z_1,z_2)+d(z_2,y_0)+d(y_0,y)$.
To prevent the failure of the triangle inequality, it is sufficient to require that $f(z_1)=f(z_2)$ implies $d(z_1,z_2)=0$ (which by symmetry of $f(z_1)=f(z_2)$ also implies $d(z_2,z_1)=0$). I think this condition is equivalent to the condition that the associated topology to $(X',d')$ is the strongest topology that makes $X\xrightarrow{f}X'$ continuous from $X$ equipped with the open ball topology of $(X,d)$, hence I'll call such Lipschitz functions $(X,d)\xrightarrow{f}(X',d')$ topologically fine.
Accordingly, we have an explicit class of strong epimorphisms in $\mathcal Hem$ given by those surjective $(X,d)\xrightarrow{f} (X',d')$ such that $f(x)=f(y)\implies d(x,y)=0=d(y,x)$ (i.e. quotients by some amount of topological indistinguishability) and $d'(x',y')=\inf_{x,y:f(x)=x',f(y)=y'}d(x,y)$ (hence topologically fine quotients in $\mathcal Hem$).
This class is the left class in an orthogonal factorization system whose right class are those morphisms such that $x\neq y\wedge f(x)=f(y)\implies\neg(d(x,y)=0=d(y,x))$. This means that any $1$-Lipshitz function $(X,d)\to(X',d')$ factors uniquely (up to isomorphism) as $(X,d)\to (X'',d'')\to (X',d')$ where the first map is in the left class and the second in the right class, and furthermore in a commutative square
$$\require{AMScd}\begin{CD}
W @>f>> Y\\
@VLVV @VRVV\\
X @>g>> Z
\end{CD}$$
there is a unique diagonal morphism $X\to Y$ factoring $g$ through $R$ and $f$ through $L$. Indeed, $W\xrightarrow{L}X$ is a quotient, and $L(w_1)=L(w_2)$ implies $d(w_1,w_2)=0=d(w_2,w_1)$ and $R\circ f(w_1)=g\circ L(w_1)=g\circ L(w_2)=R\circ f(w_2)$. The first and $f$ being $1$-Lipschitz gives $d(f(w_1),f(w_2))=0=d(f(w_2),f(w_1))$, hence $f(w_1)=f(w_2)$ by the second and the condition on the right class. Since morphisms in $L$ are fine in $\class Hem$, the diagonal maps itself is $1$-Lipschitz.
Note that the orthogonal factorization system is not a strong epi-mono factorization system because the right class of morphisms does not consist of injective functions -- but note that this lack of injectivity is never because topologically indistinguishable points are getting collapsed. It follows that the factorization of a morphism $(X,d)\to (X',d')$ where $X',d')$ is a quasi-metric space is exactly the unique factorization through the quasi-metrication of the hemi-metric space.

Note that symmetry is not used anywhere; a hemi-metric space $(X,d)$ satisfies the stronger condition


*$d(x,y)=0\implies x=y$


if and only if the associated topological space satisfies the $T_1$ separation axiom: for any pair $x\neq y\in X$, there is an open $U$ so that $x\in U,y\not\in Y$.
