# Quantitative Equality in Substructural Logic via Lipschitz doctrines

Francesco Dagnino  DIBRIS, Università di Genova, Italy
<EMAIL_ADDRESS>and  Fabio Pasquali  DIMA, Università di
Genova, Italy<EMAIL_ADDRESS>
###### Abstract.

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.

###### Key words and phrases:

hyperdoctrines, graded modalities, linear logic, quantitative reasoning

##  1\. Introduction

Equality is probably the most elementary and non-trivial predicate one can
consider in logic. It enables a very basic task, that is, reasoning about the
identity of expressions and thus of the objects they denote. Equality in First
Order Logic is nowadays fairly well understood from both a syntactic and a
semantic perspective. On the syntactic side, equality can be described as a
binary predicate $t\eqcirc u$, relating two terms $t$ and $u$, which has to
satisfy a couple of properties: every term has to be equal to itself
(_reflexivity_) and, whenever we know that $t$ and $u$ are equal and a formula
$\phi$ holds on $t$, then it holds on $u$ as well (_substitutivity_). In other
words, the former establishes that some trivial identities always hold, while
the latter allows to _transport_ a property $\phi$ from $t$ to $u$ when they
are equal; indeed, substitutivity is also known as the transport property of
equality. More formally, the equality predicate has to satisfy the following
entailments:

${\top}\vdash{t\eqcirc t}\qquad\qquad{\phi[t/x]\mathbin{\&}t\eqcirc
u}\vdash{\phi[u/x]}$

where $\top$ is the true predicate, $\mathbin{\&}$ is the conjunction and
$\phi[t/x]$ denotes the substitution of the term $t$ for the variable $x$ in
the formula $\phi$.

A simple semantic counterpart of the above description of equality is given by
_equivalence relations_. Indeed, considering a set $X$ of objects/individuals
one is interested in, a property/formula on $X$ can be seen as a function
${{\alpha}}:{{X}}\rightarrow{{\\{0,1\\}}}$, which says, for each object $x$ in
$X$, whether or not it has the property $\alpha$. Then, equality can be safely
modelled by an equivalence relation on $X$, namely, a binary function
${{\rho}}:{{X\times X}}\rightarrow{{\\{0,1\\}}}$ enjoying the usual
reflexivity, symmetry and transitivity properties, provided that formulas are
modelled by those $\alpha$ compatible with $\rho$. That is, if $x$ and $y$ are
equivalent according to $\rho$ (i.e. $\rho(x,y)=1$), then either both satisfy
$\alpha$ or both do not (i.e. $\alpha(x)=\alpha(y)$).

The understanding of equality becomes much less clear when moving to
_substructural_ logics, such as, (fragments of) Linear Logic [Gir87]. The core
idea of these logics is to see formulas as consumable resources in a proof,
which therefore cannot be freely deleted or duplicated. To achieve this, some
structural rules of usual deductive calculi are removed, specifically
weakening and contraction rules, which are precisely those enabling deletion
and duplication of formulas. As a consequence, usual true $\top$ and
conjunction $\mathbin{\&}$ are replaced by $\mathbf{1}$ and $\otimes$,
respectively, which behaves just as monoid-like operations (in particular,
$\otimes$ is not idempotent and $\mathbf{1}$ is not a top element).

Even though the model sketched above cannot work in general for the
substructural case, since it obviously validates both weakening and
contraction, from a semantic perspective, we can still have a quite natural
understanding of equality, by taking a _quantitative_ point of view.
Intuitively, a quantitative semantics measures how much a property holds
rather than just saying whether it holds or not. As a paradigmatic example,
let us model a quantitative property on a set $X$ by a function
${{\alpha}}:{{X}}\rightarrow{{[0,\infty]}}$ taking values in the set of
extended non-negative real numbers (usually considered with the reversed
order). Intuitively, the value $\alpha(x)=\epsilon$ means that $x$ has the
property $\alpha$ up to an error $\epsilon$, hence $\alpha$ surely holds on
$x$ when $\alpha(x)=0$. Following this intuitive reading of quantitative
properties, conjunction is given by the pointwise extension of addition of
real numbers, which, being non-idempotent, is capable to properly propagate
errors. In this setting, the natural generalisation of equivalence relations
are _distances_ , that is, binary functions ${{\rho}}:{{X\times
X}}\rightarrow{{[0,\infty]}}$ satisfying a quantitative version of
reflexivity, symmetry and transitivity:

$0\geq\rho(x,x)\qquad\rho(x,y)\geq\rho(y,x)\qquad\rho(x,y)+\rho(y,z)\geq\rho(x,z)$

Note that the quantitative transitivity property is nothing but the usual
triangular inequality.

Now the question is: how can we introduce equality in substructural logics so
that this quantitative semantics is supported? A first naive attempt could be
to take the linear version of equality rules in First Order Logic, introducing
a binary predicate $t\eqcirc u$ which satisfies the linear reflexivity and
substitutivity properties written below:

${\mathbf{1}}\vdash{t\eqcirc t}\qquad\qquad{\phi[t/x]\otimes t\eqcirc
u}\vdash{\phi[u/x]}$

These entailments are precisely the usual ones where standard connectives
$\top$ and $\mathbin{\&}$ are replaced by their linear version $\mathbf{1}$
and $\otimes$. However smooth, this approach raises the unexpected issue that
the equality predicate can be used an arbitrary number of times. Indeed, as
already observed in [Doz96], the following entailments are provable from the
two properties above:

${t\eqcirc u}\vdash{\mathbf{1}}\qquad\qquad{t\eqcirc u}\vdash{(t\eqcirc
u)\otimes(t\eqcirc u)}$

The former says that equality can be deleted, while the latter that it can be
duplicated. In other words, this shows that weakening and contraction rules,
which in general are banned from substructural logics, are instead admissible
for equality. This fact is undesirable per sé in a substructural setting, as
it is against its goal of controlling the use of formulas, but it is even
worse from the semantic perspective, as the quantitative interpretation of
equality is broken. Indeed, given a distance ${{\rho}}:{{X\times
X}}\rightarrow{{[0,\infty]}}$ interpreting equality, the second entailment
above forces it to satisfy the inequality $\rho(x,y)\geq\rho(x,y)+\rho(x,y)$,
which is true only when $\rho(x,y)$ is either $0$ or $\infty$. This means that
$\rho$ is, de facto, an equivalence relation.

In this paper we design a novel approach to equality in substructural logic,
which is capable to preserve its natural quantitative interpretation as a
(non-trivial) distance. On the one hand, this treatment of equality, enabling
more control on its usage, is more in the spirit of substructural logics and,
on the other, it could also shade a new light on the connection between such
logics and _quantitative reasoning_ , defining a set of formal tools
supporting it. Indeed, quantitative methods are increasingly used in many
different domains, such as differential privacy [RP10, BKOB13, XCL14, BGHP16],
denotational semantics [BM94, dAGH+17], program/behavioural metrics [DGJP04,
vBW05, CGPX14, Gav18, DGY19, DG22], and rewriting [GF22]. With respect to
usual techniques, quantitative methods better cope with the imprecision
arising when one reasons about the behaviour of complex software systems also
interacting with physical processes. The main formal system supporting these
techniques is Quantitative Equational Logic, introduced and developed by
Mardare et al. [MPP16, MPP17, MPP21, Adá22, BMPP18]. This is a logical system
with all structural rules, specifically designed to reason about real-valued
metrics, using ad-hoc symbols representing approximations of such metrics.
Nevertheless, quantitative methods are also naturally connected to
substructural logics, however, such a connection is still less explored hence
we plan to investigate it systematically, developing both syntax and
(categorical) semantics of a (minimal) substructural logic with _quantitative
equality_.

Our analysis starts by observing that, in analogy with what happens in the
specific case of program metrics [CD17, Gav18], the usual substitutive
property is not resource sensitive as it does not take into account resources
needed to perform the substitution: the equality $t\eqcirc u$ has to be
substitutive _for any_ formula $\phi$, while the “cost” of substituting $t$ by
$u$ may be different for different formulas, since, for instance, it may
depend on the number of occurrences of $t$. Hence, we need to rephrase the
substitutive property to explicitly consider such resources. To this end, we
work in (a fragment of) Linear Logic enriched with _graded modalities_ [BP15].
Roughly, one adds to the logic a family of unary connectives $\mathsf{!}_{r}$,
where $r$ is taken from a structure of resources, which make explicit “how
much” a formula can be used.

Using graded modalities, we can rephrase the substitutive property as follows:

${\phi[t/x]\otimes\mathsf{!}_{r}(t\eqcirc u)}\vdash{\phi[u/x]}$

where $r$ depends on $\phi$ (in a way that will be described in the paper) and
encodes the amount of resources needed to derive the substitution. In this
way, the equality predicate cannot be duplicated, hence it admits a non-
trivial quantitative interpretation.

The main mathematical tool we will use throughout the paper are _Lawvere’s
doctrines_ [Law69], which provide an elegant categorical/algebraic
understanding of logic. The key feature of this approach is that theories are
written as functors, named doctrines, whose domain category models contexts
and terms, and the functor maps each object to a poset that models formulas on
that object ordered by logical entailment. In this framework, logical
phenomena can be explained algebraically, abstracting away from details and
focusing only on essential features. For instance, replicability of standard
equality in substructural logics has a neat algebraic explanation: such an
equality is defined by a left adjoint, as pioneered by Lawvere [Law69, Law70],
and, as we will show, predicates defined in this way are always replicable.
This shows that a quantitative equality _cannot be given by a left adjoint_ ,
however, thanks to the language of doctrines, we manage to compare in a
rigorous way quantitative equality with the standard one, proving they share
other fundamental structural properties. More precisely, as proved in [EPR20],
standard equality in non-linear doctrines has a coalgebraic nature and
quantitative equality, generalising the standard one, is coalgebraic as well.

The rest of the paper is organised as follows. Sect. 2 recalls known facts on
equality in doctrines and presents their extension to the linear setting,
discussing the non-quantitative nature of such an equality. Sect. 3 presents
our framework for quantitative equality in a (graded) substructural logic. In
Sect. 3.1 we first define $R$-graded doctrines, which are doctrines modelling
the $(\otimes,\mathbf{1})$-fragment of Linear Logic enriched by $R$-graded
modalities, where $R$ is an ordered semiring of resources, and introduce
$R$-Lipschitz doctrines, namely, $R$-graded doctrines with quantitative
equality. Then, in Sect. 3.2, we present a core deductive calculus for
quantitative equality, based on that in [BP15], describing its sound and
complete categorical semantics in $R$-Lipschitz doctrines in Sect. 3.3. Sect.
4 compares our approach to Quantitative Equational Theories (QETs) [MPP16,
MPP17], providing some examples of theories in our calculus, which cannot be
expressed as QETs. Sect. 5 analyses 2-categorical properties of $R$-Lipschitz
doctrines. In Sect. 5.1 we show the coalgebraic nature of $R$-Lipschitz
doctrines by proving they arise as coalgebras for a 2-comonad on the
2-category of $R$-graded doctrines. This provides us with a universal
construction yielding an $R$-Lipschitz doctrine from an $R$-graded one, and we
use it to generate semantics for the calculus. In Sect. 5.2 we relate
quantitative equality with the usual one defined by left adoints, formally
proving that the former indeed refines the latter. Then, in Sect. 6 we extend
previous results to richer fragments of Linear Logic up to full LL with
quantifiers. We conclude in Sect. 7 discussing related and future work.

This paper is the journal version of [DP22]. Here, we give more background on
doctrines (Sect. 2.1) and more details on standard equality in the
substructural setting (Sect. 2.2). Moreover, we provide a categorical
comparison between our quantitative equality and the usual one by left
adjoints (Sect. 5.2). Finally, we also present more examples of theories
(Sect. 4) and report all proofs of our results.

##  2\. Preliminaries on (linear) doctrines

Doctrines provide a simple categorical framework to study several kinds of
logics. In this section, we first recall basic notions about doctrines for
standard (i.e. non-linear) logics, then we introduce the class of doctrines
modelling the fragment of linear logic we will be concerned with.

###  2.1. Doctrines in a nutshell

Denote by $\mathpzc{Pos}$ the category of posets and monotone functions. A
left adjoint to a monotone function ${{g}}:{{K}}\rightarrow{{H}}$ is a
monotone function ${{f}}:{{H}}\rightarrow{{K}}$ such that for every $x$ in $K$
and $y$ in $H$, both $y\leq gf(y)$ and $fg(x)\leq x$ hold. Equivalently $y\leq
g(x)$ if and only if $f(y)\leq x$.

