  Substructural logics naturally support a quantitative interpretation of
formulas, as they are seen as consumable resources. Distances are the
quantitative counterpart of equivalence relations: they measure how much two
objects are similar, rather than just saying whether they are equivalent or
not. Hence, they provide the natural choice for modelling equality in a
substructural setting. In this paper, we develop this idea, using the
categorical language of Lawvere's doctrines. We work in a minimal fragment of
Linear Logic enriched by graded modalities, which are needed to write a
resource sensitive substitution rule for equality, enabling its quantitative
interpretation as a distance. We introduce both a deductive calculus and the
notion of Lipschitz doctrine to give it a sound and complete categorical
semantics. The study of 2-categorical properties of Lipschitz doctrines
provides us with a universal construction, which generates examples based for
instance on metric spaces and quantitative realisability. Finally, we show how
to smoothly extend our results to richer substructural logics, up to full
Linear Logic with quantifiers.