A _doctrine_ is a pair ${\langle{{\mathpzc{C},\mathit{P}}}\rangle}$ where
$\mathpzc{C}$ is a category with finite products and
${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is a functor. The category $\mathpzc{C}$
is named the _base_ of the doctrine. For $X$ an object in $\mathpzc{C}$ the
poset $\mathit{P}(X)$ is called _fibre over_ $X$. For
${{f}}:{{X}}\rightarrow{{Y}}$ an arrow in $\mathpzc{C}$, the monotone function
${{{\mathit{P}}_{f}}}:{{\mathit{P}(Y)}}\rightarrow{{\mathit{P}(X)}}$ is called
_reindexing along_ $f$. We will often refer to a doctrine
${\langle{{\mathpzc{C},\mathit{P}}}\rangle}$ using only the functor
${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$.

A doctrine ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is _primary_ if all fibres have finite
meets and these are preserved by reindexing. The top element of
$\mathit{P}(A)$ will be denoted as $\top_{A}$, while binary meets by
$\wedge_{A}$. We shall drop the subscripts when these are clear.

There is a large variety of examples of primary doctrines (see [Jac01, vO08,
Pit00]), in this paper we will exemplify definitions considering the
following.

  1. (1)

Let $L$ be a many-sorted signature with sorts $\sigma,\tau,...$, function
symbols $f,g,...$ and predicate symbols $p,q,...$. Let $\mathcal{T}$ be a
theory in the $(\mathbin{\&},\top)$-fragment of First Order Logic over $L$.
The category $\mathpzc{Ctx}_{L}$ has contexts
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$ as
objects and lists of terms
${\langle{{t_{1},\ldots,t_{k}}}\rangle}:\vec{\sigma}\to{\langle{{y_{1}:\tau_{1},\ldots,y_{k}:\tau_{k}}}\rangle}$
as arrows, where each $t_{i}$ has sort $\tau_{i}$ in the context
$\vec{\sigma}$. Binary products are given by context concatenation, up to
renaming of variables. As detailed in [MR13b, Example 2.2] the _syntactic
doctrine $Prp_{\mathcal{T}}$_ based on $\mathpzc{Cxt}_{L}$ maps each context
$\vec{\sigma}$ to the posetal reflection of the collection of well-formed
formulas over $L$ in the $(\mathbin{\&},\top)$-fragment with free variables in
$\vec{\sigma}$ preordered by the entailment in $\mathcal{T}$. That is,
$[\phi]\leq[\psi]$ iff ${\phi}\vdash_{\vec{\sigma}}{\psi}$ is provable in
$\mathcal{T}$ ( In other words, the poset $Prp_{\mathcal{T}}(\vec{\sigma})$ is
the Lindenbaum-Tarski algebra of well-formed formulas over $L$ in the
$(\mathbin{\&},\top)$-fragment with free variables in $\vec{\sigma}$). The
doctrine $Prp_{\mathcal{T}}$ is primary where conjunctions give finite meets.

  2. (2)

Suppose $H$ is a poset, the functor
$\mathop{\mathscr{P}{}}_{H}:\mathpzc{Set}^{\mbox{\scriptsize
op}}\to\mathpzc{Pos}$ sends a set $A$ to the set of functions $H^{A}$ ordered
pointwise. For a function $f:X\to A$ and $\alpha$ in
$\mathop{\mathscr{P}{}}_{H}(A)$ the function
$\mathop{\mathscr{P}{}}_{H}(f)(\alpha)$ is the composite $\alpha f$ in
$\mathop{\mathscr{P}{}}_{H}(X)$. The doctrine $\mathop{\mathscr{P}{}}_{H}$ is
primary when $H$ is a meet-semilattice. For $H=\\{0,1\\}$ the doctrine
$\mathop{\mathscr{P}{}}_{H}$ is the contravariant powerset functor that will
be denoted simply by $\mathop{\mathscr{P}{}}$.

  3. (3)

Suppose that $A=(|A|,.,K,S)$ is a (partial) combinatory algebra as in [vO08].
The doctrine $\mathcal{R}_{A}:\mathpzc{Set}^{\mbox{\scriptsize
op}}\to\mathpzc{Pos}$ maps each set $X$ to the poset reflection of the
preorder $\mathop{\mathscr{P}{}}(|A|)^{X}$ where for
$\alpha,\beta:X\to\mathop{\mathscr{P}{}}(|A|)$, $\alpha\leq\beta$ whenever
there is $a$ in $|A|$ such that, for every $x$ in $X$ and $b$ in $\alpha(x)$,
the application $a.b$ is defined and belongs to $\beta(x)$. One says that $a$
realises $\alpha\leq\beta$. The action of $\mathcal{R}_{A}$ on functions is
given by pre-composition. $\mathcal{R}_{A}$ is primary [vO08].

Doctrines are the objects of the 2-category $\mathbf{Dtn}$ where 1-arrows
${{\langle{{F,f}}\rangle}}:{{\langle{{\mathpzc{C},\mathit{P}}}\rangle}}\rightarrow{{\langle{{\mathpzc{D},\mathit{Q}}}\rangle}}$
consist of a finite product preserving functor
${{F}}:{{\mathpzc{C}}}\rightarrow{{\mathpzc{D}}}$ and a natural transformation
${f}:{\mathit{P}}\stackrel{{\scriptstyle\makebox{\kern-0.90417pt{.}}}}{{\rightarrow}}{\mathit{Q}F^{\mbox{\scriptsize
op}}}$ as in the diagram

$\textstyle{{\mathpzc{C}^{\mbox{\scriptsize
op}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P}$$\scriptstyle{F^{\mbox{\scriptsize
op}}}$$\textstyle{\mathpzc{Pos}}$$\textstyle{{\mathpzc{D}^{\mbox{\scriptsize
op}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q}$$\scriptstyle{f\kern
1.50694pt\cdot\kern-1.50694pt}$

the 2-arrows
${\theta}:{{\langle{{F,f}}\rangle}}\Rightarrow{{\langle{{F^{\prime},f^{\prime}}}\rangle}}$
are natural transformations
${\theta}:{F}\stackrel{{\scriptstyle\makebox{\kern-0.90417pt{.}}}}{{\rightarrow}}{F^{\prime}}$
such that $f_{X}\leq_{FX}{\mathit{Q}}_{\theta_{X}}\circ f^{\prime}_{X}$ for
every object $X$ in $\mathpzc{C}$, i.e.

$\textstyle{{\mathpzc{C}^{\mbox{\scriptsize
op}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P}$$\scriptstyle{F^{\mbox{\scriptsize
op}}}$$\scriptstyle{(F^{\prime})^{\mbox{\scriptsize
op}}}$$\textstyle{\mathpzc{Pos}}$$\textstyle{{\mathpzc{D}^{\mbox{\scriptsize
op}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q}$$\scriptstyle{f\kern
1.50694pt\cdot\kern-1.50694pt}$$\scriptstyle{\kern-1.50694pt\cdot\kern
1.50694ptf^{\prime}}$.$\scriptstyle{\theta^{\mbox{\scriptsize
op}}}$$\scriptstyle{\leq}$

The composition of two consecutive 1-arrows ${\langle{{F,f}}\rangle}$ and
${\langle{{G,g}}\rangle}$ is given by
${\langle{{G,g}}\rangle}\circ{\langle{{F,f}}\rangle}={\langle{{GF,(gF^{\mbox{\scriptsize
op}})f}}\rangle}$, while composition of 2-arrows is that of natural
transformations.

Primary doctrines are the objects of the 2-full 2-subcategory $\mathbf{PD}$ of
$\mathbf{Dtn}$, where a 1-arrow from $\mathit{P}$ to $\mathit{Q}$ is a 1-arrow
${\langle{{F,f}}\rangle}$ in $\mathbf{Dtn}$ such that each component of $f$
preserves finite meets.

######  Remark 1.

The 2-categorical structure of doctrines has a relevant logical meaning:
objects correspond to theories, 1-arrows to models/translations between
theories and 2-arrows to homomorphisms of models/translations. Under this
interpretation the hom-category $\mathbf{Dtn}(\mathit{P},\mathit{Q})$ is the
category of models of $\mathit{P}$ into $\mathit{Q}$. Thus, given a theory
$\mathcal{T}$ in the $(\mathbin{\&},\top)$-fragment of First Order Logic over
a signature $L$, a categorical semantics of $\mathcal{T}$ in $\mathit{P}$ is
an object of $\mathbf{Dtn}(Prp_{\mathcal{T}},\mathit{P})$.

A categorical description of equality in terms of left adjoints goes back to
Lawvere [Law70]. More recently, Maietti and Rosolini [MR13a] identify primary
doctrines as the essential framework where equality can be studied. Primary
doctrines with equality are called elementary [MR13a] and are defined as
follows.

A primary doctrine ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is _elementary_ if for every $A$ in
$\mathpzc{C}$, there is an element $\delta_{A}$ in $\mathit{P}(A\times A)$
such that

  1. (1)

$\top_{A}\leq{\mathit{P}}_{\Delta_{A}}(\delta_{A})$

  2. (2)

for all $X$ in $\mathpzc{C}$ and $\alpha$ in $\mathit{P}(X\times A)$ it holds
that
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\land{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\delta_{A})\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\alpha)$

  1. (1)

Consider a theory $\mathcal{T}$ over the
$(\mathbin{\&},\top,\eqcirc)$-fragment of First Order Logic. Then, the
syntactic doctrine $Prp_{\mathcal{T}}$, defined as in Example 2.1(1), is
elementary. Indeed, for every context
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$
one can take as $\delta_{\vec{\sigma}}$ the formula $x_{1}\eqcirc
y_{1}\mathbin{\&}\ldots\mathbin{\&}x_{n}\eqcirc y_{n}$. over the context
$\vec{\sigma}\times\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n},y_{1}:\sigma_{1},\ldots,y_{n}:\sigma_{n}}}\rangle}$;
conditions (1) and (2) in Def. 2.1 require the provability of entailments of
the form

$\top\vdash x_{1}\eqcirc x_{1}\mathbin{\&}\ldots\mathbin{\&}x_{n}\eqcirc
x_{n}\qquad\phi(\vec{z},x_{1},\ldots,x_{n})\mathbin{\&}x_{1}\eqcirc
y_{1}\mathbin{\&}\ldots\mathbin{\&}x_{n}\eqcirc
y_{n}\vdash\phi(\vec{z},y_{1},\ldots,y_{n})$

which easly follows from reflexivity and substitutivity of $x\eqcirc y$.

  2. (2)

The primary doctrine $\mathop{\mathscr{P}{}}_{H}$ of Example 2.1(2) is
elementary when $H$ has a bottom element. For a set $X$, the equality
predicate $\delta_{X}\in H^{X\times X}$ is the Kronecker delta mapping
$(x,x^{\prime})$ to $\top$ if $x=x^{\prime}$ and to $\bot$ otherwise.

  3. (3)

The primary doctrine $\mathcal{R}_{A}$ of Example 2.1(3) is elementary where
for a set $X$ the function $\delta_{X}$ maps $(x,x^{\prime})$ to $|A|$ if
$x=x^{\prime}$ and to $\emptyset$ otherwise [vO08].

Elementary doctrines are the objects of the 2-category $\mathbf{ED}$ where a
1-arrow ${{\langle{{F,f}}\rangle}}:{\mathit{P}}\rightarrow{\mathit{Q}}$ is a
1-arrow in $\mathbf{PD}$ such that $f$ preserves equality predicates. The
2-arrows are those of $\mathbf{PD}$.

As studied in [EPR20], equality is coalgebraic in the sense that the obvious
inclusion of $\mathbf{ED}$ into $\mathbf{PD}$ has a right 2-adjoint

$\textstyle{\mathbf{ED}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathbf{PD}}$
(1)

and $\mathbf{ED}$ is isomorphic to the 2-category of coalgebras of the induced
2-comonad on $\mathbf{PD}$.

######  Remark 2.

Similarly to what we have already observed in Remark 1, given a theory
$\mathcal{T}$ in the $(\mathbin{\&},\top,\eqcirc)$-fragment of First Order
Logic, a categorical semantics of $\mathcal{T}$ in an elementary doctrine
$\mathit{P}$ is an object of $\mathbf{ED}(Prp_{\mathcal{T}},\mathit{P})$.
Therefore the adjoint situation in Diagram 1 allows to build semantics for
theories with equality, from semantics of theories without equality.

A primary doctrine ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is a _first order doctrine_ if
$\mathit{P}$ factors through the category of Heyting algebras and their
homomorphisms and for every projection $\pi:A\times B\to B$ in $\mathpzc{C}$
the map $\mathit{P}(\pi)$ has a left adjoint
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\pi}$ and a right adjoint
$\mathchoice{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
A$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
A$}}\kern-2.58334pt_{\pi}$ and these adjoints are natural in $B$, that is for
every square

$\textstyle{A\times
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi}$$\scriptstyle{\mathrm{id}_{A}\times
f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{A\times
B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi}$$\textstyle{B}$

it holds that
${\mathit{P}}_{f}\,\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\pi}=\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\pi}\,{\mathit{P}}_{\mathrm{id}_{A}\times f}$ and
${\mathit{P}}_{f}\,\mathchoice{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
A$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
A$}}\kern-2.58334pt_{\pi}=\mathchoice{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
A$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
A$}}\kern-2.58334pt_{\pi}\,{\mathit{P}}_{\mathrm{id}_{A}\times f}$. The
naturality of left and right adjoints is often called Beck-Chevalley
condition. A primary doctrine ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is a _hyperdoctrine_ if it is first order
and elementary.

  1. (1)

The syntactic doctrine $Prp_{\mathcal{T}}$ over a theory $\mathcal{T}$ in full
First Order Logic is first order (recall also Example 2.1(1)). For every
context $\vec{\sigma}$ the logical connectives between formulas with free
variables in $\vec{\sigma}$ provide the operations of the Heyting algebra. For
a formula $\alpha$ over
$\vec{\sigma}\times\vec{\tau}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}\,,\,y_{1}:\tau_{1},\ldots,y_{k}:\tau_{k}}}\rangle}$
the left adjoint along $\pi:\vec{\sigma}\times\vec{\tau}\to\vec{\tau}$ is the
formula
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\pi}\alpha$ with free variables over $\vec{\tau}$ defined
as

$\exists_{x_{1}:\sigma_{1}}\ldots\exists_{x_{n}:\sigma_{n}}\alpha$

The right adjoint
$\mathchoice{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$A$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
A$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
A$}}\kern-2.58334pt_{\pi}\alpha$ is similar where the universal quantification
is used in place of the existential one. The syntactic doctrine
$Prp_{\mathcal{T}}$ over a theory $\mathcal{T}$ (see also Example 2.1(1)) in
full First Order Logic with equality is a hyperdoctrine.

  2. (2)

The primary doctrine $\mathop{\mathscr{P}{}}_{H}$ of Example 2.1(2) is an
hyperdoctirne when $H$ is a complete Heyting algebra, i.e. it has arbitrary
suprema that distribute over meets [Pit00, vO08].

  3. (3)

The primary doctrine $\mathcal{R}_{A}$ of Example 2.1(3) is an hyperdoctrine
[vO08].

Denote by $\mathbf{FOD}$ the 2-full 2-subcategory of $\mathbf{PD}$ on first
order doctrines and those 1-arrows of $\mathbf{PD}$ that additionally commute
with all connectives and quantifiers. Similarly, $\mathbf{HD}$ denotes the
2-full 2-subcategory of $\mathbf{ED}$ on hyperdoctrines111One can see
$\mathbf{HD}$ as the pullback of $\mathbf{ED}\to\mathbf{PD}$ along
$\mathbf{FOD}\to\mathbf{PD}$.. The adjoint situation depicted in Diagram 1
restricts to the inclusion of $\mathbf{FOD}$ into $\mathbf{PD}$ and co-
restricts to the inclusion of $\mathbf{HD}$ into $\mathbf{ED}$, leading to the
following diagram

$\textstyle{\mathbf{ED}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathbf{PD}}$$\textstyle{\mathbf{HD}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathbf{FOD}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
(2)

Combining the observations made in Remark 1 and in Remark 2 it not surprising
that, given a theory $\mathcal{T}$ in full First Order Logic over a signature
$L$, a categorical semantics of $\mathcal{T}$ in a first order doctrine
$\mathit{P}$ is an object of $\mathbf{FOD}(Prp_{\mathcal{T}},\mathit{P})$; and
if $\mathcal{T}$ is with equality and $P$ is a hyperdoctrine (and not only a
first order doctrine) models of $\mathcal{T}$ in $\mathit{P}$ are objects
$\mathbf{HD}(Prp_{\mathcal{T}},\mathit{P})$.

###  2.2. Primary and elementary linear doctrines

Primary doctrines, that models the $(\&,\top)$-fragment of First Order Logic,
are the minimal setting where one can formulate rules of equality (cf. Def.
2.1). We shall call their linear counterpart primary linear doctrines. They
model the $(\otimes,\mathbf{1})$-fragment of Linear Logic and provide the
minimal structure needed to describe equality in a substructural setting. The
following definition is carved out from Seely’s definition of linear
hyperdoctrines [See89]

A _primary linear doctrine_ is a triple
${\langle{{\mathit{P},\ast,\kappa}}\rangle}$ where
${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is a doctrine and
${\ast}:{\mathit{P}\times\mathit{P}}\stackrel{{\scriptstyle\makebox{\kern-0.90417pt{.}}}}{{\rightarrow}}{\mathit{P}}$
and
${\kappa}:{\mathit{1}{C}}\stackrel{{\scriptstyle\makebox{\kern-0.90417pt{.}}}}{{\rightarrow}}{\mathit{P}}$
are natural transformations such that, for all objects $X$ in $\mathpzc{C}$,
${\langle{{\mathit{P}(X),\ast_{X},\kappa_{X}}}\rangle}$ is a commutative
monoid.

Spelling out the definition, a primary linear doctrine is determined by a
doctrine ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ and, for each object $X$ in $\mathpzc{C}$,
a monotone function
${{\ast_{X}}}:{{\mathit{P}(X)\times\mathit{P}(X)}}\rightarrow{{\mathit{P}(X)}}$
and an element $\kappa_{X}\in\mathit{P}(X)$ such that $\ast_{X}$ is
associative and commutative and $\kappa_{X}$ is the neutral element for
$\ast_{X}$ and, for ${{f}}:{{X}}\rightarrow{{Y}}$ in $\mathpzc{C}$ and
$\alpha,\beta$ in $\mathit{P}(Y)$, we have
${\mathit{P}}_{f}(\alpha)\ast_{X}{\mathit{P}}_{f}(\beta)={\mathit{P}}_{f}(\alpha\ast_{Y}\beta)$
and $\kappa_{X}={\mathit{P}}_{f}(\kappa_{Y})$222Concisely, a primary linear
doctrine is a monoid in $[\mathpzc{C}^{\mbox{\scriptsize
op}},\mathpzc{Pos}]$.. We shall often omit subscripts from $\ast$ and $\kappa$
when these are obvious.

Primary linear doctrines are the objects of the 2-category $\mathbf{LD}$ where
a 1-arrow from
${\langle{{\mathit{P},\ast^{\mathit{P}},\kappa^{\mathit{P}}}}\rangle}$to
${\langle{{\mathit{Q},\ast^{\mathit{Q}},\kappa^{\mathit{Q}}}}\rangle}$ is a
1-arrow ${{\langle{{F,f}}\rangle}}:{\mathit{P}}\rightarrow{\mathit{Q}}$ in
$\mathbf{Dtn}$ such that $f$ is a natural monoid homomorphism, and 2-arrows
are those of $\mathbf{Dtn}$.

  1. (1)

For a theory $\mathcal{T}$ in the $(\otimes,\mathbf{1})$-fragment of Linear
Logic as in [Gir87] the syntactic doctrine $Prp_{\mathcal{T}}$ as in Example
2.1(1) is primary linear.

  2. (2)

If ${\langle{{H,\ast,\kappa}}\rangle}$ is an ordered commutative monoid, then
${\langle{{\mathop{\mathscr{P}{}}_{H},\ast,\kappa}}\rangle}$ is primary
linear, where $\mathop{\mathscr{P}{}}_{H}$ is as in Example 2.1(2) and $\ast$
and $\kappa$ are defined pointwise.

  3. (3)

A BCI algebra $A={\langle{{|A|,.,B,C,I}}\rangle}$ can be seen as a linear
version of a combinatory algebra where linear combinators $B,C,I$ are used in
place of combinators $K,S$ (a precise definition is in [AHS02]). Analogously
to Example 2.1(3) we define the realisability doctrine
${{\mathcal{R}_{A}}}:{{\mathpzc{Set}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ as the functor that maps each set $X$ to
the poset reflection of the preorder $\mathop{\mathscr{P}{}}(|A|)^{X}$ where
for $\alpha,\beta\in\mathop{\mathscr{P}{}}(|A|)^{X}$, it is $\alpha\leq\beta$
whenever there is $a\in|A|$ such that, for every $x\in X$ and $b\in\alpha(x)$,
the application $a.b$ is defined and belongs to $\beta(x)$. The action of
$\mathcal{R}_{A}$ on functions is by pre-composition. Each
$\mathcal{R}_{A}(X)$ is a poset as $I$ and $B$ realise reflexivity and
transitivity of $\leq$, respectively. Given
$\alpha,\beta\in\mathop{\mathscr{P}{}}(|A|)^{X}$, define
$\alpha\ast\beta=x\mapsto\\{\textbf{P}ab\in|A|\mid a\in\alpha(x)\ \text{and}\
b\in\beta(x)\\}$, where P is the BCI pairing [Hos07], and
$\kappa_{X}=x\mapsto\\{I\\}$. Then,
${\langle{{\mathcal{R}_{A},\ast,\kappa}}\rangle}$ is a primary linear
doctrine.

  4. (4)

Let $\mathbb{W}={\langle{{W,\leq,\circ,\epsilon}}\rangle}$ be an ordered
commutative monoid (a.k.a. monoidal Kripke frame). Adapting from [DG22] the
notion of $\mathbb{W}$-relation, we define a doctrine
${{K_{\mathbb{W}}}}:{{\mathpzc{Set}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ as follows: for a set $X$,
$K_{\mathbb{W}}(X)$ is the collection of those subsets $U$ of $X\times W$ such
that if ${\langle{{x,w}}\rangle}\in U$ and $w\leq w^{\prime}$ then
${\langle{{x,w^{\prime}}}\rangle}\in U$ ordered by set inclusion, and for a
function ${{f}}:{{X}}\rightarrow{{Y}}$, $K_{\mathbb{W}}(f)$ maps $U\in
K_{\mathbb{W}}(Y)$ to $(f\times\mathrm{id}_{W})^{-1}(U)$. This is actually a
primary linear doctrine, where, for every set $X$,
$\kappa_{X}=\\{{\langle{{x,w}}\rangle}\mid\epsilon\leq w\\}$ and
$U\ast_{X}V=\\{{\langle{{x,w}}\rangle}\mid\exists_{w_{1},w_{2}}.\,w_{1}\circ
w_{2}\leq w,{\langle{{x,w_{1}}}\rangle}\in U,{\langle{{x,w_{2}}}\rangle}\in
V\\}$.

Recall that elementary doctrines can be understood as those primary doctrine
endowed with equality predicates. The following definition introduces those
primary linear doctrines that are elementary as a direct linearisation of Def.
2.1 (i.e. replacing of $\wedge,\top$ by $\ast,\kappa$).

A primary linear doctrine ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is _elementary_ if for every $A$ in
$\mathpzc{C}$, there is an element $\delta_{A}$ in $\mathit{P}(A\times A)$
such that

  1. (1)

$\kappa_{A}\leq{\mathit{P}}_{\Delta_{A}}(\delta_{A})$

  2. (2)

for all $X$ in $\mathpzc{C}$ and $\alpha$ in $\mathit{P}(X\times A)$ it holds
that
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\delta_{A})\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\alpha)$

Lawvere first noticed that equality is a left adjoint [Law70]. This turns out
to be true also in the linear setting.

######  Proposition 3.

Let ${{\mathit{P}}}:{{\mathpzc{C}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ be a primary doctrine, the following are
equivalent

  1. (1)

$\mathit{P}$ is elementary

  2. (2)

For every $A$ there is $\delta_{A}$ in $\mathit{P}(A\times A)$ such that for
every $X$ and every $\alpha$ in $\mathit{P}(X\times A)$ the assignment

$\textstyle{\mathit{P}(X\times
A)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-0.90417pt_{\mathrm{id}_{X}\times\Delta_{A}}}$$\textstyle{\mathit{P}(X\times
A\times
A)}$$\textstyle{\alpha\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\delta_{A})}$

defines a left adjoint to ${\mathit{P}}_{\mathrm{id}_{X}\times\Delta_{A}}$.

######  Proof 2.1.

(1)$\Rightarrow$ (2). Suppose
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\mathrm{id}_{X}\times\Delta_{A}}(\alpha)\leq\beta$ and
apply ${\mathit{P}}_{\mathrm{id}_{X}\times\Delta_{A}}$ to both side of the
inequality to get
$\alpha\leq{\mathit{P}}_{\mathrm{id}_{X}\times\Delta_{A}}(\beta)$. Conversely
suppose $\alpha\leq{\mathit{P}}_{\mathrm{id}_{X}\times\Delta_{A}}(\beta)$.
Consider $\beta$ as an element over $(X\times A)\times A$ and let
$p_{1},p_{2}$ and $p_{3}$ denote projections from $(X\times A)\times A\times
A$ and $\pi_{1},\pi_{2}$ and $\pi_{3}$ denote projections from $X\times
A\times A$. It holds
${\mathit{P}}_{{\langle{{p_{1},p_{2}}}\rangle}}(\beta)\ast{\mathit{P}}_{{\langle{{p_{2},p_{3}}}\rangle}}(\delta_{A})\leq{\mathit{P}}_{{\langle{{p_{1},p_{3}}}\rangle}}(\beta)$.
Evaluate both side of the inequality under
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2},\pi_{2},\pi_{3}}}\rangle}}$ to get

${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}{\mathit{P}}_{\mathrm{id}_{X}\times\Delta_{A}}(\beta)\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\delta_{A})\leq\beta$

and hence the claim.

(2)$\Rightarrow$ (1). Note that
$\delta_{A}=\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\Delta_{A}}(\kappa_{A})$, so
$\kappa_{A}\leq{\mathit{P}}_{\Delta_{A}}(\delta_{A})$. Given $\alpha$ in
$\mathit{P}(X\times A)$, from
$\alpha={\mathit{P}}_{{\langle{{\mathrm{id}_{X}\times\Delta_{A}}}\rangle}}{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\alpha)$
follows
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\mathrm{id}_{X}\times\Delta_{A}}(\alpha)={\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\delta_{A})\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\alpha)$.

The characterisation 3 will be helpful to prove some basic properties of
equality predicates. Equality predicates in elementary doctrines (i.e. in the
non-linear setting) are proved to be equivalence relations. Their linear
counterpart are distances333Binary products in base $\mathpzc{C}$ of
$\mathit{P}$ play a crucial role in defining what a distance is, as one need
diagonals and, more generally, tuples of arrows to formulate reflexivity and
transitivity. This is clear from the syntactic point of view, as one can see
from Example 2.2(1), where to write conditions for reflexivity and
transitivity one uses formulas where the same variables occurs multiple
times., which can be defined in an abstract purely algebraic way in any
primary linear doctrine ${\langle{{\mathit{P},\ast,\kappa}}\rangle}$ as
follows: a _$\mathit{P}$ -distance_ on an object $A$ is an element
$\rho\in\mathit{P}(A\times A)$ such that

$\kappa\leq{\mathit{P}}_{\Delta_{A}}(\rho)$ | (reflexivity)
---|---
$\rho\leq{\mathit{P}}_{{\langle{{\pi_{2},\pi_{1}}}\rangle}}(\rho)$ | (symmetry)
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\rho)\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\rho)\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\rho)$ | (transitivity)

  1. (1)

For the syntactic doctrine $Prp_{\mathcal{T}}$ as in Example 2.2(1), a
$Prp_{\mathcal{T}}$-distance over a context $\vec{\sigma}$ is a formula
$\rho(\vec{x},\vec{y})$ in the context $\vec{\sigma}\times\vec{\sigma}$ such
that the following entailments are derivable:
$\mathbf{1}\vdash\rho(\vec{x},\vec{x})$ and
$\rho(\vec{x},\vec{y})\vdash\rho(\vec{y},\vec{x})$ and
$\rho(\vec{x},\vec{y})\otimes\rho(\vec{y},\vec{z})\vdash\rho(\vec{x},\vec{z})$.

  2. (2)

For the primary linear doctrine
${\langle{{\mathop{\mathscr{P}{}}_{[0,\infty]},+,0}}\rangle}$ as in Example
2.2(2) (where $[0,\infty]$ is the Lawvere quantale [Law73]) a
$\mathop{\mathscr{P}{}}_{[0,\infty]}$-distance $\rho$ over a set $X$ is a
metric $\rho:X\times X\to[0,\infty]$, i.e. $0\geq\rho(x,x)$ and
$\rho(x,y)\geq\rho(y,x)$ and $\rho(x,y)+\rho(y,z)\geq\rho(x,z)$.

  3. (3)

For the realisability doctrine $\mathcal{R}_{A}$ as in Example 2.2(3), a
$\mathcal{R}_{A}$-distance $\rho$ over a set $X$ is function
${{\rho}}:{{X\times X}}\rightarrow{{\mathop{\mathscr{P}{}}(|A|)}}$ such that
there are three elements in $|A|$ realising reflexivity, symmetry,
transitivity of $\rho$.

  4. (4)

For the doctrine $K_{\mathbb{W}}$ as in Example 2.2(4), a
$K_{\mathbb{W}}$-distance over a set $X$ is a ternary relation $\rho\subseteq
X\times X\times W$ such that, for every $x,y,z$ in $X$ and every
$w,w_{1},w_{2}$ in $W$, we have $\epsilon\leq w$ implies
${\langle{{x,x,w}}\rangle}\in\rho$ and ${\langle{{x,y,w}}\rangle}\in\rho$
implies ${\langle{{y,x,w}}\rangle}\in\rho$ and
${\langle{{x,y,w_{1}}}\rangle}\in\rho$ and
${\langle{{y,z,w_{2}}}\rangle}\in\rho$ implies ${\langle{{x,z,w_{1}\circ
w_{2}}}\rangle}\in\rho$.

######  Proposition 4.

Let ${\langle{{\mathit{P},\ast,\kappa}}\rangle}$ be an elementary primary
linear doctrine. For every obect $A$ in the base of $\mathit{P}$, the equality
predicate $\delta_{A}$ is a $\mathit{P}$-distance.

######  Proof 2.2.

The first point of Def. 2.2 establishes reflexivity of $\delta_{A}$. The
second point gives transitivity when $X$ is $A$ and $\alpha$ is $\delta_{A}$.
To show symmetry, first note that
${\langle{{\pi_{2},\pi_{1}}}\rangle}\circ\Delta_{A}=\Delta_{A}$, then use
Prop. 3 to get
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{{\langle{{\pi_{2},\pi_{1}}}\rangle}}(\delta_{A})=\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{{\langle{{\pi_{2},\pi_{1}}}\rangle}}\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\Delta_{A}}(\kappa_{A})=\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\Delta_{A}}(\kappa_{A})=\delta_{A}$ and conclude by the
adunction
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\Delta_{A}}\dashv{\mathit{P}}_{\Delta_{A}}$ that
$\delta_{A}\leq{\mathit{P}}_{{\langle{{\pi_{2},\pi_{1}}}\rangle}}(\delta_{A})$.

As already mentioned in the introduction, the direct rephrasing of rules for
equality from First Order Logic to Linear Logic leads to a replicable equality
predicate. This was already observed by Dozen [Doz96] and it can be quickly
seen in the following tree

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
13.33328pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=26.66656pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{}\vdash{t\eqcirc t}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\quad\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox
spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
13.33328pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=26.66656pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{}\vdash{t\eqcirc t}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=131.7708pt\hbox{}}}\hbox{\kern
36.16331pt\hbox{$\displaystyle{}\vdash{t\eqcirc t\otimes t\eqcirc
t}$}}}}\hskip 5.0pt plus 1.0fil\penalty 2\quad\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
25.72447pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=51.44894pt\hbox{}}}\hbox{\kern
0.0pt\hbox{$\displaystyle{t\eqcirc u}\vdash{t\eqcirc u}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=261.65741pt\hbox{}}}\hbox{\kern
87.6587pt\hbox{$\displaystyle{t\eqcirc u}\vdash{t\eqcirc u\otimes t\eqcirc
u}$}}}}$

by reflexivity of $\eqcirc$, we have ${}\vdash{t\eqcirc t}$, then, introducing
$\otimes$ on the right, we get ${}\vdash{t\eqcirc t\otimes t\eqcirc t}$; by
the assumption ${t\eqcirc u}\vdash{t\eqcirc u}$, then, since $t\eqcirc
t\otimes t\eqcirc t$ is equal to $(t\eqcirc x\otimes t\eqcirc x)[t/x]$, using
substitutivity we conclude ${t\eqcirc u}\vdash{t\eqcirc u\otimes t\eqcirc u}$.

Doctrines allows to prove this drawback in more generality. Given a primary
linear doctrine ${\langle{{\mathit{P},\ast,\kappa}}\rangle}$, an element
$\alpha$ in $\mathit{P}(X)$ is called _affine_ if $\alpha\leq\kappa$ and
_replicable_ if $\alpha\leq\alpha\ast\alpha$. Note that on affine and
replicable elements the monoidal operation $\ast$ behaves as a meet operation,
hence, they can be deleted and duplicated.

  1. (1)

For the syntactic doctrine $Prp_{\mathcal{T}}$ over a theory $\mathcal{T}$ in
the $(\otimes,\mathbf{1})$-fragment of Linear Logic, an element $\alpha$ in
$Prp_{\mathcal{T}}(\vec{\sigma})$ (i.e. is a formula with free variables over
the context $\vec{\sigma}$) is affine when weakening
($\alpha\vdash\mathbf{1}$) is derivable in $\mathcal{T}$, while $\alpha$ is
replicable if contraction ($\alpha\vdash\alpha\otimes\alpha$) is derivable in
$\mathcal{T}$.

  2. (2)

For the primary linear doctrine
${\langle{{\mathop{\mathscr{P}{}}_{[0,\infty]},+,0}}\rangle}$ as in Example
2.2(2) every element $\alpha:A\to[0,\infty]$ is affine as $0$ is also a top
element, while $\alpha$ is replicable if and only if its values are either $0$
or $\infty$.

######  Proposition 5.

Let ${\langle{{\mathit{P},\ast,\kappa}}\rangle}$ be primary linear and
${{f}}:{{X}}\rightarrow{{Y}}$ an arrow of the base. If ${\mathit{P}}_{f}$ has
a left adjoint
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}$, then
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}(\kappa_{X})$ is affine and replicable.

######  Proof 2.3.

We prove affineness by noting that
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}(\kappa_{X})=\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}{\mathit{P}}_{f}(\kappa_{Y})\leq\kappa_{Y}$.
Replicability follows from
$\kappa_{X}=\kappa_{X}\ast\kappa_{X}\leq{\mathit{P}}_{f}(\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}\kappa_{X})\ast{\mathit{P}}_{f}(\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}\kappa_{X})={\mathit{P}}_{f}(\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}(\kappa_{X})\ast\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}(\kappa_{X}))$ and the adjunction between
$\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{f}$ and ${\mathit{P}}_{f}$.

By Prop. 3 it is
$\delta_{A}=\mathchoice{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$E$}}{\rotatebox[origin={c}]{180.0}{$\scriptstyle
E$}}{\rotatebox[origin={c}]{180.0}{$\scriptscriptstyle
E$}}\kern-1.29167pt_{\Delta_{A}}(\kappa_{A})$. Affineness and replicability
follows by Prop. 5.

This shows that the standard approach based on left adjoints cannot support a
quantitative notion of equality, which then needs to be defined in a different
way.

##  3\. Quantitative equality via graded modalities

Graded modalities indexed by a semiring $R$ are used in many linear calculi
and type theories to enable resource sensitive reasoning [RP10, BGMZ14,
GKO+16, OLI19, AB20, DG22, MIO21]. We introduce graded modalities in the
framework of primary linear doctrines to formulate a quantitative variant of
elementary doctrines that we call Lipschitz doctrines. We motivate the
terminology after Corollary 10. Then, we define a core deductive calculus for
quantitative equality and its categorical semantics in Lipschitz doctrines,
proving it is sound and complete.

###  3.1. Graded and Lipschitz doctrines

A _resource semiring_ is a semiring in the category $\mathpzc{Pos}$, that is,
a tuple $R={\langle{{|R|,\preceq,+,\cdot,0,1}}\rangle}$, where
${\langle{{|R|,\preceq}}\rangle}$ is a partially ordered set and $+$ and
$\cdot$ are monotone binary operations on it such that

  * •

${\langle{{|R|,+,0}}\rangle}$ is a commutative monoid and
${\langle{{|R|,\cdot,1}}\rangle}$ is a monoid,

  * •

for all $r,s,q\in|R|$ we have $r\cdot(s+q)=r\cdot s+r\cdot q$, $(s+q)\cdot
r=s\cdot r+q\cdot r$, $r\cdot 0=0$ and $0\cdot r=0$,

  * •

$+$ and $\cdot$ are monotone w.r.t. $\preceq$.

To define $R$-graded modalities, we adapt the approach in [DR21], following
the definition of graded linear exponential comonads [BGMZ14, GKO+16, Kat18].

An _$R$ -graded (linear exponential) modality_ on a primary linear doctrine
${\langle{{\mathit{P},\ast.\kappa}}\rangle}$ is an $|R|$-indexed family of
natural transformations
${\flat_{r}}:{\mathit{P}}\stackrel{{\scriptstyle\makebox{\kern-0.90417pt{.}}}}{{\rightarrow}}{\mathit{P}}$
satisfying the axioms below for all objects $X$, $\alpha,\beta$ in
$\mathit{P}(X)$ and $r,s$ in $|R|$:

  1. (1)

$\kappa\leq\flat_{r}\kappa$ (lax-monoidality-1)

  2. (2)

$\flat_{r}\alpha\ast\flat_{r}\beta\leq\flat_{r}(\alpha\ast\beta)$ (lax-
monoidality-2)

  3. (3)

$\flat_{0}\alpha\leq\kappa$ (weakening)

  4. (4)

$\flat_{r+s}\alpha\leq\flat_{r}\alpha\ast\flat_{s}\alpha$ (contraction)

  5. (5)

$\flat_{1}\alpha\leq\alpha$ (counit)

  6. (6)

$\flat_{r\cdot s}\alpha\leq\flat_{r}(\flat_{s}\alpha)$ (comultiplication)

  7. (7)

$\flat_{r}\alpha\leq\flat_{s}\beta$ if $s\preceq r$ (controvariance)

An _$R$ -graded (primary linear) doctrine_ is a primary linear doctrine
together with an $R$-graded modality on it.

Naturality ensures that $\flat_{r}$ is monotone and stable under reindexing,
for all $r$. making the graded modality a graded linear exponential comonad on
each fibre.

We collect below some examples adapted from [BP15, OLI19, DG22].

  1. (1)

The singleton set $\\{\infty\\}$ with the trivial order and operations is a
resource semiring. An $\\{\infty\\}$-graded modality on $\mathit{P}$ satisfies
the following inequalities fibre-wise: $\flat_{\infty}\alpha\leq\kappa$,
$\flat_{\infty}\alpha\leq\flat_{\infty}\alpha\ast\flat_{\infty}\alpha$,
$\flat_{\infty}\alpha\leq\alpha$ and
$\flat_{\infty}\alpha\leq\flat_{\infty}\flat_{\infty}\alpha$. Hence,
$\flat_{\infty}$ models the usual bang modality of Linear Logic [Gir87].
Syntactic doctrines on the $(\otimes,\mathbf{1},\mathsf{!})$-fragment of
Linear Logic are $\\{\infty\\}$-graded.

  2. (2)

Let $\mathbb{N}$ abbreviate the semiring
${\langle{{\mathbb{N},+,\cdot,0,1}}\rangle}$ of natural numbers and
$\mathbb{N}_{\infty}$ its extension by a new point $\infty$ with
$\infty+x=x+\infty=\infty\cdot x=x\cdot\infty=\infty$. Denote by
$\mathbb{N}^{=}$ and $\mathbb{N}^{=}_{\infty}$ the semirings $\mathbb{N}$ and
$\mathbb{N}_{\infty}$ ordered by the equality relation. If $\flat$ is an
$\mathbb{N}^{=}$-graded modality on $\mathit{P}$, since $n=1+\ldots+1$ ($n$
times), contraction and counit imply
$\flat_{n}\alpha\leq\alpha\ast\ldots\ast\alpha$ ($n$ times). Hence,
$\flat_{n}\alpha$ provides exactly $n$ copies of $\alpha$. Syntactically, this
corresponds to the _exact usage_ modality $\mathsf{!}_{n}$ of Bounded Linear
Logic [GSS92]. Indeed, syntactic doctrines built out of it are
$\mathbb{N}^{=}$-graded. If we consider $\mathbb{N}^{=}_{\infty}$, we get the
additional modality $\flat_{\infty}$ which behaves as in Item 1, modelling
unrestricted usage.

  3. (3)

Let $\mathbb{R}_{\geq 0}={\langle{{[0,\infty),\leq,+,\cdot,0,1}}\rangle}$ be
the semiring of non-negative real numbers, $[0,\infty]$ be the Lawvere
quantale [Law73] and
${\langle{{\mathop{\mathscr{P}{}}_{[0,\infty]},+,0}}\rangle}$ be a doctrine as
in Example 2.2(2). For $\alpha\in\mathop{\mathscr{P}{}}_{[0,\infty]}(X)$ and
$r\in[0,\infty)$, the assignment $\alpha\mapsto\textbf{m}_{r}\alpha$, with
$\textbf{m}_{r}\alpha(x)=r\cdot\alpha(x)$ is an $\mathbb{R}_{\geq 0}$-graded
modality on $\mathop{\mathscr{P}{}}_{[0,\infty]}$. Here $r\cdot\infty=\infty$
when $r\neq 0$ and $0\cdot\infty=0$.

  4. (4)

Consider an ordered $R$-Linear Combinatory Algebra ($R$-LCA) [Atk18], that is,
a BCI algebra $A$ (cf. Example 2.2(3)) with a function
${{!_{r}}}:{{|A|}}\rightarrow{{|A|}}$ for $r\in|R|$ and elements
$K,W_{r,s},D,d_{r,s},F_{r}$ and $O_{r,s}$, with $r\preceq s$, of $|A|$
satisfying

$\begin{array}[]{ll}K.x.!_{0}y=x&\quad W_{r,s}.x.!_{r+s}y=x.!_{r}y.!_{s}y\\\
D.!_{1}x=x&\quad d_{r,s}.!_{r\cdot s}x=!_{r}!_{s}x\\\
F_{r}.!_{r}x.!_{r}y=!_{r}(x.y)&\quad O_{r,s}.!_{s}x=!_{r}x\end{array}$

The realisability doctrine $\mathcal{R}_{A}$ (cf. Example 2.2(3)) is
$R$-graded: for $\alpha\in\mathop{\mathscr{P}{}}(|A|)^{X}$ and $r\in|R|$,
define $\flat_{r}\alpha=x\mapsto\\{!_{r}a\mid a\in\alpha(x)\\}$.

  5. (5)

Let $R$ be a resource semiring and
$\mathbb{W}={\langle{{W,\leq,\circ,\epsilon}}\rangle}$ a monoidal Kripke frame
as in Example 2.2(4). Recall from [DG22] that a lax action of $R$ on
$\mathbb{W}$ is a monotone map ${{a}}:{{|R|\times W}}\rightarrow{{W}}$ such
that

$\begin{array}[]{ll}a_{X}(r,\epsilon)\leq\epsilon&\quad a_{X}(r,w_{1}\circ
w_{2})\leq a_{X}(r,w_{1})\circ a_{X}(r,w_{2})\\\ \epsilon\leq a(0,w)&\quad
a(r,w)\circ a(s,w)\leq a(r+s,w)\\\ w\leq a(1,w)&\quad a(r,a(s,w))\leq a(r\cdot
s,w)\end{array}$

This gives rise to the $R$-graded modality $\overline{a}$ on the primary
linear doctrine $K_{\mathbb{W}}$ of Example 2.2(4) whose component at $X$ maps
$U\in K_{\mathbb{W}}(X)$ to
$\overline{a}_{r}U=\\{{\langle{{x,w}}\rangle}\mid\exists_{v}.\,a(r,v)\leq
w,{\langle{{x,v}}\rangle}\in U\\}$.

$R$-graded doctrines are the objects of the 2-category $\mathbf{LD}_{R}$ where
a 1-arrow from ${\langle{{\mathit{P},\flat}}\rangle}$ to
${\langle{{\mathit{Q},\sharp}}\rangle}$ is a 1-arrow
${{\langle{{F,f}}\rangle}}:{\mathit{P}}\rightarrow{\mathit{Q}}$ in
$\mathbf{LD}$ preserving modalities, that is, for all $r\in|R|$ and object $X$
in the base of $\mathit{P}$, it holds ${\sharp_{r}}_{FX}\circ
f_{X}=f_{X}\circ{\flat_{r}}_{X}$; while 2-arrows, compositions and identities
are those of $\mathbf{LD}$.

Prop. 6 establishes the inclusion $\mathbf{PD}\hookrightarrow\mathbf{LD}_{R}$.

######  Proposition 6.

Let ${\langle{{\mathit{P},\ast,\kappa}}\rangle}$ be a primary linear doctrine
and
${\flat_{r}}:{\mathit{P}}\stackrel{{\scriptstyle\makebox{\kern-0.90417pt{.}}}}{{\rightarrow}}{\mathit{P}}$
be the identity for all $r\in|R|$. Then, $\mathit{P}$ is a primary doctrine
iff $\flat$ is an $R$-graded modality on it.

######  Proof 3.1.

Let $X$ be an object in the base category of $\mathit{P}$ and $\alpha$ an
element in $\mathit{P}(X)$. The left-to-right implication is easy to check:
the non-trivial axiom to verify is weakening, indeed, we have
$\flat_{0}\alpha=\alpha\leq\kappa$, as $\kappa$ is the top element of
$\mathit{P}(X)$. For the converse we have to show that $\kappa$ is the top
element of $\mathit{P}(X)$ and $\alpha\leq\alpha\ast\alpha$ for all
$\alpha\in\mathit{P}(X)$. By weakening $\alpha=\flat_{0}\alpha\leq\kappa$ and
contraction gives
$\alpha=\flat_{r+r}\alpha\leq\flat_{r}\alpha\ast\flat_{r}\alpha=\alpha\ast\alpha$.

A quantitative equality for an $R$-graded doctrine
${\langle{{\mathit{P},\flat}}\rangle}$ is then defined to be a
$\mathit{P}$-distance satisfying an _$R$ -graded substitutivite property_ as
detailed below:

An _$R$ -Lipschitz doctrine_ is a triple
${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ where
${\langle{{\mathit{P},\flat}}\rangle}$ is an $R$-graded doctrine and, for each
object $A$ in the base, $\mathsf{d}_{A}$ is a $\mathit{P}$-distance on $A$
such that, for all objects $A$ and $X$ and $\alpha$ in $\mathit{P}(X\times A)$

  1. (a)

there is an $r$ in $|R|$ such that

${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\ast\flat_{r}{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\mathsf{d}_{A})\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\alpha);$

  2. (b)

$\mathsf{d}_{A\times
X}={\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\mathsf{d}_{A})\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{4}}}\rangle}}(\mathsf{d}_{X})$;

  3. (c)

$\mathsf{d}_{A\times
X}\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\mathsf{d}_{A})$ and
$\mathsf{d}_{A\times
X}\leq{\mathit{P}}_{{\langle{{\pi_{2},\pi_{4}}}\rangle}}(\mathsf{d}_{X})$;

  4. (d)

$\mathsf{d}_{1}=\kappa$.

The key difference between elementary and $R$-Lipschitz doctrines is the
substitutive property, which, taking advantage of graded modalities, in the
latter is stated in a resource sensitive way. Indeed, to prove a substitution,
we need to have _enough equality resources_.

Since symmetry and transitivity are no longer derivable from substitutivity,
for Lipschitz doctrines we assumed $\mathsf{d}_{A}$ to be a
$\mathit{P}$-distance (and not only a reflexive relation), as these are
natural properties for equality.

The product $A\times B$ mimics the concatenation of the context $A$ with the
context $B$, hence axioms (b), (c) and (d) encode the _independence of
contexts_. It allows the independent use of equalities in a product.

In Sect. 5.1 we will describe a construction producing a Lipschitz doctrine
out of any graded doctrine, which will provide us with several examples. For
the moment we consider only the following one:

Denote by $\mathpzc{Met}_{L}$ the category of metric spaces (whose metrics
take values in $[0,\infty]$) and Lipschitz continuous functions. For a metric
space $A$, denote by $|A|$ the underlying set and by $\mathsf{d}_{A}$ the
metric of $A$. Note that $\mathpzc{Met}_{L}$ has finite products where
$|A\times B|=|A|\times|B|$ and $\mathsf{d}_{A\times
B}(x,y,x^{\prime},y^{\prime})=\mathsf{d}_{A}(x,x^{\prime})+\mathsf{d}_{B}(y,y^{\prime})$.
Endow the Lawvere quantale $[0,\infty]$ with the Euclidean metric and let
$\mathit{Lip}(A)$ be the set of Lipschitz continuous functions from a metric
space $A$ to $[0,\infty]$. Each $\mathit{Lip}(A)$ is an ordered commutative
monoid where the order and the operations are defined pointwise. If
${{f}}:{{A}}\rightarrow{{B}}$ and ${{\alpha}}:{{B}}\rightarrow{{[0,\infty]}}$
are Lipschitz continuous, denote by $\mathit{Lip}(f)(\alpha)$ the composition
${{\alpha f}}:{{A}}\rightarrow{{[0,\infty]}}$. Then
${{\mathit{Lip}}}:{{\mathpzc{Met}_{L}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is a primary linear doctrine. Note that
$\mathsf{d}_{A}\in\mathit{Lip}(A\times A)$ as the inequality
$\mathsf{d}_{A}(x,x^{\prime})+\mathsf{d}_{A}(y,y^{\prime})\geq|\mathsf{d}_{A}(x^{\prime},y^{\prime})-\mathsf{d}_{A}(x,y)|$
holds. Endow $\mathit{Lip}$ with the $\mathbb{R}_{\geq 0}$-graded modality m
which acts as in Example 3.1(3), i.e.
$\textbf{m}_{r}\alpha(x)=r\cdot\alpha(x)$, then
${\langle{{\mathit{Lip},\textbf{m},\mathsf{d}}}\rangle}$ is a Lipschitz
doctrine: indeed every $\alpha\in\mathit{Lip}(X\times A)$ is Lipschitz
continuous, hence there is $r\in[0,\infty)$ such that
$r\cdot\mathsf{d}_{X\times
A}(x,a,x^{\prime},a^{\prime})\geq|\alpha(x^{\prime},a^{\prime})-\alpha(x,a)|$
that, by reflexivity of $\mathsf{d}_{X}$, implies
$r\cdot\mathsf{d}_{A}(a,a^{\prime})\geq|\alpha(x,a^{\prime})-\alpha(x,a)|$ and
this is equivalent to
$\alpha(x,a)+r\cdot\mathsf{d}_{A}(a,a^{\prime})\geq\alpha(x,a^{\prime})$.

Axiom (a), describing substitution, can be equivalently rephrased as follows.

######  Proposition 7.

Let ${\langle{{\mathit{P},\flat}}\rangle}$ be an $R$-graded doctrine and
$\mathsf{d}$ a family of $\mathit{P}$-distances. The following are equivalent:

  1. (1)

${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ is $R$-Lipschitz;

  2. (2)

${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ satisfies axioms of Def. 3.1
where (a) is replaced by the following:

    1. (a’)

for all objects $A$ and $\alpha$ in $\mathit{P}(A)$, there is $r\in|R|$ such
that

${\mathit{P}}_{\pi_{1}}(\alpha)\ast\flat_{r}\mathsf{d}_{A}\leq{\mathit{P}}_{\pi_{2}}(\alpha).$

######  Proof 3.2.

1)$\Rightarrow$2) take as $X$ the terminal object of $\mathpzc{C}$ to get
(a’). 2)$\Rightarrow$1) Take $\alpha$ in $\mathit{P}(X\times A)$, then
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\ast\flat_{r}\mathsf{d}_{X\times
A}\leq{\mathit{P}}_{{\langle{{\pi_{3},\pi_{4}}}\rangle}}(\alpha)$. By (b) one
has
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\alpha)\ast\flat_{r}{\mathit{P}}_{{\langle{{\pi_{2},\pi_{4}}}\rangle}}\mathsf{d}_{A}\leq{\mathit{P}}_{{\langle{{\pi_{3},\pi_{4}}}\rangle}}(\alpha)$.
Reindexing along ${\langle{{\pi_{1},\pi_{2},\pi_{1},\pi_{3}}}\rangle}:X\times
A\times A\to X\times A\times X\times A$ completes the proof.

Axioms (c) and (d) of Def. 3.1 are equivalent to affineness of equality.

######  Proposition 8.

Let ${\langle{{\mathit{P},\flat}}\rangle}$ be an $R$-graded doctrine and
$\mathsf{d}$ be a family of $\mathit{P}$-distances. The following are
equivalent:

  1. (1)

${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ is $R$-Lipschitz;

  2. (2)

$\mathsf{d}$ satisfies the following axioms:

    1. (a”)

axioms (a) and (b) of Def. 3.1 hold,

    2. (b”)

$\mathsf{d}_{A}$ is affine.

######  Proof 3.3.

1)$\Rightarrow$2) follows from $\mathsf{d}_{A\times
1}={\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\mathsf{d}_{A})$ and
$\mathsf{d}_{A\times 1}\leq\mathsf{d}_{1}=\kappa$. 2)$\Rightarrow$1) is
immediate.

The quantitative nature of this notion of equality can be noticed also from
its relationship with reindexing, described by the following proposition.

######  Proposition 9.

Let ${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ be an $R$-Lipschitz
doctrine. For any arrow ${{f}}:{{A_{1}\times...\times A_{n}}}\rightarrow{{B}}$
in the base category of $\mathit{P}$, there are $r_{1},...,r_{n}\in|R|$ such
that

$\flat_{r_{1}}{\mathit{P}}_{{\langle{{\pi_{1},\pi_{n+1}}}\rangle}}(\mathsf{d}_{A_{1}})\ast...\ast\flat_{r_{n}}{\mathit{P}}_{{\langle{{\pi_{n},\pi_{2n}}}\rangle}}(\mathsf{d}_{A_{n}})\leq{\mathit{P}}_{f\times
f}(\mathsf{d}_{B})$

######  Proof 3.4.

For all $i\in 1..n$, let
$\vec{\pi}_{i}={\langle{{\pi_{i},\ldots,\pi_{n}}}\rangle}$. By Def. 3.1((a))
we know that, for all $i\in 1..n$, there is $r_{i}\in|R|$ such that

${\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{i-1},\vec{\pi}_{i},\pi_{n+1},\ldots,\pi_{n+i-1},\vec{\pi}_{i}}}\rangle}}({\mathit{P}}_{f\times
f}(\mathsf{d}_{B}))\ast\flat_{r_{i}}({\mathit{P}}_{{\langle{{\pi_{1},\pi_{n+i}}}\rangle}}(\mathsf{d}_{A_{i}}))\leq{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{i},\vec{\pi}_{i+1},\pi_{n+1},\ldots,\pi_{n+i},\vec{\pi}_{i+1}}}\rangle}}({\mathit{P}}_{f\times
f}(\mathsf{d}_{B}))$

holds in $A_{1}\times\ldots\times A_{n}\times A_{1}\times\ldots\times A_{n}$.
Combining these inequalities, using monotonicity of $\ast$ and tarnsitivity of
$\leq$, we get

${\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n},\pi_{1},\ldots,\pi_{n}}}\rangle}}({\mathit{P}}_{f\times
f}(\mathsf{d}_{B}))\ast\flat_{r_{1}}({\mathit{P}}_{{\langle{{\pi_{1},\pi_{n+1}}}\rangle}}(\mathsf{d}_{A_{1}}))\ast\ldots\ast\flat_{r_{n}}({\mathit{P}}_{{\langle{{\pi_{n},\pi_{2n}}}\rangle}}(\mathsf{d}_{A_{n}}))\leq{\mathit{P}}_{f\times
f}(\mathsf{d}_{B})$

Note that
${\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n},\pi_{1},\ldots,,\pi_{n}}}\rangle}}({\mathit{P}}_{f\times
f}(\mathsf{d}_{B}))={\mathit{P}}_{f\circ{\langle{{\pi
1,\ldots,\pi_{n}}}\rangle}}({\mathit{P}}_{\Delta_{B}}(\mathsf{d}_{B}))$. Then,
the thesis follows because
$\kappa\leq{\mathit{P}}_{f\circ{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}({\mathit{P}}_{\Delta_{B}}(\mathsf{d}_{B}))$
holds by reflexivity of $\mathsf{d}_{B}$.

######  Corollary 10.

Let ${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ be an $R$-Lipschitz
doctrine. For any arrow ${{f}}:{{A}}\rightarrow{{B}}$ in the base category of
$\mathit{P}$, there exists $r\in|R|$ such that
$\flat_{r}\mathsf{d}_{A}\leq{\mathit{P}}_{f\times f}(\mathsf{d}_{B})$.

Corollary 10 describes a condition similar to the Lipschitz condition on maps
between metric spaces and motivates the name in Def. 3.1.

Finally, also $R$-Lipschitz doctrines can be organised into a 2-category
$\mathbf{LLD}_{R}$, whose objects are $R$-Lipschitz doctrines, a 1-arrow from
${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ to
${\langle{{\mathit{Q},\flat^{\prime},\mathsf{d}^{\prime}}}\rangle}$ is 1-arrow
${{\langle{{F,f}}\rangle}}:{{\langle{{\mathit{P},\flat}}\rangle}}\rightarrow{{\langle{{\mathit{Q},\flat^{\prime}}}\rangle}}$
preserving the distance, that is, such that, for each object $A$ in the base
category of $\mathit{P}$, it holds $\mathsf{d}^{\prime}_{FA}=f_{A\times
A}(\mathsf{d}_{A})$, and a 2-arrow from ${\langle{{F,f}}\rangle}$ to
${\langle{{G,g}}\rangle}$ is a 2-arrow
${\theta}:{{\langle{{F,f}}\rangle}}\Rightarrow{{\langle{{G,g}}\rangle}}$ in
$\mathbf{LD}_{R}$.

###  3.2. A deductive calculus for quantitative equality

So far we have seen that theories $\mathcal{T}$ over a signature $L$ generate
syntactic doctrines $Prp_{\mathcal{T}}$. This section describes a calculus
whose associated syntactic doctrine is $R$-Lipschitz.

Assume $R={\langle{{|R|,\preceq,+,\cdot,0,1}}\rangle}$ is a resource semiring
and $L$ a first order signature. A judgment has the form
${\Gamma}\vdash_{\vec{\sigma}}{\phi}$ where $\Gamma=\phi_{1},\ldots,\phi_{k}$
is a finite multiset and $\phi_{1},\ldots,\phi_{k},\phi$ are formulas over $L$
in the context
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$.
We will often omit the context $\vec{\sigma}$ to improve readability.

We first introduce PLLR, a calculus extending the
$(\otimes,\mathbf{1})$-fragment of Linear Logic by a family of modalities
$\mathsf{!}_{r}$, for $r\in|R|$. The front ‘P’ is for primary as its
associated syntactic doctrine is a primary linear doctrine (endowed with an
$R$-graded modality).

Rules of PLLR are a subset of the calculus presented in [BP15], in Fig. 1 we
report only rules for modalities as structural rules and those for $\otimes$
and $\mathbf{1}$ are standard. The first four rules are the graded variant of
standard rules for the bang modality of Linear Logic. Rules [w] and [c] encode
graded structural rules: by weakening we can add formulas marked as not used
(labelled by $0$) and contraction tracks the usage by addition. Rule [der]
tells that hypotheses with grade $1$ can be treated as linear hypotheses and
rule [pro] introduces $\mathsf{!}_{r}$, scaling by $r$ the grades of the
hypotheses. Rule [decr] allows to approximate the usage of a formula following
(contravariantly) the order of the semiring.

*[left=[w],vcenter] Γ ⊢_ ϕ Γ,!_0ψ ⊢_ ϕ *[left=[c],vcenter] Γ,!_rψ,!_sψ ⊢_ ϕ Γ,!_r+s ψ ⊢_ ϕ *[left=[der],vcenter] Γ,ψ ⊢_ ϕ Γ,!_1ψ ⊢_ ϕ *[left=[pro],vcenter] !_s_1ψ_1,…,!_s_nψ_n ⊢_ ϕ !_r⋅s_1ψ_1,…,!_r⋅s_nψ_n ⊢_ !_rϕ *[left=[decr],vcenter] Γ ⊢_ !_sϕ Γ ⊢_ !_rϕ r⪯s

Figure 1. Rules for graded bang modality

To extend PLLR by a quantitative equality, we need to add a resource sensitive
substitution rule. Hence, we need a way to compute for each formula $\phi$ and
variable $x$ the cost (represented as an element of the semiring) of
substituting $x$ in $\phi$. To this end, we first enrich the notion of
signature.

An _$R$ -graded signature_ is a first order signature $L$ where symbols have
an _$R$ -graded arity_, that is, an assignment
$|\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}|$ as
the following:

$\displaystyle|f|={\langle{{r_{1},\sigma_{1}}}\rangle},\ldots,{\langle{{r_{n},\sigma_{n}}}\rangle}\to\tau$
$\displaystyle|p|={\langle{{r_{1},\sigma_{1}}}\rangle},\ldots,{\langle{{r_{n},\sigma_{n}}}\rangle}$

where $f$ and $p$ are a function and a predicate symbol, respectively, and,
$\sigma_{i}$ is the sort of the $i$-th argument, while $r_{i}\in|R|$ says how
much the cost of substituting a variable in the $i$-th position is amplified.
We write $|f|_{i}$ (resp. $|p|_{i}$) in place of $r_{i}$ in the assignments
above.

Denote by $\mathit{V}$ and $\mathit{Trm}$ the sets of variables and terms
inductively constructed from symbols in $L$ in the usual way (using the
standard arity obtained from the graded one by erasing resources). Resources
in the graded arity determines a function
${{\mathsf{gr}}}:{{\mathit{Trm}\times\mathit{V}}}\rightarrow{{|R|}}$ as
follows:

  * •

$\mathsf{gr}(z,x)=0$ if $x\neq z$

  * •

$\mathsf{gr}(x,x)=1$

  * •

$\mathsf{gr}(f(t_{1},\ldots,t_{n}),x)=|f|_{1}\cdot\mathsf{gr}(t_{1},x)+\ldots+|f|_{n}\cdot\mathsf{gr}(t_{n},x)$

Intuitively, $\mathsf{gr}(t,x)$ represents the cost of substituting the
variable $x$ inside the term $t$. Note that $\mathsf{gr}(t,x)$ depends on the
number of occurrences of $x$ in $t$. For instance, if $f_{0}$, $f_{1}(x)$,…,
$f_{n}(x,x,\ldots,x)$ are terms where $|f|_{i}=1$ for all $i\in 0..n$, then
$\mathsf{gr}(f_{i}(x,\ldots,x),x)=1+\ldots+1$ ($i$ times). In particular, for
constants, i.e. function symbols $f$ with no arguments, we always have
$\mathsf{gr}(f,x)=0$.

Denote by $\mathit{Wff}$ the set of well-formed formulas constructed from
symbols in $L$, the equality symbol $\eqcirc$ and using $\otimes$,
$\mathbf{1}$ and $\mathsf{!}_{r}$ as connectives. We extend the function
$\mathsf{gr}$ to a function
${{\mathsf{gr}}}:{{\mathit{Wff}\times\mathit{V}}}\rightarrow{{|R|}}$ mapping a
formula $\phi$ and a variable $x$ to the amount of resources needed to
substitute $x$ in $\phi$:

  * •

$\mathsf{gr}(p(t_{1},\ldots,t_{n}),x)=|p|_{1}\cdot\mathsf{gr}(t_{1},x)+\ldots+|p|_{n}\cdot\mathsf{gr}(t_{n},x))$,

  * •

$\mathsf{gr}(t\eqcirc_{\tau}u,x)=\mathsf{gr}(t,x)+\mathsf{gr}(u,x)$,

  * •

$\mathsf{gr}(\phi\otimes\psi,x)=\mathsf{gr}(\phi,x)+\mathsf{gr}(\psi,x)$,

  * •

$\mathsf{gr}(\mathbf{1},x)=0$,

  * •

$\mathsf{gr}(\mathsf{!}_{r}\phi,x)=r\cdot\mathsf{gr}(\phi,x)$.

Similarly to terms, the cost for substituting the variable $x$ in a formula
$\phi$ depends on the number of occurrences of $x$ in $\phi$. For instance, we
have $\mathsf{gr}(p(x)\otimes p(y),x)=|p|_{1}$, while $\mathsf{gr}(p(x)\otimes
p(x),x)=|p|_{1}+|p|_{1}$. Again, for a predicate symbol $p$ with no arguments,
we have $\mathsf{gr}(p,x)=0$.

The calculus PLLR extended by rules in Fig. 2 will be called LPLLR, where the
first ‘L’ is for Lipschitz.

*[left=[r],vcenter] ⊢_ t≖_τt *[left=[s],vcenter] Γ ⊢_ t≖_τu Γ ⊢_ u≖_τt *[left=[t],vcenter] Γ ⊢_ t≖_τu Δ ⊢_ u≖_τv Γ,Δ ⊢_ t≖_τv *[left=[w-eq],vcenter] Γ ⊢_ ϕ Γ,t≖_τu ⊢_ ϕ *[left=[subst],vcenter] Γ ⊢_ ϕ[t/x] Δ ⊢_ !_gr(ϕ,x) t≖_τu Γ,Δ ⊢_ ϕ[u/x]

Figure 2. Rules for graded equality.

We have rules for reflexivity, symmetry and transitivity of $\eqcirc_{\sigma}$
and a rule for weakening. Note the substitution rule: a substitution is
derivable only if _enough equality resources_ are available. These are
determined by the function $\mathsf{gr}$.

######  Remark 11.

If
$|f|={\langle{{|f|_{1},\sigma_{1}}}\rangle}\ldots{\langle{{|f|_{n},\sigma_{n}}}\rangle}\to\tau$
is the arity of the function symbol $f$, then one can prove the entailment

${\mathsf{!}_{|f|_{1}}(x_{1}\eqcirc_{\sigma_{1}}y_{1}),\ldots,\mathsf{!}_{|f|_{n}}(x_{n}\eqcirc_{\sigma_{n}}y_{n})}\vdash{f(\vec{x})\eqcirc_{\tau}f(\vec{y})}$

where $\vec{x}=x_{1},\ldots,x_{n}$ and $\vec{y}=y_{1},\ldots,y_{n}$.
Interpreting the equality as a distance means that the application of the
function $f$ amplifies the distance between $x_{i}$ and $y_{i}$ by a factor
$|f|_{i}$. Similarly, if $p$ is a predicate symbol of arity
$|p|={\langle{{|p|_{1},\sigma_{1}}}\rangle}\ldots{\langle{{|p|_{n},\sigma_{n}}}\rangle}$,
one can derive the entailment

${p(\vec{x}),\mathsf{!}_{|p|_{1}}(x_{1}\eqcirc_{\sigma_{1}}y_{1}),\ldots,\mathsf{!}_{|p|_{n}}(x_{n}\eqcirc_{\sigma_{n}}y_{n})}\vdash{p(\vec{y})}$

meaning that one has to amplify equality between $x_{i}$ and $y_{i}$ by
$|p|_{i}$ to derive $p(\vec{y})$ from $p(\vec{x})$.

######  Proposition 12.

Let $\mathcal{T}$ be a theory in LPLLR over the $R$-graded signature $L$. The
syntactic doctrine
${{Prp_{\mathcal{T}}}}:{{\mathpzc{Cxt}_{L}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ is an $R$-Lipschitz doctrine with
$R$-graded modality given by $\mathsf{!}$ and a family of distances
$\mathsf{d}^{\eqcirc}$ inductively defined by

$\mathsf{d}^{\eqcirc}_{{\langle{{}}\rangle}}=\mathbf{1}\quad\quad\quad\quad\mathsf{d}^{\eqcirc}_{{\langle{{\vec{\sigma},x_{n+1}:\sigma_{n+1}}}\rangle}}=\mathsf{d}^{\eqcirc}_{\vec{\sigma}}\otimes(x_{n+1}\eqcirc_{\sigma_{n+1}}x^{\prime}_{n+1})$

######  Proof 3.5.

To check that $Prp_{\mathcal{T}}$ is $R$-Lipschitz we first need to prove that
it is $R$-graded where $\otimes$ and $\mathbf{1}$ give the primary linear
structure and $\mathsf{!}$ the $R$-graded modality. The former is known (cf.
Example 2.2(1)), while to prove the latter we need to show that rules in Fig.
1 suffice to derive that $\mathsf{!}$ satisfies axioms listed in Def. 3.1.
Naturality of $\mathsf{!}_{r}$ holdes as it commutes with subsitution, while
its monotonicity easily follows by rules [der] and [pro]. Moreover, weakening,
contraction, counit, comultiplication and controvariance follows immediately
from rules [w], [c], [der], [pro] and [decr]. To show lax-monoidality-2, we
first derive
$\mathsf{!}_{1}\alpha,\mathsf{!}_{1}\beta\vdash\alpha\otimes\beta$ from
$\alpha,\beta\vdash\alpha\otimes\beta$, using rule [der] twice. Then, by rule
[pro], we get
$\mathsf{!}_{r}\alpha,\mathsf{!}_{r}\beta\vdash\mathsf{!}_{r}(\alpha\otimes\beta)$.
Finally, then introducing $\otimes$ on the left, we get
$\mathsf{!}_{r}\alpha\otimes\mathsf{!}_{r}\beta\vdash\mathsf{!}_{r}(\alpha\otimes\beta)$,
as needed. The proof of lax-monoidality-1 is similar: from $\vdash\mathbf{1}$
we derive $\vdash\mathsf{!}_{r}\mathbf{1}$ using [pro] and we conclude
introducing $\mathbf{1}$ on the left.

To prove that $Prp_{\mathcal{T}}$ is $R$-Lipschitz, we have to show that rules
in Fig. 2 imply conditions in Def. 3.1. Rule [w-eq] ensures that
$\mathsf{d}^{\eqcirc}_{\vec{\sigma}}$ is affine for every context
$\vec{\sigma}$, hence, by Prop. 8, it suffices to check only axioms (a) and
(b) of Def. 3.1. Since products in $\mathpzc{Cxt}_{L}$ are given by context
concatenation, axiom (b) is straightforward, by definition of
$\mathsf{d}^{\eqcirc}$. Finally, by Prop. 7, it remains to show that, for
every context
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$
and every formula $\alpha$ in $Prp_{\mathcal{T}}(\vec{\sigma})$, there is $r$
in $|R|$ such that the entailment

$\alpha(x_{1},\ldots,x_{n})\otimes\mathsf{!}_{r}\mathsf{d}^{\eqcirc}_{\vec{\sigma}}\vdash\alpha(y_{1},\ldots,y_{n})$

in the context
${\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n},y_{1}:\sigma_{1},\ldots,y_{n}:\sigma_{n}}}\rangle}$
is provable in $\mathcal{T}$. To this end, first of all, note that, using rule
[subst], for every $\Gamma$ and $i\in 1..n$, from
$\Gamma\vdash\alpha(y_{1},\ldots,y_{i-1},x_{i},\ldots,x_{n})$ and
$\mathsf{!}_{r_{i}}x_{i}\eqcirc_{\sigma_{i}}y_{n}\vdash\mathsf{!}_{r_{i}}x_{i}\eqcirc_{\sigma_{i}}y_{i}$,
we can derive
$\Gamma,\mathsf{!}_{r_{i}}x_{i}\eqcirc_{\sigma_{i}}y_{i}\vdash\alpha(y_{1},\ldots,y_{i},x_{i+1},\ldots,x_{n})$,
where
$r_{i}=\mathsf{gr}(\alpha(y_{1},\ldots,y_{i-1},x_{i},\ldots,x_{n}),x_{i})$.
Therefore, starting from
$\alpha(x_{1},\ldots,x_{n})\vdash\alpha(x_{1},\ldots,x_{n})$ and iteratively
using this fact, we can prove

$\alpha(x_{1},\ldots,x_{n}),\mathsf{!}_{r_{1}}x_{1}\eqcirc_{\sigma_{1}}y_{1},\ldots,\mathsf{!}_{r_{n}}x_{n}\eqcirc_{\sigma_{n}}y_{n}\vdash\alpha(y_{1},\ldots,y_{n})$

Now, observe that, using rule [w-eq], we have
$\mathsf{d}^{\eqcirc}_{\vec{\sigma}}\vdash x_{i}\eqcirc_{\sigma_{i}}y_{i}$,
for all $i\in 1..n$, and, by monotonicity of $\mathsf{!}_{s}$, we get
$\mathsf{!}_{s}\mathsf{d}^{\eqcirc}_{\vec{\sigma}}\vdash\mathsf{!}_{s}x_{i}\eqcirc_{\sigma_{i}}y_{i}$,
for all $s\in|R|$ and $i\in 1..n$. Hence, by cut, we derive

$\alpha(x_{1},\ldots,x_{n}),\mathsf{!}_{r_{1}}\mathsf{d}^{\eqcirc}_{\vec{\sigma}},\ldots,\mathsf{!}_{r_{n}}\mathsf{d}^{\eqcirc}_{\vec{\sigma}}\vdash\alpha(y_{1},\ldots,y_{n})$

Let us set $r=r_{1}+\ldots+r_{n}$. Then, by iteratively applying rule [c] we
get
$\alpha(x_{1},\ldots,x_{n}),\mathsf{!}_{r}\mathsf{d}^{\eqcirc}_{\vec{\sigma}}\vdash\alpha(y_{1},\ldots,y_{n})$,
and so the thesis follows by introducing $\otimes$on the left.

###  3.3. Semantics in $R$-Lipschitz doctrines

The interpretation of a theory in a doctrine is standard [Pit00, Jac01]: it
maps contexts and terms to objects and arrows of the base and formulas to
elements of the fibres, respecting the entailments. The interpretation of
LPLLR in an $R$-Lipschitz doctrine has to be defined with the additional
requirement that $\mathsf{gr}$ agrees with the structure of the doctrine.

Let $L$ be an $R$-graded signature. An _$R$ -graded interpretation_ of $L$
into a $R$-Lipschitz doctrine
${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ assigns to every sort
$\sigma$ an object $\llbracket\sigma\rrbracket$ in the base of $\mathit{P}$,
to every function symbol $f$ of arity
${\langle{{|f|_{1},\sigma_{1}}}\rangle}\ldots{\langle{{|f|_{n},\sigma_{n}}}\rangle}\to\tau$
an arrow ${{\llbracket
f\rrbracket}}:{{\llbracket\sigma_{1}\rrbracket\times\ldots\times\llbracket\sigma_{n}\rrbracket}}\rightarrow{{\llbracket\tau\rrbracket}}$
in the base of $\mathit{P}$ such that

$\prod_{i=1}^{n}\flat_{|f|_{i}}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\llbracket
f\rrbracket\times\llbracket
f\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})$ (3)

and to every predicate symbol $p$ of arity
${\langle{{|p|_{1},\sigma_{1}}}\rangle}\ldots{\langle{{|p|_{n},\sigma_{n}}}\rangle}$
an element $\llbracket p\rrbracket$ in
$\mathit{P}(\llbracket\sigma_{1}\rrbracket\times\ldots\times\llbracket\sigma_{n}\rrbracket)$
such that

${\mathit{P}}_{\mathrm{pr}_{1}}(\llbracket
p\rrbracket)\ast\prod_{i=1}^{n}\flat_{|p|_{i}}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\mathrm{pr}_{2}}(\llbracket
p\rrbracket)$ (4)

where $\mathrm{pr}_{1}={\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}$ and
$\mathrm{pr}_{2}={\langle{{\pi_{n+1},\ldots,\pi_{2n}}}\rangle}$.

Intuitively, we can pick as interpretation of a function symbol $f$ an arrow
$\llbracket f\rrbracket$ for which the cost of substituting the $i$-th
argument is $|f|_{i}$, and similarly for predicate symbols. In other words,
the graded arity of $f$ determines valid Lipschitz constansts for its
interpretation $\llbracket f\rrbracket$.

We can interpret an $\mathbb{R}_{\geq 0}$-graded signature $L$ in the
Lipschitz doctrine ${{\mathit{Lip}}}:{{\mathpzc{Met}_{L}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ presented in Example 3.1. The
interpretation maps sorts to metric spaces, a function symbol $f$ of arity
${\langle{{|f|_{1},\sigma_{1}}}\rangle}\ldots{\langle{{|f|_{n},\sigma_{n}}}\rangle}\to\tau$
to a Lipschitz function ${{\llbracket
f\rrbracket}}:{{\llbracket\sigma_{1}\rrbracket\times\ldots\llbracket\sigma_{n}\rrbracket}}\rightarrow{{\llbracket\tau\rrbracket}}$
whose Lipschitz constant is $|f|_{1}+\ldots+|f|_{n}$ and a predicate symbol
$p$ of arity
${\langle{{|p|_{1},\sigma_{1}}}\rangle}\ldots{\langle{{|p|_{n},\sigma_{n}}}\rangle}$
to a Lipschitz function ${{\llbracket
p\rrbracket}}:{{\llbracket\sigma_{1}\rrbracket\times\ldots\times\llbracket\sigma_{n}\rrbracket}}\rightarrow{{[0,\infty]}}$
whose Lipschitz constant is $|p|_{1}+\ldots+|p|_{n}$.

An $R$-graded interpretation of $L$ induces an interpretation of contexts and
terms in the base of $\mathit{P}$ and an interpretation of formulas in the
fibres of $\mathit{P}$. More precisely, a context
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$ is
interpreted by the product
$\llbracket\vec{\sigma}\rrbracket_{\mathit{Trm}}=\llbracket\sigma_{1}\rrbracket\times\ldots\times\llbracket\sigma_{n}\rrbracket$,
a term $t$ of sort $\tau$ in $\vec{\sigma}$ by an arrow ${{\llbracket
t\rrbracket_{\mathit{Trm}}}}:{{\llbracket\vec{\sigma}\rrbracket_{\mathit{Trm}}}}\rightarrow{{\llbracket\tau\rrbracket}}$
and a formula $\phi$ in $\vec{\sigma}$ by an element
$\llbracket\phi\rrbracket_{\mathit{Wff}}\in\mathit{P}(\llbracket\vec{\sigma}\rrbracket_{\mathit{Trm}})$,
as follows:

$\displaystyle\llbracket x_{i}\rrbracket_{\mathit{Trm}}$
$\displaystyle=\pi_{i}$ $\displaystyle\llbracket
f(t_{1},\ldots,t_{n})\rrbracket_{\mathit{Trm}}$ $\displaystyle=\llbracket
f\rrbracket\circ{\langle{{\llbracket
t_{1}\rrbracket_{\mathit{Trm}},\ldots,\llbracket
t_{n}\rrbracket_{\mathit{Trm}}}}\rangle}$ $\displaystyle\llbracket
p(t_{1},\ldots,t_{n})\rrbracket_{\mathit{Wff}}$
$\displaystyle={\mathit{P}}_{{\langle{{\llbracket
t_{1}\rrbracket_{\mathit{Trm}},\ldots,\llbracket
t_{n}\rrbracket_{\mathit{Trm}}}}\rangle}}(\llbracket p\rrbracket)$
$\displaystyle\llbracket\phi\otimes\psi\rrbracket_{\mathit{Wff}}$
$\displaystyle=\llbracket\phi\rrbracket_{\mathit{Wff}}\ast\llbracket\psi\rrbracket_{\mathit{Wff}}$
$\displaystyle\llbracket\mathbf{1}\rrbracket_{\mathit{Wff}}$
$\displaystyle=\kappa$
$\displaystyle\llbracket\mathsf{!}_{r}\phi\rrbracket_{\mathit{Wff}}$
$\displaystyle=\flat_{r}\llbracket\phi\rrbracket_{\mathit{Wff}}$
$\displaystyle\llbracket t\eqcirc_{\tau}u\rrbracket_{\mathit{Wff}}$
$\displaystyle={\mathit{P}}_{{\langle{{\llbracket
t\rrbracket_{\mathit{Trm}},\llbracket
u\rrbracket_{\mathit{Trm}}}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})$

An $R$-graded interpretation of a theory $\mathcal{T}$ of LPLLR over $L$, is
an $R$-graded interpretation
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket$
of $L$ such that
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Wff}}$
respects entailments in $\mathcal{T}$.

We will often omit subscripts $\mathit{Trm}$ and $\mathit{Wff}$ from
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket$
when these are clear. If $\Gamma$ is a list of formulas
$\phi_{1},...,\phi_{n}$ then $\llbracket\Gamma\rrbracket$ abbreviates
$\llbracket\phi_{1}\rrbracket\ast...\ast\llbracket\phi_{n}\rrbracket$.

The following theorem states soundness for the semantics of LPLLR.

######  Theorem 13.

Let
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket$
be an $R$-graded interpretation of a theory $\mathcal{T}$ in LPLLR over $L$
into an $R$-Lipschitz ${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$. Then,
${{\langle{{\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Trm}},\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Wff}}}}\rangle}}:{{\langle{{Prp_{\mathcal{T}},\mathsf{!},\mathsf{d}^{\eqcirc}}}\rangle}}\rightarrow{{\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}}$
is a 1-arrow in $\mathbf{LLD}_{R}$.

The proof is carried out by the usual induction on rules [Pit00, Jac01],
relying on the following lemma:

######  Lemma 14.

For every $R$-graded interpretation
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket$
of $L$ into ${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ we have:

  1. (1)

for any term $t:\tau$ in the context
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$

$\prod_{i=1}^{n}\flat_{\mathsf{gr}(t,x_{i})}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\llbracket
t\rrbracket\times\llbracket
t\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})$

  2. (2)

for any formula $\phi$ in the context
$\vec{\sigma}={\langle{{x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n}}}\rangle}$

${\mathit{P}}_{\mathrm{pr}_{1}}(\llbracket\phi\rrbracket)\ast\prod_{i=1}^{n}\flat_{\mathsf{gr}(\phi,x_{i})}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\mathrm{pr}_{2}}(\llbracket\phi\rrbracket)$

where $\mathrm{pr}_{1}={\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}$ and
$\mathrm{pr}_{2}={\langle{{\pi_{n+1},\ldots,\pi_{2n}}}\rangle}$.

######  Proof 3.6.

1) is proved by induction on $t:\sigma$. If $t:\sigma$ is a variable in
$\vec{\sigma}$, i.e. $t:\sigma$ is $x_{p}:\sigma_{p}$ for $1\leq p\leq n$,
then $\llbracket t\rrbracket$ is the projection
$\pi_{p}:\llbracket\sigma_{1}\rrbracket\times....\times\llbracket\sigma_{n}\rrbracket\to\llbracket\sigma_{p}\rrbracket$
and $\mathsf{gr}(t,x_{j})=1$ if $p=j$ and is $0$ if $p\not=j$, so
$\flat_{\mathsf{gr}(t,x_{j})}\mathsf{d}_{\llbracket\sigma_{j}\rrbracket}\leq\kappa$
(for $j\not=p$ by weakening of $\flat$) and
$\flat_{\mathsf{gr}(t,x_{p})}\mathsf{d}_{\llbracket\sigma_{p}\rrbracket}\leq\mathsf{d}_{\llbracket\sigma_{p}\rrbracket}$
(by counit of $\flat$), so

$\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(t,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{{\langle{{\pi_{p},\pi_{n+p}}}\rangle}}(\flat_{\mathsf{gr}(t,x_{p})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})$

whence the claim as
${\langle{{\pi_{p},\pi_{n+p}}}\rangle}=\pi_{p}\times\pi_{p}=\llbracket
t\rrbracket\times\llbracket t\rrbracket$.

Suppose $t:\tau$ is of the form $f(t_{1},...,t_{m})$ where $f$ is a function
symbol of arity $\tau_{1},....,\tau_{m}\to\tau$, and each $t_{k}$ is a term of
type $\tau_{k}$ in the context $\sigma_{1},...,\sigma_{n}$, satisfying the
inductive hypothesis, i.e.

$\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(t_{k},x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\llbracket
t_{k}\rrbracket\times\llbracket
t_{k}\rrbracket}(\mathsf{d}_{\llbracket\tau_{k}\rrbracket})$

Multiply both sides by $\flat_{|f|_{k}}$ and use comultiplication of $\flat$
to get

$\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{|f|_{k}\cdot\mathsf{gr}(t_{k},x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\llbracket
t_{k}\rrbracket\times\llbracket
t_{k}\rrbracket}(\flat_{|f|_{k}}\mathsf{d}_{\llbracket\tau_{k}\rrbracket})$

From $\llbracket t_{k}\rrbracket\times\llbracket
t_{k}\rrbracket={\langle{{\pi_{k},\pi_{m+k}}}\rangle}\circ({\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket
t_{m}\rrbracket}}\rangle}\times{\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket t_{m}\rrbracket}}\rangle})$ one has

${\mathit{P}}_{\llbracket t_{k}\rrbracket\times\llbracket
t_{k}\rrbracket}(\flat_{|f|_{k}}\mathsf{d}_{\llbracket\tau_{k}\rrbracket})={\mathit{P}}_{{\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket
t_{m}\rrbracket}}\rangle}\times{\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket
t_{m}\rrbracket}}\rangle}}{\mathit{P}}_{{\langle{{\pi_{k},\pi_{m+k}}}\rangle}}(\flat_{|f|_{k}}\mathsf{d}_{\llbracket\tau_{k}\rrbracket})$

The way in which the interpretation of an $R$-graded signature is defined
ensures the satisfaction of inequality (3) for $f$.

$\prod_{k=1}^{m}{\mathit{P}}_{{\langle{{\pi_{k},\pi_{m+k}}}\rangle}}(\flat_{|f|_{k}}\mathsf{d}_{\llbracket\tau_{k}\rrbracket})\leq{\mathit{P}}_{\llbracket
f\rrbracket\times\llbracket
f\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})$

Since $\llbracket t\rrbracket=\llbracket
f(t_{1},...,t_{m})\rrbracket=\llbracket f\rrbracket\circ{\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket t_{m}\rrbracket}}\rangle}$, evaluating both
side of the inequality along ${\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket
t_{m}\rrbracket}}\rangle}\times{\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket t_{m}\rrbracket}}\rangle}$ one has

$\prod_{k=1}^{m}{\mathit{P}}_{\llbracket t_{k}\rrbracket\times\llbracket
t_{k}\rrbracket}(\flat_{|f|_{k}}\mathsf{d}_{\llbracket\tau_{k}\rrbracket})\leq{\mathit{P}}_{\llbracket
t\rrbracket\times\llbracket
t\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})$

whence

$\prod_{k=1}^{m}\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{|f|_{k}\cdot\mathsf{gr}(t_{k},x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\llbracket
t\rrbracket\times\llbracket
t\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})$

finally recall that
$\mathsf{gr}(t,x_{i})=|f|_{1}\cdot\mathsf{gr}(t_{1},x_{i})+...+|f|_{m}\cdot\mathsf{gr}(t_{m},x_{i}))$.
Contraction of $\flat$ completes the proof.

2) If $\phi$ is $p(t_{1},...,t_{m})$ where $p$ predicate symbol of $L$ of
arity $\tau_{1},...,\tau_{m}$ and $t_{i}$ is a term of $L$ of arity
$\sigma_{1},...,\sigma_{n}\to\tau_{i}$, then
$\mathsf{gr}(p,x_{i})=|p|_{1}\cdot\mathsf{gr}(t_{1},x_{i})+...+|p|_{n}\cdot\mathsf{gr}(t_{n},x_{i})$.
Condition displayed in (4) together with contraction of $\flat$ gives

${\mathit{P}}_{\mathrm{pr}_{1}}(\llbracket
p\rrbracket)\ast\prod_{i=1}^{n}\flat_{\mathsf{gr}(\phi,x_{i})}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{\mathrm{pr}_{2}}(\llbracket
p\rrbracket)$

where $\mathrm{pr}_{1}={\langle{{\pi_{1},\ldots,\pi_{m}}}\rangle}$ and
$\mathrm{pr}_{2}={\langle{{\pi_{m+1},\ldots,\pi_{2m}}}\rangle}$.

The reindexing of both sides along ${\langle{{\llbracket
t_{1}\rrbracket,...,\llbracket t_{m}\rrbracket}}\rangle}$ yields that the
right hand side, that becomes
${\mathit{P}}_{{\langle{{\pi_{n+1},\ldots,\pi_{2n}}}\rangle}}(\llbracket\phi\rrbracket)$,
is greater or equal to the left hand side, that becomes

${\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\phi\rrbracket)\ast\prod_{k=1}^{m}{\mathit{P}}_{{\langle{{\pi_{k},\pi_{n+k}}}\rangle}}(\flat_{\mathsf{gr}(p,x_{k})}{\mathit{P}}_{\llbracket
t_{k}\rrbracket\times\llbracket
t_{k}\rrbracket}\mathsf{d}_{\llbracket\tau_{k}\rrbracket})$

By point 1) of this proposition, the displayed formula is greater than or
equal to

${\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\phi\rrbracket)\ast\prod_{k=1}^{m}\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{1},\pi_{n+1}}}\rangle}}(\flat_{\mathsf{gr}(p,x_{k})\cdot\mathsf{gr}(t_{k},x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})$

recall that
$\mathsf{gr}(\phi,x_{i})=|p|_{1}\cdot\mathsf{gr}(t_{1},x_{i})+...+|p|_{m}\cdot\mathsf{gr}(t_{m},x_{i})$,
so contraction of $\flat$ leads to the claim.

If $\phi$ is $t\eqcirc_{\tau}u$ where $tu$ are terms of arity
$\sigma_{1},...,\sigma_{n}\to\tau$, then
$\llbracket\phi\rrbracket={\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})$ and
$\mathsf{gr}(\phi,x_{i})=\mathsf{gr}(t,x_{i})+\mathsf{gr}(u,x_{i})$, so by of
$\flat$ and conditions on $t$ and $u$ it holds that

$\displaystyle{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}{\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})\ast\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(\phi,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})$
$\displaystyle\leq\ $
$\displaystyle{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}{\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})\ast{\mathit{P}}_{\llbracket
t\rrbracket\times\llbracket
t\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})\ast{\mathit{P}}_{\llbracket
u\rrbracket\times\llbracket
u\rrbracket}(\mathsf{d}_{\llbracket\tau\rrbracket})$ $\displaystyle\leq\ $
$\displaystyle{\mathit{P}}_{{\langle{{\pi_{n+1},\ldots,\pi_{2n}}}\rangle}}{\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})$

by transitivity of $\mathsf{d}_{\llbracket\tau\rrbracket}$.

If $\phi$ is $\psi\otimes\theta$ where both $\psi$ and $\theta$ are well
formed formulas in the context $\vec{\sigma}$ satisfying the inductive
hypothesis, then
$\llbracket\phi\rrbracket=\llbracket\psi\rrbracket\ast\llbracket\theta\rrbracket$
and
$\mathsf{gr}(\phi,x_{i})=\mathsf{gr}(\psi,x_{i})+\mathsf{gr}(\theta,x_{i})$.
By contraction of $\flat$, it follows

$\displaystyle{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\psi\rrbracket\ast\llbracket\theta\rrbracket)\ast\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(\psi,x_{i})+\mathsf{gr}(\theta,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})$
$\displaystyle\leq\ $
$\displaystyle{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\psi\rrbracket\ast\llbracket\theta\rrbracket)\ast\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(\psi,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket}\ast\flat_{\mathsf{gr}(\theta,x_{i})})\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})$
$\displaystyle=\ $
$\displaystyle{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\psi\rrbracket)\ast\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(\psi,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})]\ast{\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\theta\rrbracket)\ast\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(\theta,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})$

By hypothesis on $\psi$ the firs formulas in the square brackets is less than
or equal to
${\mathit{P}}_{{\langle{{\pi_{n+1},\ldots,\pi_{2n}}}\rangle}}(\llbracket\psi\rrbracket)$
and the same for $\theta$, whence the claim.

If $\phi$ is 1 then $\mathsf{gr}(\phi,x_{i})=0$. Then
$\llbracket\textbf{1}\rrbracket=\kappa$ and the claim is trivial by weakening
fo $\flat$.

If $\phi$ is $\mathsf{!}_{r}\psi$ for some well formed formula $\psi$ in the
context $\vec{\sigma}$, then
$\llbracket\phi\rrbracket=\flat_{r}\llbracket\psi\rrbracket$ and
$\mathsf{gr}(\phi,x_{i})=r\cdot\mathsf{gr}(\psi,x_{i})$. By the hypothesis on
$\psi$ it is

${\mathit{P}}_{{\langle{{\pi_{1},\ldots,\pi_{n}}}\rangle}}(\llbracket\psi\rrbracket)\ast\prod_{i=1}^{n}{\mathit{P}}_{{\langle{{\pi_{i},\pi_{n+i}}}\rangle}}(\flat_{\mathsf{gr}(\psi,x_{i})}\mathsf{d}_{\llbracket\sigma_{i}\rrbracket})\leq{\mathit{P}}_{{\langle{{\pi_{n+1},\ldots,\pi_{2n}}}\rangle}}(\llbracket\psi\rrbracket)$

It suffices to multiply both sides by $\flat_{r}$ and use comultiplication of
$\flat$ to prove the claim.

We can now sketch the proof of Theorem 13.

######  Proof 3.7 (Proof of Theorem 13).

The only non-trivial part of the theorem is to prove that every component of
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Wff}}$
is monotone. As we said before, this is done by induction on rules of LPLLR.
We check only cases for [pro] and [subst], leaving the other to the reader.

[pro]:

Suppose
$\llbracket\mathsf{!}_{s_{1}}\psi_{1}\rrbracket\ast...\ast\llbracket\mathsf{!}_{s_{n}}\psi_{n}\rrbracket\leq\llbracket\phi\rrbracket$.
By definition of
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Wff}}$,
the left hand side of the inequality is equal to
$\flat_{s_{1}}\llbracket\psi_{1}\rrbracket\ast...\ast\flat_{s_{n}}\llbracket\psi_{n}\rrbracket$.
Then, by monotonicity of $\flat_{r}$, we get
$\flat_{r}(\flat_{s_{1}}\llbracket\psi_{1}\rrbracket\ast...\ast\flat_{s_{n}}\llbracket\psi_{n}\rrbracket)\leq\flat_{r}\llbracket\phi\rrbracket$.
By lax-monoidality-2 and comultiplication we get $\flat_{r\cdot
s_{1}}\llbracket\psi_{1}\rrbracket\ast\ldots\ast\flat_{r\cdot
s_{n}}\llbracket\psi_{n}\rrbracket\leq\flat_{r}\llbracket\phi\rrbracket$.
Finally, again by definition of
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Wff}}$,
we get the thesis.

[subst]:

Consider a context $\vec{\sigma}$, a sort $\tau$, terms $t$, $u$ of sort
$\tau$ in the context $\vec{\sigma}$ and a formula $\phi$ in the context
$\vec{\sigma},x:\tau$. Suppose that
$\llbracket\Gamma\rrbracket\leq\llbracket\phi[t/x]\rrbracket$ and
$\llbracket\Delta\rrbracket\leq\llbracket\mathsf{!}_{\mathsf{gr}(\phi,x)}t\eqcirc_{\tau}u\rrbracket$.
By definition we have
$\llbracket\phi[t/x]\rrbracket={\mathit{P}}_{{\langle{{\mathrm{id}_{\llbracket\vec{\sigma}\rrbracket},\llbracket
t\rrbracket}}\rangle}}(\llbracket\phi\rrbracket)$ and
$\llbracket\mathsf{!}_{\mathsf{gr}(\phi,x)}t\eqcirc_{\tau}u\rrbracket={\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\flat_{\mathsf{gr}(\phi,x)}\mathsf{d}_{\llbracket\tau\rrbracket})$.
Combining these inequalities, we get

$\llbracket\Gamma,\Delta\rrbracket=\llbracket\Gamma\rrbracket\ast\llbracket\Delta\rrbracket\leq{\mathit{P}}_{{\langle{{\mathrm{id}_{\llbracket\vec{\sigma}\rrbracket},\llbracket
t\rrbracket}}\rangle}}(\llbracket\phi\rrbracket)\ast{\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})$

Using Item (2) of Lemma 14 and reflexivity of equality predicates, the
following inequality holds in the poset
$\mathit{P}(\llbracket\vec{\sigma}\rrbracket\times\llbracket\tau\rrbracket\times\llbracket\tau\rrbracket)$:
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{2}}}\rangle}}(\llbracket\phi\rrbracket)\ast\flat_{\mathsf{gr}(\phi,x)}{\mathit{P}}_{{\langle{{\pi_{2},\pi_{3}}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})\leq{\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\llbracket\phi\rrbracket)$,
and, reindexing along
${{{\langle{{\mathrm{id}_{\llbracket\vec{\sigma}\rrbracket},\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}}:{{\llbracket\vec{\sigma}\rrbracket}}\rightarrow{{\llbracket\vec{\sigma}\rrbracket\times\llbracket\tau\rrbracket\times\llbracket\tau\rrbracket}}$,
we obtain

${\mathit{P}}_{{\langle{{\mathrm{id}_{\llbracket\vec{\sigma}\rrbracket},\llbracket
t\rrbracket}}\rangle}}(\llbracket\phi\rrbracket)\ast\flat_{\mathsf{gr}(\phi,x)}{\mathit{P}}_{{\langle{{\llbracket
t\rrbracket,\llbracket
u\rrbracket}}\rangle}}(\mathsf{d}_{\llbracket\tau\rrbracket})\leq{\mathit{P}}_{{\langle{{\mathrm{id}_{\llbracket\vec{\sigma}\rrbracket},\llbracket
u\rrbracket}}\rangle}}(\llbracket\phi\rrbracket)$

Putting together these inequalities and by definition of
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket_{\mathit{Wff}}$
we get the thesis.

######  Remark 15.

Recall from Example 3.3 that an $\mathbb{R}_{\geq 0}$-graded signature can be
interpreted into the Lipschitz doctrine
${{\mathit{Lip}}}:{{\mathpzc{Met}_{L}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$. The equality predicate $\eqcirc_{\tau}$
is interpreted as the metric $\mathsf{d}_{\llbracket\tau\rrbracket}$ of the
space $\llbracket\tau\rrbracket$. This implies that replicability of equality
is not derivable in LPLLR, as it would imply
$\mathsf{d}_{\llbracket\tau\rrbracket}(x,y)\geq\mathsf{d}_{\llbracket\tau\rrbracket}(x,y)+\mathsf{d}_{\llbracket\tau\rrbracket}(x,y)$
which needs not to be true for a generic metric space
$\llbracket\tau\rrbracket$.

The following proposition states completeness of the semantics of LPLLR in the
sense of [Pit00].

######  Proposition 16.

Let $\mathcal{T}$ be a theory in LPLLR over a signature $L$ and $\phi,\psi$
formulas over $L$. If, for all $R$-Lipschitz doctrines
${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$ and for all interpretations
$\llbracket\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\rrbracket$
of $\mathcal{T}$ in ${\langle{{\mathit{P},\flat,\mathsf{d}}}\rangle}$, we have
$\llbracket\phi\rrbracket_{\mathit{Wff}}\leq\llbracket\psi\rrbracket_{\mathit{Wff}}$,
then ${\phi}\vdash{\psi}$ is provable in $\mathcal{T}$.

The proof of this result is straightforward, as we can take the trivial
interpretation in the syntactic doctrine $Prp_{\mathcal{T}}$, which is
$R$-Lipschitz

######  Remark 17.

One could prove a stronger completeness result, showing an _internal language
theorem_. This consists in proving the equivalence between the 2-category of
$R$-Lipschitz doctrines and a suitable 2-category of LPLLR theories. As it is
well-known, the key lemma of this kind of results shows that from any doctrine
one can extract a theory, where, loosely speaking, sorts and function symbols
are objects and arrows in the base, while predicate symbols and axioms are
elements and entailments in the fibres. One could do this for $R$-Lipschitz
doctrines, where the difficult part is to determine grades in the $R$-graded
arities. This is achieved thanks to Prop. 9 with the use of the axiom of
choice. A rigorous proof is left for future work.

##  4\. Examples from quantitative equational theories and beyond

Mardare et al. [MPP16, MPP17] introduced the notion of _quantitative
equational theory_ (QET) as a formal tool to describe and reason about
quantitative algebras, that is, algebras whose carrier is a metric space and
whose operations are non-expansive maps. In this section, we show how the
calculus LPLLR and its semantics can be used to reason about quantitative
algebras, comparing it with QETs and obtaining at the same time a range of
examples of LPLLR theories. In the literature [MPP16, MPP17, MPP21, Adá22,
BMPP18], QETs are studied in great detail using the language of monads and
proving many completeness results. Here, we just focus on examples,
illustrating how LPLLR works, leaving for future work a formal and systematic
comparison between LPLLR and QETs.

We first recall the key features of a QET. Syntactically, terms are built out
from a single-sorted signature $\Omega$ of possibly infinitary function
symbols, we write $f:I\in\Omega$, where $I$ is a set, when $f$ is a function
symbol in $\Omega$ whose arity is $I$. In order to deal with distances, the
key idea is to explicitly handle quantities, by working with labelled
equations $t\eqcirc_{\epsilon}u$, where $\epsilon$ is a non-negative rational
number. Such an equation states that the distance between $t$ and $u$ is
bounded by $\epsilon$. A sequent has the shape $\Gamma\vdash
t\eqcirc_{\epsilon}u$, where $\Gamma$ is a possibly infinite set of equations,
and the calculus is defined by the following rules, where $f:I\in\Omega$ and
$\sigma$ is a substitution.

(Refl) $\displaystyle\vdash t\eqcirc_{0}t$ (NExp)
$\displaystyle\\{t_{i}\eqcirc_{\epsilon}u_{i}\mid i\in I\\}\vdash
f((t_{i})_{i\in I})\eqcirc_{\epsilon}f((u_{i})_{i\in I})$ (Sym) $\displaystyle
t\eqcirc_{\epsilon}u\vdash u\eqcirc_{\epsilon}t$ (Subst)
$\displaystyle\Gamma\vdash t\eqcirc_{\epsilon}u\ \text{implies}\
\sigma(\Gamma)\vdash\sigma(t)\eqcirc_{\epsilon}\sigma(u)$ (Triang)
$\displaystyle\\{t\eqcirc_{\epsilon}u,u\eqcirc_{\epsilon^{\prime}}v\\}\vdash
t\eqcirc_{\epsilon+\epsilon^{\prime}}v$ (Assum) $\displaystyle\text{if}\
t\eqcirc_{\epsilon}u\in\Gamma,\ \text{then}\ \Gamma\vdash
t\eqcirc_{\epsilon}u$ (Arch)
$\displaystyle\\{t\eqcirc_{\epsilon^{\prime}}u\mid\epsilon^{\prime}>\epsilon\\}\vdash
t\eqcirc_{\epsilon}u$ (Cut) $\displaystyle\text{if}\ \Gamma\vdash\psi\
\text{for all $\psi\in\Theta$ and}\ \Theta\vdash t\eqcirc_{\epsilon}u,$
$\displaystyle\text{then}\ \Gamma\vdash t\eqcirc_{\epsilon}u$

A first crucial difference between a QET and LPLLR is that the underling logic
of the former is not linear, as contraction and weakening are derivable: the
hypotheses $\Gamma$ form a set, the rule (Cut) is in additive form and the
rule (Assum) disregards some hypotheses. As a consequence, each formula in a
QET has to be interpreted in a standard non-quantitative way, e.g. as a
subset, while in LPLLR every formula admits a direct quantitative
interpretation e.g., as $[0,\infty]$-valued function. Therefore, to reason
quantitatively, in a QET one has to deal with an infinite family of predicates
(i.e. labelled equations) representing all possible approximations of a
metric, which requires an explicit handling of quantities. On the other hand,
in LPLLR one has a single equality predicate which is directly interpreted as
a $[0,\infty]$-valued metric. Working with explicit quantities makes it
necessary to add specific rules to manage them (such as (Arch)) and to allow
sequents with infinitely many hypotheses. Note also that infinitary sequents
are needed to deal with infinitary function symbols, which are allowed in
QETs, while LPLLR only deals with finitary ones to keep sequents finitary as
well.

Another important difference is that in QETs function symbols are forced to be
non-expansive by the rule (NExp), while in LPLLR they can be arbitrary
Lipschitz functions. Since non-expansive maps are Lipschitz with constant
equal to $1$, LPLLR can treat them, but, as we will see, it can go beyond this
limitation, dealing with quantitative algebras where operations are arbitrary
Lipschitz functions.

Remaining rules are instead similar: rules (Refl), (Sym) and (Triang) above
formalise the axioms of a distance and correspond to rules [r], [s] and [t] of
LPLLR, while rules (Subst) and (Cut) correspond to monotonicity of
substitution and the cut rule of LPLLR.

We now focus on examples. Examples in [MPP16] can be rephrased as LPLLR
theories where $R$ is the semiring $\mathbb{R}_{\geq 0}$ of non-negative real
numbers, in such a way that their intended semantics induces a sound
interpretation of the corresponding LPLLR theory in the doctrine of metric
spaces and Lipschitz maps (cf. Example 3.1). We will shorten notation for
functions symbols in a single-sorted graded signature: if $f$ is a function
symbol with
$|f|={\langle{{r_{1},\star}}\rangle}\ldots{\langle{{r_{n},\star}}\rangle}\to\star$,
we write $f:{\langle{{r_{1},\ldots,r_{n}}}\rangle}$.

We start by considering the theory QS0 of quantitative semilattices with zero.
To write QS0 as a QET, one takes a signature whose function symbols are $+:2$
and $0:0$, while, to write QS0 as an LPLLR theory, one takes a
$\mathbb{R}_{\geq 0}$-graded signature with one sort, no predicate symbols and
whose function symbols are $+:{\langle{{1,1}}\rangle}$ and
$0:{\langle{{}}\rangle}$, meaning that $+$ is non-expansive in both arguments.
In Fig. 3, we list on the left the axioms of QS0 given in [MPP16] and on the
right the corresponding ones in LPLLR.

$\begin{array}[]{lll}&\text{QET}&\text{LPLL${}_{R}$}\\\
\textbf{\small(S0)}&\vdash x+0\eqcirc_{0}x&\vdash x+0\eqcirc x\\\
\textbf{\small(S1)}&\vdash x+x\eqcirc_{0}x&\vdash x+x\eqcirc x\\\
\textbf{\small(S2)}&\vdash x+y\eqcirc_{0}y+x&\vdash x+y\eqcirc y+x\\\
\textbf{\small(S3)}&\vdash(x+y)+z\eqcirc_{0}x+(y+z)&\vdash(x+y)+z\eqcirc
x+(y+z)\\\
\textbf{\small(S4)}&\\{x\eqcirc_{\epsilon}x^{\prime},y\eqcirc_{\epsilon^{\prime}}y^{\prime}\\}\vdash
x+y\eqcirc_{\epsilon\lor\epsilon^{\prime}}x^{\prime}+y^{\prime}&\end{array}$

Figure 3. Axioms for quantitative semigroups as a QET and as an LPLLR theory.

The axiom (S0) says that the distance between $x+0$ and $x$ is less than $0$.
This information in LPLLR is given forcing $\mathbf{1}\vdash x+0\eqcirc x$,
thanks to the fact that $\mathbf{1}$ is interpreted as the function constantly
equal to $0$. Axioms (S1), (S2) and (S3) are translated similarly. Axiom (S4)
in the QET refines the non-expansiveness of $+$ and it is needed to properly
handle labels of equations. Since in LPLLR there are no labels, this axiom is
not needed, as non-expansiveness of $+$ follows from rules of LPLLR and the
graded arity in the considered signature. Note that the axioms in LPLLR are
the usual ones of the theory of semilattices: $+$ is associative, commutative
and idempotent and $0$ is the neutral element.

A semantics for QS0 as QET is given in [MPP16] as follows. Let
${\langle{{M,d}}\rangle}$ be a metric space and consider the metric space
${\langle{{C_{d},H_{d}}}\rangle}$ where $C_{d}$ the set of compact subsets of
$M$ with respect to $d$ and $H_{d}(A,B)=\max\\{\sup_{a\in A}d(a,B),\sup_{b\in
B}d(b,A)\\}$, with $d(m,X)=\inf_{x\in X}d(m,x)$ for $m\in M$ and $X\subseteq
M$, is the Hausdorff distance. Then, $0$ is interpreted as the empty set and
$+$ as the function of type
${\langle{{C_{d},H_{d}}}\rangle}\times{\langle{{C_{d},H_{d}}}\rangle}\rightarrow{\langle{{C_{d},H_{d}}}\rangle}$
mapping two compact sets to their union. This assignment gives rise to a
semantics also of QS0 seen as an LPLLR theory in the $\mathbb{R}_{\geq
0}$-Lipschitz doctrine
${{\mathit{Lip}}}:{{\mathpzc{Met}_{L}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$ (cf. Example 3.1). We interpret a context
with $n$ variables as the product of $n$ copies of
${\langle{{C_{d},H_{d}}}\rangle}$ and a term with $n$ free variables as a
Lipschitz function from ${\langle{{C_{d},H_{d}}}\rangle}^{n}$ to
${\langle{{C_{d},H_{d}}}\rangle}$.

Other examples discussed in [MPP16] deal with metrics over probability
distributions. The considered theories are defined over a signature whose
function symbols are $+_{e}:2$ for all $e\in[0,1]$, which can be thought of as
probabilistic choice operators with probability $e$, that is, intuitively,
$x+_{e}y$ is $x$ with probability $e$ and $y$ with probability $1-e$. The QET
IBAp of $p$-Interpolative Barycentric Algebras, with $p\geq 1$, can be
rephrased in LPLLR using a single-sorted $\mathbb{R}_{\geq 0}$-graded
signature with no predicate symbols and whose function symbols are
$+_{e}:{\langle{{e^{1/p},(1-e)^{1/p}}}\rangle}$ for all $e\in[0,1]$, meaning
that $+_{e}$ scales the distance of the first argument by a factor $e^{1/p}$
and that of the second argument by a factor $(1-e)^{1/p}$. We report the
axioms in Fig. 4.

$\begin{array}[]{lll}&\text{QET}&\text{LPLL${}_{R}$}\\\
\textbf{\small(B1)}&\vdash x+_{1}y\eqcirc_{0}x&\vdash x+_{1}y\eqcirc x\\\
\textbf{\small(B2)}&\vdash x+_{e}x\eqcirc_{0}x&\vdash x+_{e}x\eqcirc x\\\
\textbf{\small(SC)}&\vdash x+_{e}y\eqcirc_{0}y+_{1-e}x&\vdash x+_{e}y\eqcirc
y+_{1-e}x\\\
\textbf{\small(SA)}&\vdash(x+_{e}y)+{e^{\prime}}z\eqcirc_{0}x+_{ee^{\prime}}(y+_{\frac{e^{\prime}-ee^{\prime}}{1-ee^{\prime}}}z)&\vdash(x+_{e}y)+_{e^{\prime}}z\eqcirc
x+_{ee^{\prime}}(y+_{\frac{e^{\prime}-ee^{\prime}}{1-ee^{\prime}}}z)\\\
\textbf{\small(IB${}_{p}$)}&\\{x\eqcirc_{\epsilon_{1}}y,x^{\prime}\eqcirc_{\epsilon_{2}}y^{\prime}\\}\vdash
x+_{e}y\eqcirc_{\delta}x^{\prime}+_{e}y^{\prime}&\\\
&\hfill(\delta\geq(e\epsilon_{1}^{p}+(1-e)\epsilon_{2}^{p})^{1/p})&\end{array}$

Figure 4. Axioms for interpolative barycentric algebras as a QET and as an
LPLLR theory.

The axioms are translated as for the theory QS0. The last one has no
counterpart in LPLLR as it essentially states that $+_{e}$ is Lipschitz with
coeficients $e^{1/p}$ and $(1-e)^{1/p}$, 444To check this we rely on the
inequality $(a+b)^{1/p}\leq a^{1/p}+b^{1/p}$, which holds for non-negative
real numbers $a,b$. and this in LPLLR follows from the the fact that $+_{e}$
has gaded arity ${\langle{{e^{1/p},(1-e)^{1/p}}}\rangle}$ and so we can derive
the entailment $\mathsf{!}_{e^{1/p}}x\eqcirc
y,\mathsf{!}_{(1-e)^{1/p}}x^{\prime}\eqcirc y^{\prime}\vdash x+_{e}y\eqcirc
x^{\prime}+_{e}y^{\prime}$.

Mardare et al. [MPP16] define a semantics of this theory taking as domain of
the interpretation the set $\Delta[M]$ of Borel probability measures over a
metric space ${\langle{{M,d}}\rangle}$ with the $p$-Wasserstein distance
$W_{d}^{p}$ defined by

$W_{d}^{p}(\mu,\nu)=\sup\left\\{\left|\int f^{p}\mathsf{d}\mu-\int
f^{p}\mathsf{d}\nu\right|^{1/p}\mid{{f}}:{{M}}\rightarrow{{[0,\infty)}}\
\text{is non-expansive}\right\\}$

and interpreting $+_{e}$ as the convex combination of two distributions, that
is, the function mapping a pair of distributions ${\langle{{\mu,\nu}}\rangle}$
to $e\mu+(1-e)\nu$. This choice, induces an interpretation of the
corresponding LPLLR theory in
${{\mathit{Lip}}}:{{\mathpzc{Met}_{L}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$, as it is easy to see that the convex
combination operation has Lipschitz constants $e^{1/p}$ and $(1-e)^{1/p}$ with
respect to $W_{d}^{p}$.

A specialised version of the theory IBAp is the theory BA of Left-Invariant
Barycnetric Algebras, which is obtained by replacing the axiom (IBp) by the
axiom (LI) stating $\vdash x+_{e}z\eqcirc_{\epsilon}y+_{e}z$ where
$\epsilon\geq e$. This axiom, together with the others, basically requires
that Lipschitz constants of $+_{e}$ are $e$ and $1-e$, but it also forces the
distance to be smaller than $1$. To rephrase this theory in LPLLR, we need to
consider a single-sorted $\mathbb{R}_{\geq 0}$-graded signature where function
symbols are $+_{e}:{\langle{{e,1-e}}\rangle}$, for all $e\in[0,1]$, and having
a constant predicate symbol $\mathsf{u}:{\langle{{}}\rangle}$ modelling the
real number $1$. This matches the intuition that in our setting real numbers
are “truth values”, hence they can be represented syntactically by constant
predicate symbols. Finally, we have to add to the theory above the axiom
$\mathsf{u}\vdash x\eqcirc y$, stating that the distance is smaller than $1$.
Note that, using the rules of LPLLR, we can prove
$\mathsf{!}_{\epsilon}\mathsf{u}\vdash x\eqcirc x+_{e}z\eqcirc y+_{e}z$, for
all $\epsilon\geq e$, which corresponds exactly to the axiom (LI).

Following again [MPP16], a semantics of the theory BA in the Lipschitz
doctrine
$\mathit{D}_{{\langle{{\mathop{\mathscr{P}{}}_{[0,\infty]},\textbf{m}}}\rangle}}$
can be constructed by taking as interpretation of the sort the set
$\Delta[S,\Sigma]$ of probability measures over a measurable space
${\langle{{S,\Sigma}}\rangle}$, with the total variation distance
$T(\mu,\nu)=\sup_{E\in\Sigma}|\mu(E)-\nu(E)|$, and interpreting $+_{e}$ again
as the convex combination of distributions.

###  4.1. Beyond QETs

As already noticed, in QETs function symbols must be interpreted by non-
expansive maps due to the rule (NExp). The calculus LPLLR, instead, can
express theories where function symbols have to be interpreted by arbitrary
Lipschitz maps. As examples of such situation, we briefly describe the
theories $\mathbb{R}$-MVS, of metric vector spaces over the field $\mathbb{R}$
of real numbers, and $R$-GC, of $R$-graded combinators over a given resource
semiring $R$, which, therefore, cannot be expressed as QETs.

The single-sorted $\mathbb{R}_{\geq 0}$-graded signature of $\mathbb{R}$-MVS
has no predicate symbols and consists of function symbols
$+:{\langle{{1,1}}\rangle}$, $-:{\langle{{1}}\rangle}$ and
$0:{\langle{{}}\rangle}$ for the group structure and
$\lambda_{a}:{\langle{{|a|}}\rangle}$ for scalar multiplication by $a$, for
all $a\in\mathbb{R}$. Note that the scalar multiplication $\lambda_{a}$ is
required to scale the distance by a factor $|a|$, hence in general it is not
non-expansive; indeed, the entailment $\mathsf{!}_{|a|}x\eqcirc
y\vdash\lambda_{a}(x)\eqcirc\lambda_{a}(y)$ is provable. Below we report the
axioms:

(G1) $\displaystyle\vdash(x+y)+z\eqcirc x+(y+z)$ (L1)
$\displaystyle\vdash\lambda_{a}(x+y)\eqcirc\lambda_{a}(x)+\lambda_{a}(y)$ (G2)
$\displaystyle\vdash x+y\eqcirc y+x$ (L2)
$\displaystyle\vdash\lambda_{a+b}(x)\eqcirc\lambda_{a}(x)+\lambda_{b}(x)$ (G3)
$\displaystyle\vdash x+0\eqcirc x$ (L3)
$\displaystyle\vdash\lambda_{ab}(x)\eqcirc\lambda_{a}(\lambda_{b}(x))$ (G4)
$\displaystyle\vdash x+(-x)\eqcirc 0$ (L4)
$\displaystyle\vdash\lambda_{1}(x)\eqcirc x$

These axioms are actually the standard ones for vector spaces, the only
difference is that the underlying calculus is substructural, hence equality
can be interpreted as a distance. Any real vector space $V$ with a norm
$\|\mathchoice{\mbox{--}}{\mbox{--}}{\mbox{\scriptsize--}}{\mbox{\tiny--}}\|$
gives a semantics for this theory: the distance $d(u,v)=\|u-v\|$ makes the
group operations non-expansive and the scalar multiplication by $a$ a
Lipschitz function with constant $|a|$ as $\|au-av\|=|a|\cdot\|u-v\|$.

Another example where function symbols are not necessarily non-expansive is
the theory $R$-GC of $R$-graded combinators an $R$-Linear Combiantory Algebra
[Atk18] (see also Example 3.1(4)) over a given resource semiring $R$. The
single-sorted $R$-graded signature of $R$-GC has no predicate symbols,
function symbols $\cdot:{\langle{{1,1}}\rangle}$ and
$\mathsf{b}_{r}:{\langle{{r}}\rangle}$,555We use $\mathsf{b}_{r}$ instead of
the more standard $!_{r}$ to avoid confusion with the modality of the logical
calculus. for all $r\in|R|$, constants $B,C,I,K,W_{r,s},D,d_{r,s},F_{r}$, for
all $r,s\in|R|$, and $O_{r,s}$, for all $r,s\in|R|$ with $r\preceq s$. The
symbol $\mathsf{b}_{r}$ has grade $r$ as, intuitively, the expression
$\mathsf{b}_{r}t$ provides “$r$ copies of $t$”, hence, the cost of a
substitution inside $\mathsf{b}_{r}$ should be amplified by $r$. Indeed, as a
consequence of the rules of LPLLR the entailment ${\mathsf{!}_{r}t\eqcirc
u}\vdash{\mathsf{b}_{r}t\eqcirc\mathsf{b}_{r}u}$ is derivable. The axioms of
the theory are the following:

(GC1) $\displaystyle\vdash((B\cdot x)\cdot y)\cdot z\eqcirc x\cdot(y\cdot z)$
(GC2) $\displaystyle\vdash((C\cdot x)\cdot y)\cdot z\eqcirc(x\cdot z)\cdot y$
(GC3) $\displaystyle\vdash I\cdot x\eqcirc x$ (GC4)
$\displaystyle\vdash(K\cdot x)\cdot\mathsf{b}_{0}y\eqcirc x$ (GC5)
$\displaystyle\vdash(W_{r,s}\cdot
x)\cdot\mathsf{b}_{r+s}\eqcirc(x\cdot\mathsf{b}_{r}y)\cdot\mathsf{b}_{s}y$
(GC6) $\displaystyle\vdash D\cdot\mathsf{b}_{1}x\eqcirc x$ (GC7)
$\displaystyle\vdash d_{r,s}\cdot\mathsf{b}_{r\cdot
s}x\eqcirc\mathsf{b}_{r}(\mathsf{b}_{s}x)$ (GC8)
$\displaystyle\vdash(F_{r}\cdot\mathsf{b}_{r}x)\cdot\mathsf{b}_{r}y\eqcirc\mathsf{b}_{r}(x\cdot
y)$ (GC9) $\displaystyle\vdash
O_{r,s}\cdot\mathsf{b}_{s}x\eqcirc\mathsf{b}_{r}x$

When $R$ is the semiring $\mathbb{R}_{\geq 0}$ of non-negative real numbers,
models of $\mathbb{R}_{\geq 0}$-GC in $\mathit{Lip}$ provide a metric variant
of (total) $\mathbb{R}_{\geq 0}$-Linear Combinatory Algebras [Atk18] (see also
Example 3.1(4)). Hence, equality is interpreted as a metric on cominators,
which could be regarded as a program distance, and, for every
$r\in[0,\infty)$, $\mathsf{b}_{r}$ is interpreted as a Lipschitz map with
constant $r$.

##  5\. The 2-category of Lipschitz doctrines

As we have seen in the previous section, $R$-Lipschitz doctrines are the
objects of the 2-category $\mathbf{LLD}_{R}$. In this section we study its
properties, relating it with with other 2-categories of doctrines. More in
detail, we first show that $R$-Lipschitz doctrines arise as coalgebras for a
2-comonad on $R$-graded ones. This result smoothly generalises what happens in
the non-linear setting and provides us with a universal contruction of
$R$-Lipschitz doctrines from $R$-garded ones. Then, we study how our
quantitative equality relates to the standard one given by left adjoints,
introducing elementary $R$-graded doctrines and comparing them with
$R$-Lipschitz ones.

###  5.1. $R$-Lipschitz doctrines as coalgebras

A key property of standard equality in the non-linear setting, recognise by
[Pas15, EPR20], is that it arises as a coalgebra structure over a primary
doctrine, that is, a doctrine modelling conjunctions. More precisely, consider
Diagram 1 from Sect. 2

$\textstyle{\mathbf{ED}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\top}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathbf{PD}}$

It shows an adjoint situation between $\mathbf{PD}$ and $\mathbf{ED}$, i.e.
the 2-categories of primary doctrines and that of elementary ones that is,
primary doctrines with equality. That adjoint situation is comonadic. This
fact not only reveals the coalgebraic nature of equality, but provides a
universal construction yielding elementary doctrines from primary ones.

The goal of this subsection is to generalise this fact to our linear setting.
That is, we present a universal construction producing a Lipschitz doctrine
out of any $R$-graded one. To this end, we define a 2-functor
${{\mathrm{R_{Lip}}}}:{{\mathbf{LD}_{R}}}\rightarrow{{\mathbf{LLD}_{R}}}$ that
is the right 2-adjoint of the obvious forgetful 2-functor
${{\mathrm{U_{Lip}}}}:{{\mathbf{LLD}_{R}}}\rightarrow{{\mathbf{LD}_{R}}}$ and
prove that $R$-Lipschitz doctrines are the coalgebras of the 2-comonad induced
by such a 2-adjunction. On one hand, this result provides us with a universal
construction of $R$-Lipschitz doctrines, which gives us a tool to produce
semantics for the calculus LPLLR. On the other hand, it shows that our
quantitative notion of equality, although not falling within Lawvere’s
definition by left adjoints (Prop. 5), generalises it and preserves its
coalgebraic nature.

To construct $\mathrm{R_{Lip}}$, for any $R$-graded doctrine
${\langle{{\mathit{P},\flat}}\rangle}$, we build an $R$-Lipschitz doctrine
${{\mathit{D}_{{\langle{{\mathit{P},\flat}}\rangle}}}}:{{\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}^{\mbox{\scriptsize
op}}}}\rightarrow{{\mathpzc{Pos}}}$, called _Lipschitz completion_ of
${\langle{{\mathit{P},\flat}}\rangle}$. Let $\mathpzc{C}$ be the base of
$\mathit{P}$. The category
$\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}$ is defined as follows:

  * •

objects are pairs ${\langle{{A,\rho}}\rangle}$ where $A$ is an obect in
$\mathpzc{C}$ and $\rho$ is an affine $\mathit{P}$-distance on $A$;

  * •

an arrow from ${\langle{{A,\rho}}\rangle}$ to ${\langle{{B,\sigma}}\rangle}$
is an arrow ${{f}}:{{A}}\rightarrow{{B}}$ in $\mathpzc{C}$ such that
$\flat_{r}\rho\leq{\mathit{P}}_{f\times f}(\sigma)$, for some $r\in|R|$;

  * •

composition and identities are those of $\mathpzc{C}$.

Given
${{f}}:{{{\langle{{A,\rho}}\rangle}}}\rightarrow{{{\langle{{B,\sigma}}\rangle}}}$
we say that $r\text{ tracks }f$ if $r$ is such that
$\flat_{r}\rho\leq{\mathit{P}}_{f\times f}(\sigma)$. So
${{f}}:{{A}}\rightarrow{{B}}$ underlies an arrow
${{f}}:{{{\langle{{A,\rho}}\rangle}}}\rightarrow{{{\langle{{B,\sigma}}\rangle}}}$
if there is $r$ that tracks $f$.

Intuitively, objects of $\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}$
can be regarded as metric spaces inside $\mathit{P}$ and its arrows as
abstract Lipschitz functions between such spaces. It is easy to see that
$\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}$ is a category: identities
are well-defined as, for every ${\langle{{A,\rho}}\rangle}$, the identity
$\mathrm{id}_{A}$ is tracked by $1$ thanks to the counit axiom of $\flat$;
also composition is well defined as, if $r\text{ tracks }f$ and $s\text{
tracks }g$, then $s\cdot r\text{ tracks }gf$ by comultiplication and
naturality of $\flat_{s}$

$\flat_{s\cdot
r}\rho\leq\flat_{s}\flat_{r}\rho\leq\flat_{s}{\mathit{P}}_{f\times
f}(\sigma)={\mathit{P}}_{f\times f}(\flat_{s}\sigma)\leq{\mathit{P}}_{f\times
f}({\mathit{P}}_{g\times g}(\tau))$

Given elements $\rho\in\mathit{P}(A\times A)$ and $\sigma\in\mathit{P}(B\times
B)$, we denote by $\rho\boxtimes\sigma$ the element
${\mathit{P}}_{{\langle{{\pi_{1},\pi_{3}}}\rangle}}(\rho)\ast{\mathit{P}}_{{\langle{{\pi_{2},\pi_{4}}}\rangle}}(\sigma)$
in $\mathit{P}(A\times B\times A\times B)$.

The proof of the following proposition is straightforward.

######  Proposition 18.

Let ${\langle{{\mathit{P},\ast,\kappa}}\rangle}$ be a primary linear doctrine.
If $\rho$ and $\sigma$ are $\mathit{P}$-distances, then $\rho\boxtimes\sigma$
is a $\mathit{P}$-distance. If $\rho$ and $\sigma$ are affine, then
$\rho\boxtimes\sigma$ is affine.

Relying on this property, we can prove the following result.

######  Proposition 19.

The category $\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}$ has finite
products.

######  Proof 5.1.

A terminal object is ${\langle{{1,\kappa_{1\times 1}}}\rangle}$, where $1$ is
a terminal object in $\mathpzc{C}$. Indeed, for any object
${\langle{{A,\rho}}\rangle}$ in
$\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}$, the unique map
${{t_{A}}}:{{A}}\rightarrow{{1}}$ in $\mathpzc{C}$, induces a map from
${\langle{{A,\rho}}\rangle}$ to ${\langle{{1,\kappa_{1\times 1}}}\rangle}$
since by weakening it holds $\flat_{0}\rho\leq\kappa_{A\times
A}={\mathit{P}}_{t_{A}\times t_{A}}(\kappa_{1\times 1})$. Given
${\langle{{A,\rho}}\rangle}$ and ${\langle{{B,\sigma}}\rangle}$ in
$\mathpzc{L}_{{\langle{{\mathit{P},\flat}}\rangle}}$, the pair
${\langle{{A\times B,\rho\boxtimes\sigma}}\rangle}$ is an object in