# From Identity to Difference: A Quantitative Interpretation of the Identity
Type

Paolo Pistone
Università di Bologna, Italy
<EMAIL_ADDRESS>
###### Abstract

We explore a quantitative interpretation of 2-dimensional intuitionistic type
theory (ITT) in which the identity type is interpreted as a “type of
differences”. We show that a fragment of ITT, that we call difference type
theory (dTT), yields a general logical framework to talk about quantitative
properties of programs like approximate equivalence and metric preservation.
To demonstrate this fact, we show that dTT can be used to capture
compositional reasoning in presence of errors, since any program can be
associated with a “derivative” relating errors in input with errors in output.
Moreover, after relating the semantics of dTT to the standard weak
factorization systems semantics of ITT, we describe the interpretation of dTT
in some quantitative models developed for approximate program transformations,
incremental computing, program differentiation and differential privacy.

##  1 Introduction

### From Program Equivalence to Program Differences

In program semantics, a classical problem is to know whether two programs
behave in _the same_ way in all possible contexts. Yet, in several fields of
computer science, especially those involving numerical and probabilistic forms
of computation (like e.g. machine learning), it is often more important to be
able to describe to which extent two programs behave in a _similar_ , although
non equivalent, way. Hence, a crucial aspect is to be able to measure the
change in the overall result that is induced by the replacement of a (say,
computationally expensive) program by some (more efficient but only)
approximately correct one.

These observations have motivated much research on denotational semantics
involving _metric_ and _differential_ aspects, that is, in which one can
measure differences between programs, as well as their capacity of amplifying
errors. For instance, it has been observed that a fundamental property for a
protocol to ensure _differential privacy_ [30, 7, 15] is that the associated
program is not too _sensitive_ to errors; this has led to an elegant semantics
[5] where types are interpreted as metric spaces and programs are interpreted
by functions with bounded derivative (i.e.  _Lipschitz-continuous_ functions).
More generally, the recent literature in theoretical computer science has seen
the blossoming of many different notions of “derivative” for higher-order
programming languages, each accounting for some differential aspect of
computation: from connections with linearity (e.g. the _differential
$\lambda$-calculus_ [14, 9, 10]) to incremental computation [11, 1, 3], from
higher-order automatic differentiation [21, 27] to higher-order approximate
program transformations [36, 13, 23].

Do all these differential approaches share a common logic? Is there some
common notion of “derivative” for higher-order programs? In this paper we
argue that a proper fragment of standard intuitionistic type theory (ITT in
the following), that we call _difference type theory_ ($\mathrm{dTT}$ in
short) provides a convenient framework to formalize the compositional
reasoning about program derivatives found in some of these semantics.

### The Identity Type

Our quantitative approach to intuitionistic type theory relies on a non-
standard interpretation of the identity type. When Martin-Löf introduced ITT
[26], the identity type $I_{A}(t,u)$ was one of its main novelties. Under the
Curry-Howard correspondence, the elements of $I_{A}(t,u)$ were interpreted as
proofs of the fact that $t$ and $u$ denote the same object of type $A$. The
introduction rule for the identity type constructs an object
$\mathsf{refl}(t)\in I_{A}(t,t)$ for all $t\in A$, witnessing the equality
$t=t\in A$; instead, the elimination rule provides a computational
interpretation of Leibniz’s indiscernibles principle by justifying a form of
_transport of identity_ : from an equality proof $p\in I_{A}(t,u)$ and a proof
$q\in\mathcal{C}(t,t,\mathsf{refl}(t))$, one can construct a proof
$\mathsf{J}(t,u,p,q)$ of $\mathcal{C}(t,u,p)$.

As is well-known, ITT comes in two flavors: in the _extensional_ version one
has rules for passing to and from $p\in I_{A}(t,u)$ and $t=u\in A$, i.e.
saying that a proof of $I_{A}(t,u)$ exists precisely when $t=u\in A$ holds;
with these rules, one can show that any element of $I_{A}(t,u)$, if any, is of
the form $\mathsf{refl}(t)$. In the _intensional_ version these additional
rules are not present (with the significant advantage that type-checking
becomes decidable), and this leaves space for non-standard interpretations, as
we will see.

In more recent times, a new wave of interest in intensional ITT has spread in
connection with an interpretation relating it to homotopy theory [34]: by
exploiting the transport of identity principle, one can prove that the
dependent type $I_{A}(x,y)$ carries the structure of a _groupoid_ (i.e. a
category with invertible arrows), and that proofs $f:A\to B$ lift to
_functors_ $I_{A}(f):I_{A}(x,y)\to I_{B}(f(x),f(y))$ between the respective
groupoids. This is the basic ground for a suggestive and well-investigated
interpretation, where $I_{A}(t,u)$ becomes the space of _homotopies_ between
$t$ and $u$.

While the original semantics of ITT based on _locally cartesian closed
category_ [20] validates the extensionality rules (which make the homotopy
interpretation trivial), an elegant semantics for intensional ITT has been
established since [16, 4, 35] based on the theory of _weak factorization
systems_ , providing the basis for the construction of various homotopy-
theoretic models.

### The Type of Differences

Without extensionality, there can be different ways of proving $I_{A}(t,u)$,
as we saw. What if these were not seen as ways of proving that $t$ and $u$
denote the same object, but rather as ways of measuring the _difference_
between $t$ and $u$? The main point of this paper is to convince the reader
that this idea is not only consistent, but yields some interesting new
interpretation of (a fragment of) intensional ITT.

For example, in presence of a type $\mathrm{Real}$ of real numbers with
constants $\mathbf{r}$ for all $r\in\mathbb{R}$, we might wish to interpret an
element $a\in I_{\mathrm{Real}}(\mathbf{r},\mathbf{s})$ as a difference
between $\mathbf{r}$ and $\mathbf{s}$, that is, as a positive real greater or
equal to $|r-s|$. The introduction rule produces the element
$\mathsf{refl}(\mathbf{r})=\mathbf{0}\in
I_{\mathrm{Real}}(\mathbf{r},\mathbf{r})$, the _self-distance_ of
$\mathbf{r}$; the interpretation of the elimination rule is more delicate, as
this rule makes reference to arbitrary predicates; yet, let us consider a
predicate of the form $\mathcal{C}(x,y,p)=I_{\mathrm{Real}}(f(x),g(y))$, where
$x,y\in\mathrm{Real}$, $p\in I_{A}(x,y)$ and
$f,g\in\mathrm{Real}\to\mathrm{Real}$ are two _smooth_ (i.e. infinitely
differentiable) functions. Then given a difference $a\in
I_{\mathrm{Real}}(\mathbf{r},\mathbf{s})$ and a difference $b\in
I_{\mathrm{Real}}(f(\mathbf{r}),g(\mathbf{r}))$ we can obtain a difference
$c\in I_{\mathrm{Real}}(f(\mathbf{r}),g(\mathbf{s}))$ by reasoning as follows:
first, since $g$ is smooth, by standard analytical reasoning (read: the mean
value theorem) we can find some positive real $L_{r,s}$ such that
$L_{r,s}\cdot a\geq L_{r,s}\cdot|r-s|\geq|g(r)-g(s)|\in
I_{\mathrm{Real}}(g(\mathbf{r}),g(\mathbf{s}))$; hence the operation
$r,s,a\mapsto L_{r,s}\cdot a$ yields a way to _transport differences_ between
$r$ and $s$ into differences between $g(r)$ and $g(s)$. This difference can
now be used to produce a difference
$\mathsf{J}(\mathbf{r},\mathbf{s},a,b)=b+L_{r,s}\cdot a\in
I_{\mathrm{Real}}(f(\mathbf{r}),g(\mathbf{s}))$, as required by the
elimination rule applied to $\mathcal{C}(x,y,p)$.

More generally, we will see that by interpreting higher-order programs as
suitably “differentiable” maps, one can justify different kinds of “transport
of difference” arguments, yielding quantitative interpretations of the
elimination rule for the identity type.

### Plan of the Paper

In Section 2 we introduce difference type theory $\mathrm{dTT}$, a fragment of
ITT in which $I_{A}(t,u)$ is seen as a type of differences, and we provide a
short overview of the kind of compositional differential reasoning
formalizable in this system. In Section 3 we introduce a notion of model for
$\mathrm{dTT}$ (that we call a _$\mathrm{dTT}$ -category_), and we prove that
any instance of this notion yields a form of weak factorization system, thus
relating our semantics to the usual semantics of the identity type.

In later sections we sketch some differential models of $\mathrm{dTT}$. In
Sec. 4 we describe the interpretation of a sub-exponential version of
$\mathrm{dTT}$ in the metric semantics used for differential privacy [5],
providing a formal language to express metric preservation. In Sec. 5 we show
that $\mathrm{dTT}$ yields a natural language for differential logical
relations [13, 23, 28], an approach to approximate program transformations in
which program differences are themselves higher-order entities. In Sec. 6 we
provide an interpretation of $\mathrm{dTT}$ in models of higher-order
incremental computing [11], with program differences interpreted as
increments; finally, in Sec. 7 we show an interpretation of $\mathrm{dTT}$ in
models of the differential $\lambda$-calculus [14, 9, 10].

##  2 Difference Type Theory

Let us start with a motivating example: suppose
$\mathtt{H}:(\mathrm{Nat}\to\mathrm{Real})\to\mathrm{Real}$ is a program that
takes a function $\mathtt{f}$ from integers to reals and computes a value
$\widetilde{\mathtt{H}}(\mathtt{f}(0),\dots,\mathtt{f}(N))$ depending on the
first $N+1$ outputs of $\mathtt{f}$. For instance, $\mathtt{H}$ might compute
some aggregated value from a time series $\mathtt{f}$ (e.g. $\mathtt{H}$
computes the average temperature in London from a series of measures taken
from $\mathtt{f}$). Since measuring $\mathtt{f}$ every, say, minute might be
too expensive, it might be worth considering an _approximated_ computation, in
which $\mathtt{f}$ is only measured _every $k$ minutes_, (i.e. $\mathtt{f}$ is
applied only to values $0,k,2k,\dots,\lfloor N/k\rfloor$), and each computed
value is fed to $\widetilde{\mathtt{H}}$ $k$ times (this technique is well-
known under the name of _loop perforation_ [31]).

What is the error we can expect for the replacement of
$\mathtt{H}(\mathtt{f})$ by its approximation? We will show that a fragment of
ITT, that we call _difference type theory_ (in short $\mathrm{dTT}$), can be
used to reason about this kind of situations in a natural and compositional
way.

### The Syntax of $\mathrm{dTT}$

The fragment of ITT we consider in this paper includes two universes of types
$\mathrm{Type}$ and $\mathrm{dType}$ (whose elements will be indicated,
respectively, as $A,B,C,\dots$ and as
$\mathcal{A},\mathcal{B},\mathcal{C},\dots$), with formation rules illustrated
in Fig. 1. In our basic language the types $A\in\mathrm{Type}$ are just usual
_simple types_ (yet in our examples we will often consider extensions or
variants of this language). The types $\mathcal{A}\in\mathrm{dType}$ can
depend on terms of some simple type; we will often refer to them as
_predicates_ ; intuitively, an element of some predicate $\mathcal{A}(t,u)$,
depending on terms $t,u$ of some simple type, will be interpreted as denoting
_differences_ , or _errors_ , between the terms $t,u$.

$A,B\in\mathrm{Type}$ $A\to B,A\times B\in\mathrm{Type}$ $A\in\mathrm{Type}$
$t,u\in A$ $D_{A}(t,u)\in\mathrm{dType}$ $(x\in A)$
$\mathcal{A},\mathcal{B}\in\mathrm{dType}$
$\mathcal{A}\times\mathcal{B}\in\mathrm{dType}$ $A\in\mathrm{Type}$ $(x\in A)$
$\mathcal{C}(x)\in\mathrm{dType}$ $(\Pi x\in
A)\mathcal{C}(x)\in\mathrm{dType}$ $A\in\mathrm{Type}$ $(x,y\in A)$
$\mathcal{C}(x,y)\in\mathrm{dType}$ $(\Pi x,y\in
A)(D_{A}(x,y)\to\mathcal{C}(x,y))\in\mathrm{dType}$

Figure 1: Type formation rules for $\mathrm{dTT}$.

$(x\in A)$ $t\in A\phantom{)}$ $\partial(t)\in D_{A}(t,t)$ $a\in D_{A}(t,u)$
$(x,y\in A$) $\mathcal{C}(x,y)\in\mathrm{dType}$ $(x\in A)$
$b(x)\in\mathcal{C}(x,x)$ $\mathsf{J}(t,u,a,[x]b)\in\mathcal{C}(t,u)$ $t\in A$
$(x\in A)$ $b(x)\in\mathcal{C}(x,x)$ $(\beta)$
$\mathsf{J}(t,t,\partial(t),[x]b)=b[t/x]\in\mathcal{C}(t,t)$ $(x\in A)$ $a\in
D_{A}(t,u)$ $(\eta)$ $\mathsf{J}(t,u,a,[x]\partial(x))=a\in D_{A}(t,u)$

Figure 2: Introduction, elimination and computation rules for $D_{A}(t,u)$.

The introduction, elimination and computation rules of $\mathrm{dTT}$ are
those of standard intuitionistic type theory, restricted to the types of
$\mathrm{dTT}$ (we recall them in the Appendix). We use $D_{A}(t,u)$ instead
of $I_{A}(t,u)$ for the usual identity type, since we are thinking of it as a
_type of differences_. We illustrate in Fig. 2 the rules for the difference
type $D_{A}(t,u)$. Terms are constructed starting from a countable set of
_term variables_ $x,y,z,\dots$ and a countable (disjoint) set of _difference
variables_ $\epsilon,\delta,\theta,\dots$. The rules in Fig. 2 must be read as
dependent on some _context_ , which, for $\mathrm{dTT}$, are of the form
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))$,
where $\mathbf{x}\in\Phi_{0}=(x_{1}\in A_{1},\dots,x_{n}\in A_{n})$ is a
sequence of (non-type dependent) declarations for $A_{i}\in\mathrm{Type}$, and
$\boldsymbol{\epsilon}\in\Phi_{2}(\mathbf{x})=(\epsilon_{1}\in\mathcal{C}_{1}(\mathbf{x}),\dots,\epsilon_{m}\in\mathcal{C}_{m}(\mathbf{x}))$
is a sequence of declarations for
$(\mathbf{x}\in\Phi_{0})\mathcal{C}_{i}(\mathbf{x})\in\mathrm{dType}$.

A term $(\mathbf{z}\in\Phi_{1})t\in A$, where $A\in\mathrm{Type}$, is just an
ordinary $\lambda$-term with pairing. We call such terms _program terms_ and
we use $t,u,v$ for them. We will consider variants of this basic language with
other type and term primitives (e.g. ground types like
$\mathrm{Nat},\mathrm{Bool}$ or the probabilistic monad $\Box A$), as well as
a _sub-exponential_ variant ST$\lambda$C!, with bounded linear types of the
form $!_{k}A\multimap B$ (see [18, 30]), described in the Appendix.

A term
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1})a\in\mathcal{A}$,
for some $(\mathbf{x}\in\Phi_{0})\mathcal{A}\in\mathrm{dType}$ belongs to the
grammar

$a::=\epsilon\mid\lambda x.a\mid at\mid\lambda xy\epsilon.a\mid
atta\mid\langle
a,a\rangle\mid\pi_{1}(a)\mid\pi_{2}(a)\mid\partial(t)\mid\mathsf{J}(t,t,a,[x]a)$

We call such terms _difference terms_ and we will use $a,b,c$ for them.

Intuitively, a term of the form $\partial(t)$ (i.e. $\mathsf{refl}(t)$ in ITT)
indicates the _self-difference_ of $t$. For example, when considering
semantics based on metric spaces, $\partial(t)$ will represent the null error,
i.e. $0$. However, in other models of $\mathrm{dTT}$, $\partial(t)$ needs not
be zero (in fact, 0 is not even part of our basic syntax). In particular, in
the models from Section 5 and 6, for a higher-order function $f\in A\to B$,
$\partial(f)$ will provide a measure of the sensitivity of $f$ (in fact, in
such model $\partial(f)$ coincides with the _derivative_ of $f$, see below).

The terms of the form $\mathsf{J}(t,u,a,[x]b)$ are the main computational
objects (and also the least intuitive) of $\mathrm{dTT}$. The idea behind the
quantitative interpretation of this constructor is that, given self-
differences $b(x)\in\mathcal{C}(x,x)$, $\mathsf{J}$ “transports” an error $a$
between $t$ and $u$, measured in $D_{A}$, onto an error between $t$ and $u$
measured in $\mathcal{C}$. For example, as discussed in the introduction,
$\mathcal{C}(x,y)$ might be the type of differences $D_{B}(fx,gy)$, and
$\mathsf{J}$ will thus transport a difference $a$ between $t$ and $u$ onto a
difference between $ft$ and $gu$.

A fundamental application of $\mathsf{J}$ is the following: for any function
$f\in A\to B$, the _derivative of $f$_ is the following difference term

$\mathsf{D}[f]:=\lambda
xy\epsilon.\mathsf{J}(x,y,\epsilon,[x]\partial(fx))\in(\Pi x,y\in
A)(D_{A}(x,y)\to D_{B}(fx,fy))$

$\mathsf{D}[f]$ tracks errors in input into errors in output of $f$, and can
thus be taken as a measure of the _sensitivity_ of $f$. In the models of
$\mathrm{dTT}$ described in the following sections $\mathsf{D}[f]$ will be
interpreted by different notions of program derivative, including the “true”
derivative of $f$, when the latter encodes a real-valued smooth function.

From the computation rules of $\mathsf{J}$ we deduce the following computation
rules for derivatives:

$\displaystyle\mathsf{D}[f](t,t,\partial(t))$ $\displaystyle=\partial(ft)$
($\beta\mathsf{D}$) $\displaystyle\mathsf{D}[\lambda x.x](t,u,a)$
$\displaystyle=a$ ($\eta\mathsf{D}$)

($\beta\mathsf{D}$) says that the derivative of $f$ computed on the self-
distance of a point is just the self-distance of the image of the point. When
$\mathsf{D}[f]$ is seen as the “true” derivative, the self-distances
$\partial(v)$ are just the null error $0$, and so ($\beta\mathsf{D}$) says
that the derivative computed in $0$ is $0$. ($\eta\mathsf{D}$) says that the
error produced in output by the identity function is just the error in input
(this is in accordance with the analytical intuition too).

Given $f\in A\to B$ and $g\in B\to C$ the composition of $\mathsf{D}[f]$ with
$\mathsf{D}[g]$ yields a difference of type $(\Pi x,y\in A)(D_{A}(x,y)\to
D_{C}(gf(x),gf(y))$. Several models of $\mathrm{dTT}$ will satisfy the _chain
rule_ axiom below, which identifies the latter with the derivative of $g\circ
f$:

$\displaystyle\mathsf{D}[\lambda x.g(fx)]=\lambda
xy\epsilon.\mathsf{D}[g](fx)(fy)(\mathsf{D}[f]xy\epsilon)$
($\mathsf{D}\mathrm{chain}$)

######  Example 2.1.

For all $f\in\mathrm{Nat}\to\mathrm{Real}$, let
$f^{*}\in\mathrm{Nat}\to\mathrm{Real}$ be defined by $f^{*}(2i)=f(i)$ and
$f^{*}(2i+1)=f^{*}(2i)$. The loop perforation of index 2 of $\mathtt{H}(f)$ is
precisely $\mathtt{H}(f^{*})$. We sketch how to construct a difference between
$\mathtt{H}(f)$ and $\mathtt{H}(f^{*})$ in $\mathrm{dTT}$.

The step function $\Delta f(x)=|f(x+1)-f(x)|$ can be defined as $\Delta
f(x)=\mathsf{D}[f](x+1,1)$ (where we take a difference between
$x,y\in\mathrm{Nat}$ to be any positive real $\geq|x-y|$). For all
$x\in\mathrm{Nat}$, the function $d$ with $d(2x)=0$ and $d(2x+1)=\Delta f(2x)$
yields then an element $d\in(\Pi
x\in\mathrm{Nat})D_{\mathrm{Real}}(f(x),f^{*}(x))$. Using this and the
derivative of $\widetilde{\mathtt{H}}$ we can compute a distance $b\in
D_{\mathrm{Real}}({\mathtt{H}}(f),{\mathtt{H}}(f^{*}))$ by
$b=\mathsf{D}[\widetilde{\mathtt{H}}]([f(i),d(i)]_{i=0,\dots,N})$.

More generally, we can construct a function $c\in(\Pi
f,g\in\mathrm{Nat}\to\mathrm{Real})(D_{\mathrm{Nat}\to\mathrm{Real}}(f,g)\to
D_{\mathrm{Real}}({\mathtt{H}}(f),{\mathtt{H}}(g))$: from a distance
$\epsilon\in D_{\mathrm{Nat}\to\mathrm{Real}}(f,g)$ we can deduce a function
$e(\epsilon)\in(\Pi x\in\mathrm{Nat})D_{\mathrm{Real}}(f(x),g(x))$ by letting
$e(\epsilon)=\mathsf{J}(f,g,\epsilon,[x]\partial(f(x)))$, and we define
$c(f,g,\epsilon)$ by replacing $d$ by $e(\epsilon)$ in $b$.

######  Example 2.2 (distance function).

In presence of a type $\mathrm{Bool}$ for Booleans, with constants
$\mathbf{0},\mathbf{1}\in\mathrm{Bool}$ and
$\mathsf{case}_{C}:\mathrm{Bool}\to C\to C\to C$ (with
$\mathsf{Case}_{C}(\mathbf{0},x,y)=x$ and
$\mathsf{Case}_{C}(\mathbf{1},x,y)=y$), and with a constant $\infty\in
D_{\mathrm{Bool}}(\mathbf{0},\mathbf{1})$, it is possible to define a distance
function $d_{A}\in(\Pi x,y\in A)D_{A}(x,y)$ for all simple type $A$, by
letting $d_{A}=\lambda
xy.\mathsf{J}(\mathbf{0},\mathbf{1},\infty,[w]\partial(\mathsf{case}_{A}(w,x,y)))$.
If we admit the equational rule $\mathsf{Case}_{C}(w,x,x)=x$, then using the
Equation ($\mathsf{J}w$) (see below) we can deduce that $d_{A}xx$ coincides
with the self-difference $\partial(x)$.

### Predicates in $\mathrm{dTT}$

An important property of $\mathrm{dTT}$ is that any predicate
$(\mathbf{x}\in\Phi_{0})\mathcal{C}(\mathbf{x})\in\mathrm{dType}$ is obtained
by substitution from a special family of binary predicates, defined below.

######  Definition 2.1.

A predicate is said _pure for $A$_ if it is of the form $(x,y\in
A)\mathcal{C}(x,y)$ and one of the following holds:

  * •

$\mathcal{C}(x,y)=D_{A}(x,y)$;

  * •

$A=B_{1}\times B_{2}$ and
$\mathcal{C}(x,y)=\mathcal{B}_{1}(\pi_{1}(x),\pi_{1}(y))\times\mathcal{B}_{2}(\pi_{2}(x),\pi_{2}(y))$,
where $\mathcal{B}_{1}$ is pure for $B_{1}$ and $\mathcal{B}_{2}$ is pure for
$B_{2}$;

  * •

$A=B\to C$ and $\mathcal{C}(x,y)=(\Pi z\in A)\mathcal{B}(xz,yz)$, where
$\mathcal{B}(z,z^{\prime})$ is pure for $C$;

  * •

$A=B\to B\to C$ and $\mathcal{C}(x,y)=(\Pi x^{\prime},y^{\prime}\in
B)(D_{A}(x^{\prime},y^{\prime})\to\mathcal{B}(xx^{\prime}y^{\prime},yx^{\prime}y^{\prime}))$,
where $\mathcal{B}(x^{\prime},y^{\prime})$ is pure for $C$.

######  Lemma 2.1.

For any predicate $(\mathbf{z}\in\Phi_{0})\mathcal{C}(\mathbf{z})$ there
exists a pure predicate $(x,y\in A)\mathcal{C}^{\flat}(x,y)$ and terms
$(\mathbf{z}\in\Phi_{0})t,u\in A$ such that
$\mathcal{C}(\mathbf{z})=\mathcal{C}^{\flat}(t,u)$.

For example, the predicate $(z\in A,w\in A)(\Pi x\in B)D_{C}(f(z,x),g(z,w,x))$
is obtained from the pure predicate $(y,y^{\prime}\in B\to C)(\Pi x\in
B)D_{C}(yx,y^{\prime}x)$ and the functions $(z\in A,w\in A)\lambda
x.f(z,x),\lambda x.g(z,w,x)\in B\to C$. Lemma 2.1 will play a crucial role in
defining models of $\mathrm{dTT}$: we will start by interpreting pure
predicates, and we will obtain the interpretation of all other predicates by a
_pullback_ operation (corresponding to substitution).

######  Remark 2.1.

In standard ITT, the identity type $I_{A}(\\_,\\_)$ yields a _groupoid_ 111In
fact, one obtains a groupoid by considering elements $p\in I_{A}(t,u)$ up to
the equivalence induced by 3-dimensional homotopies in $I_{I_{A(t,u)}}(p,q)$.,
i.e. a category with invertible arrows. In $\mathrm{dTT}$ one can only prove
that $D_{A}(\\_,\\_)$ has the structure of a _deductive system_ (i.e. a _non-
associative_ category, see [24]) in which for each arrow $a\in D_{A}(t,u)$
there is a “transpose” arrow $a^{*}\in D_{A}(u,t)$, with
$\partial(t)^{*}=\partial(t)$.

######  Remark 2.2.

In some formulation of intuitionistic type theory (e.g. see [20]) one finds a
stronger version of the $\eta$-rule, which in the fragment $\mathrm{dTT}$
would read as follows:

$a\in D_{A}(t,u)$ $(x\in A,y\in A\mid\epsilon\in D_{A}(x,y))$
$c(x,y,\epsilon)\in\mathcal{C}(x,y)$
$\mathsf{J}(t,u,a,[x]c(x,x,\partial(x)))=c(t,u,a)\in\mathcal{C}(t,u)$
($\mathsf{J}\eta^{+}$)

However, in presence of ($\mathsf{J}\eta^{+}$) one can deduce that
$a=\partial(t)\in D_{A}(t,t)$222 This is proved as follows: by letting
$c(x,y,\epsilon)=\epsilon$ and $d(x,y,\epsilon)=\partial(x)$, from
$c(x,x,\partial(x))=d(x,x,\partial(x))$, we deduce
$a=c(t,t,a)=\mathsf{J}_{\mathcal{C}}(t,t,a,[x]c(x,x,\partial(x)))=\mathsf{J}_{\mathcal{C}}(t,t,a,[x]d(x,x,\partial(x)))=d(t,t,a)=\partial(t)$.
holds for all $t\in A$ and $a\in D_{A}(t,t)$, hence trivializing the
interpretation of $D_{A}(x,x)$. Moreover, we can see that the rule also
trivializes the interpretation of $\mathsf{D}[f]$ as the “true” derivative,
since it implies $\mathsf{D}[f]=\lambda x.\partial(fx)$333It suffices to take
$c(x,y,\epsilon)=\partial(fx)$. (i.e. $\mathsf{D}[f]=\lambda x.0$ when
$\partial(v)$ is interpreted as the null error).

However, the following instance of ($\mathsf{J}\eta^{+}$) is valid in all
models we consider:

$\displaystyle\mathsf{J}(t,u,a,[x]b)=b\qquad(x\notin\mathrm{FV}(b))$
($\mathsf{J}w$)

### Function Extensionality

In ITT the function extensionality axiom essentially asserts that from a proof
that $f$ and $g$ send identical points into identical points, one can
construct a proof that $f$ is identical to $g$. In the following sections we
will consider models which satisfy two variants of this axiom, namely

$\displaystyle D_{A\to B}(f,g)$ $\displaystyle\equiv(\Pi x\in
A)D_{B}(f(x),g(x))$ ($\mathsf{FExt1}$) $\displaystyle D_{A\to B}(f,g)$
$\displaystyle\equiv(\Pi x,y\in A)(D_{A}(x,y)\to D_{B}(f(x),g(y)))$
($\mathsf{FExt2}$)

Axioms ($\mathsf{FExt1}$) (resp. ($\mathsf{FExt2}$)) says that a difference
between two functions $f,g\in A\to B$ is the same as a map from a point $x\in
A$ into a difference between $f(x)$ and $g(x)$ in $B$ (resp. a map from a
difference $\epsilon$ between two points of $A$ into differences between their
respective images). Observe that, without these axioms, one can still
construct programs

$\displaystyle\mathsf{E}_{1}$ $\displaystyle\in(\Pi f,g\in A\to B)(D_{A\to
B}(f,g)\to(\Pi x\in A)D_{B}(f(x),g(x)))$ $\displaystyle\mathsf{E}_{2}$
$\displaystyle\in(\Pi f,g\in A\to B)(D_{A\to B}(f,g)\to(\Pi x,y\in
A)(D_{A}(x,y)\to D_{B}(f(x),g(y))))$

given by $\mathsf{E}_{1}=\lambda fg\phi x.\mathsf{J}(f,g,\phi,[h]\lambda
x.\partial(f(x)))$ and $\mathsf{E}_{2}=\lambda fg\delta
xy\epsilon.\mathsf{J}(f,g,\varphi,[h]\mathsf{D}[h])$.

Moreover, some of the models we consider will also satisfy the axiom below

$D_{A\times B}(t,u)\equiv D_{A}(\pi_{1}(t),\pi_{1}(u))\times
D_{B}(\pi_{2}(t),\pi_{2}(u))$ ($\mathsf{CExt}$)

stating that a difference between pairs is a pair of differences. Even without
($\mathsf{CExt}$), one can construct terms $\mathsf{C}_{1},\mathsf{C}_{2}$ to
and from the types above (yet they do not define an isomorphism).

In presence of one or more of the extensionality axioms, it makes sense to
consider further computational rules for the operators $\mathsf{J}$ and
$\mathsf{D}$ (for instance, the rule stating that for a higher-order function
$f\in A\to B$, $\partial(f)=\mathsf{D}[f]$), that we discuss in the Appendix.

##  3 Models of $\mathrm{dTT}$ and Weak Factorization Systems

The by now standard semantics of the identity type is based on _weak
factorization systems_ (in short, WFS). A WFS is a category endowed with two
classes of arrows $\mathcal{L}$ and $\mathcal{R}$, such that any arrow
factorizes as the composition of a $\mathcal{L}$-arrow and a
$\mathcal{R}$-arrow (the typical example is $\mathrm{Set}$, with $\mathcal{L}$
being the class of surjective functions and $\mathcal{R}$ the class of
injective functions).

The goal of this section is to introduce a workable notion of model for
$\mathrm{dTT}$, as formal basis for the concrete models illustrated in the
next sections, and to relate it to the standard WFS semantics of ITT. We will
first present a basic setting, that we call a _$\mathrm{dTT}$ -category_,
which allows for the interpretation of $\mathrm{dTT}$ (and roughly follows
[35]). We then introduce a slight variant of WFS, that we call _$U$ -WFS_,
where $U$ is some monoidal functor. This variant is adapted to the ontology of
$\mathrm{dTT}$, where one has two distinct families of terms, and only
requires that the ($U$-image of the) arrows from the first family factor
through the arrows of the second family. We finally show that any
$\mathrm{dTT}$-category gives rise to a $U$-WFS.

The fundamental example of a $\mathrm{dTT}$-category will be the _context
category_ of $\mathrm{dTT}$, that is, the category $\mathsf{Ctx}$ with objects
being contexts and arrows
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\to(\mathbf{y}\in\Psi_{0}\mid\boldsymbol{\delta}\in\Psi_{1}(\mathbf{y}))$
being sequences $(\mathbf{t}\mid\mathbf{a})$ of ($\beta\eta$-equivalence
classes of) terms such that $(\mathbf{x}\in\Phi_{0})t_{i}\in A_{i}$ and
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))a_{j}\in\mathcal{C}_{j}(\mathbf{t})$
holds for all $A_{i}\in\mathrm{Type}$ occurring in $\Psi_{0}$ and
$\mathcal{C}_{j}(\mathbf{x})\in\mathrm{dType}$ occurring in $\Psi_{1}$. We let
$\mathsf{Ctx}_{0}$ be the full subcategory of $\mathsf{Ctx}$ made of contexts
of the form $(\mathbf{x}\in\Phi_{0}\mid)$, and
$\iota:\mathsf{Ctx}_{0}\to\mathsf{Ctx}$ indicate the inclusion functor.

When considering the sub-exponential simply typed $\lambda$-calculus
ST$\lambda$C! as base language, we let $\mathsf{Ctx}_{0}^{!}$ indicate the
category of ST$\lambda$C!-typed terms and
$H:\mathsf{Ctx}_{0}^{!}\hookrightarrow\mathsf{Ctx}_{0}\stackrel{{\scriptstyle\iota}}{{\to}}\mathsf{Ctx}$
indicate the associated embedding inside $\mathsf{Ctx}$ (where
$\mathsf{Ctx}_{0}^{!}\hookrightarrow\mathsf{Ctx}_{0}$ corresponds to the
“forgetful” embedding of ST$\lambda$C! inside ST$\lambda$C - for more details,
see the Appendix).

Observe that the category $\mathsf{Ctx}_{0}$ is cartesian closed, while
$\mathsf{Ctx}_{0}^{!}$ is symmetric monoidal closed and $\mathsf{Ctx}$ is only
cartesian. Hence, the basic data to interpret $\mathrm{dTT}$ will be given by
a strict monoidal functor $U:\mathbb{C}_{0}\to\mathbb{C}$ between a symmetric
monoidal closed category $\mathbb{C}_{0}$ (interpreting either ST$\lambda$C or
ST$\lambda$C!) and a cartesian category $\mathbb{C}$ (interpreting the
difference terms). We will use $\Gamma.\Delta$ for the monoidal product of
$\mathbb{C}_{0}$.

While $\mathbb{C}_{0}$ only accounts for simple types, $\mathbb{C}$ needs to
have enough structure to account for type dependency: for all object $\Gamma$
of $\mathbb{C}_{0}$, we consider a collection $\mathscr{P}(\Gamma)$ of
_predicates over $\Gamma$_ such that, for all $P\in\mathscr{P}(\Gamma)$, there
exists an object $\Gamma\mid P$ of $\mathbb{C}$ and an arrow
$\pi_{\Gamma}:\Gamma\mid P\to U\Gamma$ called the _projection_ of $P$. We also
require that for any predicate $P\in\mathscr{P}(\Gamma)$ and
$f:\Delta\to\Gamma$, the pullback $(Uf)^{\sharp}(\Gamma\mid P)$ exists and is
generated by some object $f^{\sharp}P\in\mathscr{P}(\Delta)$:

${{\Delta\mid f^{\sharp}P}}$${{\Gamma\mid
P}}$${{U\Delta}}$${{U\Gamma}}$$\scriptstyle{\pi_{\Delta}}$$\scriptstyle{f^{+}}$$\scriptstyle{\pi_{\Gamma}}$$\scriptstyle{Uf}$

Moreover, we require that the equalities $\mathrm{id}^{\sharp}P=P$, $(g\circ
f)^{\sharp}p=g^{\sharp}(f^{\sharp}P)$, $\mathrm{id}^{+}=\mathrm{id}$, $(g\circ
f)^{+}=g^{+}\circ f^{+}$ all hold. In the case of $\mathsf{Ctx}$,
$\mathscr{P}(\Phi_{0})$ is the set of predicates
$(\mathbf{x}\in\Phi_{0})\mathcal{C}(\mathbf{x})\in\mathrm{dType}$. Given a
predicate $(x,y\in A)\mathcal{C}(x,y)$ and simply typed terms
$(t,u):(\mathbf{y}\in\Psi_{0})\to(x,y\in A)$, the pullback
$(t,u)^{\sharp}\mathcal{C}$ corresponds to the predicate
$(\mathbf{y}\in\Psi_{0})\mathcal{C}(t(\mathbf{y}),u(\mathbf{y}))$.

Given predicates $P\in\mathscr{P}(\Gamma)$ and $Q\in\mathscr{P}(\Delta)$, we
indicate an arrow $h\in\mathbb{C}(\Gamma\mid P,\Delta\mid Q)$ as $(h_{0}\mid
h_{1})$ if $h=h_{0}^{+}\circ h_{1}$, for some
$h_{0}\in\mathbb{C}_{0}(U\Gamma,U\Delta)$ and $h_{1}\in\mathbb{C}(\Gamma\mid
P,\Gamma\mid h_{0}^{\sharp}Q)$ occurring in a commuting diagram as below.

${\Gamma\mid P}$${\Gamma\mid h_{0}^{\sharp}Q}$${\Delta\mid
Q}$${U\Gamma}$${U\Gamma}$${U\Delta}$$\scriptstyle{h_{1}}$$\scriptstyle{\pi_{\Gamma}}$$\scriptstyle{\pi_{\Gamma}}$$\scriptstyle{h_{0}^{+}}$$\scriptstyle{\pi_{\Delta}}$$\scriptstyle{Uh_{0}}$

In $\mathsf{Ctx}$ this precisely says that an arrow
$(\mathbf{t}\mid\mathbf{a}):(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\to(\mathbf{y}\in\Psi_{0}\mid\boldsymbol{\delta}\in\Psi_{1}(\mathbf{y}))$
is composed of arrows $\mathbf{t}\in\Phi_{0}\to\Psi_{1}$ and
$\mathbf{a}\in\Phi_{1}(\mathbf{x})\to\Psi_{1}(\mathbf{t}(\mathbf{x}))$.

To handle the difference types we need to make some further requirements.
First, we consider a sub-family
$\mathscr{P}^{\flat}(\Gamma)\subseteq\mathscr{P}(\Gamma.\Gamma)$ of binary
predicates, that we call _pure_ predicates, which _generates_ the family
$\mathscr{P}(\\_)$, in the sense that for all object $\Gamma$ and predicate
$P\in\mathscr{P}(\Gamma)$ there exists an object $\Delta$, a pure predicate
$P^{\flat}\in\mathscr{P}^{\flat}(\Delta)\subseteq\mathscr{P}(\Delta.\Delta)$
and $f\in\mathbb{C}_{0}(\Gamma,\Delta.\Delta)$ such that
$P=f^{\sharp}(P^{\flat})$. In the case of $\mathsf{Ctx}$ this is precisely
what is asserted by Lemma 2.1.

For any $\Gamma$, we require a choice of a pure predicate
$\Gamma^{\mathsf{D}}\in\mathscr{P}^{\flat}(\Gamma)$. The introduction rule
requires the existence of an arrow
$r_{\Gamma}:U\Gamma\to(\Gamma.\Gamma\mid\Gamma^{\mathsf{D}})$ such that
$\pi_{\Gamma.\Gamma}\circ r_{\Gamma}$ coincides with the diagonal
$\delta_{U\Gamma}:U\Gamma\to U(\Gamma.\Gamma)=U\Gamma\times U\Gamma$. In
$\mathsf{Ctx}$ $(\Phi_{0})^{\mathsf{D}}$ is
$(\mathbf{x},\mathbf{y}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in
D_{\Phi_{0}}(\mathbf{x},\mathbf{y}))$, where
$D_{\Phi_{0}}(\mathbf{x},\mathbf{y})$ is the list of all
$D_{A_{i}}(x_{i},y_{i})$, for $A_{i}$ occurring in $\Phi_{0}$, and
$r_{\Phi_{0}}$ is given by $(\mathbf{x},\mathbf{x}\mid\partial(\mathbf{x}))$
(where
$\partial(\mathbf{x})=\langle\partial(x_{1}),\dots,\partial(x_{k})\rangle$).
Actually, in order to handle contexts properly, we must consider a slightly
more complex condition (see the Appendix). To handle the elimination rule, for
any binary predicate $P=f^{\sharp}P^{\flat}\in\mathscr{P}(\Gamma.\Gamma)$ and
commutative diagram

${U\Gamma}$${\Gamma.\Gamma\mid
P}$${\Gamma.\Gamma\mid\Gamma^{\mathsf{D}}}$${U\Gamma\times
U\Gamma}$$\scriptstyle{r_{\Gamma}}$$\scriptstyle{c}$$\scriptstyle{\pi_{\Gamma.\Gamma}}$$\scriptstyle{\pi_{\Gamma.\Gamma}}$

we require the existence of a diagonal filler
$j:(\Gamma.\Gamma\mid\Gamma^{\mathsf{D}})\to(\Gamma.\Gamma\mid P)$ making both
triangles commute. In $\mathsf{Ctx}$, $P=f^{\sharp}P^{\flat}$ is a predicate
$(\mathbf{x},\mathbf{y}\in\Phi_{0})\mathcal{C}(\mathbf{x},\mathbf{y})=\mathcal{C}^{\flat}(f_{1}(\mathbf{x},\mathbf{y}),f_{2}(\mathbf{x},\mathbf{y}))$,
$c$ is of the form $(\mathbf{x},\mathbf{x}\mid c^{\prime}(\mathbf{x}))$, where
$c^{\prime}(\mathbf{x})\in\mathcal{C}(\mathbf{x},\mathbf{x})$, and a diagonal
filler is provided by
$j=(\mathbf{x},\mathbf{y}\mid\mathsf{J}(\mathbf{x},\mathbf{y},\boldsymbol{\epsilon},[\mathbf{x}]c^{\prime}))$.
The commutation of the upper triangle $j\circ r_{\Gamma}=c$ coincides then
with the $\beta$-rule. The validity of the $\eta$-rule corresponds to the fact
that, when $P=\Gamma^{\mathsf{D}}$, $f=\pi_{1},g=\pi_{2}$ and $c=r_{\Gamma}$,
$j$ coincides with the identity arrow
$\mathrm{id}_{\Gamma.\Gamma\mid\Gamma^{\mathsf{D}}}$. We will not require the
$\eta$-condition in general. Again, to handle contexts and substitutions
properly, we must consider a slightly more complex construction, together with
a few coherence conditions for $r_{\Gamma}$ and $j$ (see [4, 35]), but we
discuss these more technical aspects in the Appendix.

Finally, we must require that $\mathbb{C}$ has enough structure to interpret
the dependent products present in the fragment $\mathrm{dTT}$; we describe
this structure in the Appendix.

We let a _$\mathrm{dTT}$ -category_ be a strict monoidal functor
$U:\mathbb{C}_{0}\to\mathbb{C}$ together with collections of predicates
$\mathscr{P}(\\_),\mathscr{P}^{\flat}(\\_)$ and of difference structures
$(\\_^{\mathsf{D}},r_{\\_},j_{\\_,\\_,\\_})$ satisfying the properties above.
The following proposition assures that one can interpret $\mathrm{dTT}$ in any
$\mathrm{dTT}$-category.

######  Proposition 3.1.

For any $\mathrm{dTT}$-category $U:\mathbb{C}_{0}\to\mathbb{C}$, if
$\mathbb{C}_{0}$ is cartesian closed, any map $m$ from base type variables to
$\mathrm{Ob}(\mathbb{C}_{0})$ extends into functors
$\llbracket\\_\rrbracket_{m}:\mathsf{Ctx}_{0}\to\mathbb{C}_{0}$ and
$\llparenthesis\\_\rrparenthesis_{m}:\mathsf{Ctx}\to\mathbb{C}$, satisfying
$U\circ\llbracket\\_\rrbracket_{m}=\llparenthesis\\_\rrparenthesis_{m}\circ\iota$,
and preserving all relevant structure. If $\mathbb{C}_{0}$ is symmetric
monoidal closed, the same holds with $\mathsf{Ctx}_{0}$ replaced by
$\mathsf{Ctx}_{0}^{!}$ and $\iota$ replaced by $H$.

To conclude our general presentation of the semantics of $\mathrm{dTT}$, we
show how it relates to WFS. We recall that, given a category $\mathbb{C}$ and
two arrows $f\in\mathbb{C}(A,B)$ and $g\in\mathbb{C}(C,D)$, $f$ is said to
have the _left-lifting property_ with respect to $g$ (and $g$ is said to have
the _right lifting property_ with respect to $f$), if for every commutative
diagram

${A}$${C}$${B}$${D}$$\scriptstyle{f}$$\scriptstyle{h}$$\scriptstyle{g}$$\scriptstyle{k}$

there exists a diagonal filler $j\in\mathbb{C}(B,C)$ making both triangles
commute. Given a set $\mathscr{S}$ of arrows in a category, we let
$\mathscr{S}^{\pitchfork}$ (resp ${}^{\pitchfork}\mathscr{S}$) indicate the
set of arrows $g$ such that any arrow in $\mathscr{S}$ has the left (resp.
right) lifting property with respect to $g$. The following notion generalizes
usual WFS:

######  Definition 3.1.

Let $U:\mathbb{C}\to\mathbb{D}$ be a functor. An _$U$ -weak factorization
system_ (in short, $U$-WFS) _for $\mathbb{C}$ inside $\mathbb{D}$_ is a pair
of classes of maps $(\mathcal{L},\mathcal{R})$ of $\mathbb{D}$ such that (1)
for every morphism $f$ of $\mathbb{C}$, $Uf=p_{f}\circ i_{f}$, with
$i_{f}\in\mathcal{L}$ and $p_{f}\in\mathcal{R}$, and (2)
$\mathcal{L}^{\pitchfork}=\mathcal{R}$ and
$\mathcal{L}=^{\pitchfork}\mathcal{R}$.

Observe that a weak factorization system in the usual sense is just a
$\mathrm{Id}$-WFS.

When a functor $U:\mathbb{C}_{0}\to\mathbb{C}$ yields a
$\mathrm{dTT}$-category, it is possible to construct a $U$-WFS
$(\mathcal{L}_{\mathscr{P}},\mathcal{R}_{\mathscr{P}})$ for $\mathbb{C}_{0}$
inside $\mathbb{C}$ by letting
$\mathcal{L}_{\mathscr{P}}=^{\pitchfork}\mathscr{P}^{*}$ and
$\mathcal{R}_{\mathscr{P}}=\mathcal{L}^{\pitchfork}$, where $\mathscr{P}^{*}$
is made of all arrows obtained by composing the arrows
$\pi_{\Gamma}:\Gamma\mid P\to U\Gamma\times U\Gamma$, for all
$P\in\mathscr{P}^{\flat}(\Gamma)$ with projections in $\mathbb{C}$. The
$U$-factorization of an arrow $f:\Gamma\to\Delta$ in $\mathbb{C}_{0}$ is given
by $p_{f}\circ i_{f}$, where
$p_{f}=\pi_{2}\circ\pi_{\Gamma.\Delta}:\Gamma.\Delta\mid\Delta_{f}\to\Delta$,
$\Delta_{f}$ is a suitable pullback, and $i_{f}$ is the arrow obtained by the
universality of pullback in the diagram below:

${U\Gamma}$${U\Delta}$${\Gamma.\Delta\mid\Delta_{f}}$${\Delta.\Delta\mid\Delta^{\mathsf{D}}}$${U\Gamma\times
U\Delta}$${U\Delta\times U\Delta}$$\scriptstyle{\langle
U\Gamma,Uf\rangle}$$\scriptstyle{r_{f}}$$\scriptstyle{Uf}$$\scriptstyle{r_{\Delta}}$$\scriptstyle{\pi_{\Gamma.\Delta}}$$\scriptstyle{\pi_{\Delta.\Delta}}$$\scriptstyle{Uf.U\Delta}$

where $\Delta_{f}=(f.\Delta)^{\sharp}(\Delta^{\mathsf{D}})$. To show that
$r_{f}\in\mathcal{L}_{\mathscr{P}}$ we must rely on the difference structure
in an essential way: the required diagonal filler is obtained by an arrow of
the form $j$. We describe this construction (which follows the argument from
[16]) in the Appendix.

######  Theorem 3.2.

For any $\mathrm{dTT}$-category $U:\mathbb{C}_{0}\to\mathbb{C}$, with
collections of predicates $\mathscr{P}(\\_),\mathscr{P}^{\flat}(\\_)$, the
pair $(\mathcal{L}_{\mathscr{P}},\mathcal{R}_{\mathscr{P}})$ forms a $U$-WFS
of $\mathbb{C}_{0}$ inside $\mathbb{C}$.

##  4 Metric Preservation

We start our parade of models of $\mathrm{dTT}$ by considering metric models
focusing on program _sensitivity_. In several situations it is important to
know that a program is not too sensitive to small changes in the input. A key
example is differential privacy: if $f:\mathrm{db}\to\mathrm{Real}$ is a
program producing some aggregated information from some database $\mathrm{db}$
(e.g. $f$ outputs the percentage of LGBTIQ+ people among the students of a
given university), we wish the result of $f$ not to depend too much on any
single item of $\mathrm{db}$, so that information about single individuals
cannot be leaked from the outputs of $f$.

A standard way to capture sensitivity is through the _Lipschitz_ -condition: a
function $f$ between metric spaces $(X,a)$ and $(Y,b)$ is $r$-Lipschitz, for
some positive real $r$, when it satisfies $b(f(x),f(y))\leq r\cdot a(x,y)$ for
all $x,y\in X$. It is well-known that from a $r$-Lipschitz function
$f:\mathrm{db}\to\mathrm{Real}$ one can obtain, by adding _Laplace-distributed
noise_ , a randomized function $f^{*}:\mathrm{db}\to\mathrm{Real}$ which is
$r\epsilon$-differentially private.444Formally, this means that for all two
inputs $x,x^{\prime}\in\mathrm{db}$ that differ by at most one parameter and
for all $S\subseteq\mathbb{R}$, the probability $P[f^{*}(x)\in S]$ that
$f^{*}(x)\in S$ is bounded by $e^{r\epsilon}\cdot P[f^{*}(x^{\prime})\in S]$.

The type system $\mathrm{Fuzz}$ [30] was designed to ensure that well-typed
programs correspond to Lipschitz functions. Formally, it is a variant of
_bounded linear logic_ [18], i.e. an affine simply typed $\lambda$-calculus
with a bounded exponential $!_{r}A$, where a program $f\in\ !_{r}A\multimap B$
corresponds to a $r$-Lipschitz function. We consider here a basic fragment
ST$\lambda$C! of $\mathrm{Fuzz}$ (described in the Appendix).

$\mathrm{Fuzz}$ admits a natural and simple semantics in the symmetric
monoidal closed category $\mathrm{Met}$ of metric spaces and _non-expansive_
(i.e. 1-Lipschitz) maps (with monoidal product $(X.a)\otimes(Y.b)=(X\times
Y,a+b)$). In particular, the bounded exponential $!_{r}A$ is interpreted as
the _re-scaling_ $rX$ of a metric space $(X,a)$ (i.e. with $ra(x,y)=r\cdot
a(x,y)$), so that a non-expansive map from $rX$ to $Y$ is the same as a
$r$-Lipschitz function from $X$ to $Y$.

We construct a model of a variant of $\mathrm{dTT}$ where we take program
terms to be ST$\lambda$C!-typable terms. The resulting semantics will
associate each simple type $A$ with some metric space, and will interpret
$D_{A}(t,u)$ as the set of positive reals greater than the distance between
$t$ and $u$. Any difference term $a$ is interpreted by a function yielding
positive real numbers in output; in particular the self-differences
$\partial(t)$ correspond to $0$, and for any non-expansive function $f$,
$\mathsf{D}[f]$ will correspond to the map $x,y,\epsilon\mapsto\epsilon$,
ensuring metric preservation.

We provide a sketch of the $\mathrm{dTT}$-category structure of the forgetful
functor $U:\mathrm{Met}\to\mathrm{Set}$, described in more details in the
Appendix. For any metric space $(X,a)$, the pure predicates
$\mathscr{P}^{\flat}(X)$ are all (pseudo-)metric spaces $P=(X,b)$ over $X$,
with $(X\times X\mid P)=\coprod_{x,y\in X}\widetilde{b}(x,y)$, where
$\widetilde{b}(x,y)=\\{r\mid b(x,y)\leq r\\}$, with projection
$\pi_{X}:(X\otimes X\mid P)\to X\times X$ given by $\pi_{X}(\langle\langle
x,y\rangle,s\rangle)=\langle x,y\rangle$.555Actually, to handle the higher-
order structure, we must consider _parameterized_ (pseudo-)metric spaces over
$X$, see the Appendix. Moreover, for any metric space $(Y,b)$,
$\mathscr{P}(Y)$ is made of pullbacks $\langle f,g\rangle^{\sharp}P$, where
$P=(X,a)\in\mathscr{P}^{\flat}(X)$ and $\langle
f,g\rangle\in\mathrm{Met}(Y,X\otimes X)$, where $(Y\mid\langle
f,g\rangle^{\sharp}P)=\coprod_{y\in Y}a(f(y),g(y))$, with projection
$\pi_{Y}:(Y\mid\langle f,g\rangle^{\sharp}P)\to Y$ given by $\pi_{Y}(\langle
y,s\rangle)=y$.

For any metric space $(X,a)$, the pure predicate
$X^{\mathsf{D}}\in\mathscr{P}^{\flat}(X)$ is $(X,a)$ itself, with
$r_{X}:X\to(X\otimes X\mid X^{\mathsf{D}})$ given by $r_{X}(x)=\langle\langle
x,x\rangle,0\rangle$. For any binary predicate $P=\langle
f,g\rangle^{\sharp}P^{\flat}\in\mathscr{P}(X\otimes X)$ (with $(X\otimes X\mid
P)=\coprod_{x,y\in X}\widetilde{b}(f(x,y),g(x,y))$, for some metric space
$(Y,b)$ and $\langle f,g\rangle\in\mathrm{Met}(X\otimes X,Y\otimes Y)$), and
for any function $c:X\to(X\otimes X\mid P)$ with $c(x)=\langle\langle
x,x\rangle,c^{\prime}(x)\rangle$, we can define a diagonal filler $j:(X\otimes
X\mid X^{\mathsf{D}})\to(X\otimes X\mid P)$ by

$j(\langle\langle x,y\rangle,r\rangle)=\langle\langle
x,y\rangle,c^{\prime}(x)+r\rangle$

In fact, from from $\langle f,g\rangle\in\mathrm{Met}(X\otimes X,Y\otimes Y)$
we deduce
$b(f(x,y),f(x^{\prime},y^{\prime}))+b(g(x,y),g(x^{\prime},y^{\prime}))\leq
a(x,x^{\prime})+b(y,y^{\prime})$. Hence, from
$c^{\prime}(x)\in\widetilde{b}(f(x,x),g(x,x))$ and
$b(f(x,y),f(x,x))+b(g(x,x),g(x,y))\leq a(x,x)+a(x,y)\leq r$, we deduce
$(j(\langle\langle x,y\rangle,r\rangle))_{2}\in\widetilde{b}(f(x,y),g(x,y))$
by the triangular law. The validity of the $\beta$-rule follows from $((j\circ
r_{X})(x))_{2}=c^{\prime}(x)$; moreover, when $f(x,y)=x$, $g(x,y)=y$ and
$c^{\prime}(x)=0$, $j(\langle\langle
x,y\rangle,\epsilon\rangle)=\langle\langle x,y\rangle,\epsilon\rangle$, so the
$\eta$-rule is also valid.

######  Remark 4.1.

When $h\in\mathrm{Met}(rX,Y)$ interprets some $r$-Lipschitz program $t\in\
!_{r}A\multimap B$, the predicate $D_{B}(tx,ty)$ corresponds to the pullback
$\langle
h\circ\pi_{1},h\circ\pi_{2}\rangle^{\sharp}(X,a)\in\mathscr{P}(rX\otimes rX)$,
and the derivative $\mathsf{D}[t]$ is interpreted then by the map
$x,y,\epsilon\mapsto\epsilon$, as desired.

######  Remark 4.2.

From Theorem 3.2 it follows that given metric spaces $(X,a)$ and $(Y,b)$, any
$f\in\mathrm{Met}(rX,Y)$ factors as $X\stackrel{{\scriptstyle
i_{f}}}{{\to}}\coprod_{x\in X,y\in
Y}\widetilde{b}(f(x),y)\stackrel{{\scriptstyle p_{f}}}{{\to}}Y$, where
$i_{f}(x)=\langle\langle x,f(x)\rangle,0\rangle$.

######  Example 4.1.

$\mathrm{dTT}$ can be used to formalize meta-theoretical reasoning about
$\mathrm{Fuzz}$ as discussed in [30, 5]. For instance, we might extend simple
types with the _probability monad_ $\Box A$, adding suitable primitives. Then,
by interpreting the type $D_{\Box A}(t,u)$ with the metric
$d(\delta_{1},\delta_{2})=\frac{1}{\epsilon}\cdot\left(\sup_{x\in
A}\left|\ln\left(\frac{\delta_{1}(x)}{\delta_{2}(x)}\right)\right|\right)$
(with $\delta_{1},\delta_{2}$ distributions over $A$), for any randomized
program $f\in\ !_{r}A\to\Box B$, the statement $\mathsf{D}[f]\in(\Pi x,y\in
A)(D_{A}(x,y)\to D_{\Box B}(f(x),f(y)))$ expresses that for all $x,y\in A$,
$\epsilon\geq d(x,y)$ and $b\in B$, $\left|P[f(x)=b]-P[f(y)=b]\right|\leq
e^{r\epsilon}$, that is, that $f$ is a $r\epsilon$-differentially private
function.

######  Example 4.2.

Suppose $\mathtt{H}(f)$ computes the average of the simulations
$f(0),\dots,f(N)$, i.e.
${\mathtt{H}}(f)=\frac{1}{N+1}\cdot\sum_{i=0}^{N}f(i)$; note that
$\widetilde{\mathtt{H}}(\vec{x})=\frac{1}{N+1}\cdot\sum_{i=0}^{N}x_{i}:\mathrm{Real}^{N+1}\to\mathrm{Real}$
is $\frac{1}{N+1}$-Lipschitz, and thus
$\mathsf{D}[\widetilde{\mathtt{H}}]([x,y]_{i=0,\dots,N})=\frac{1}{N+1}\cdot\sum_{i}y_{i}$.
We deduce then that for all $r$-Lipschitz function $f\in\
!_{r}\mathrm{Nat}\multimap\mathrm{Real}$, the perforation error $b\in
D_{\mathrm{Real}}(\mathtt{H}(f),\mathtt{H}(f^{*}))$ computed in Example 2.1
corresponds to $\frac{1}{N+1}\cdot\sum_{i=0}^{\lfloor
N/2\rfloor}r\cdot\mathsf{D}[f](2i,1)=\frac{\lfloor N/2\rfloor+1}{N+1}\cdot r$.

##  5 Differential Logical Relations

When studying approximate program transformations like loop perforation, the
Lipschitz condition is often too restrictive. In fact, even basic operations
of the simply typed $\lambda$-calculus can make this property fail: while the
binary function $f(k,x)=k\cdot x:\mathrm{Real}^{2}\to\mathrm{Real}$ is
$|k|$-Lipschitz in $x$ for all $k\in\mathbb{R}$, the unary function
$g(x)=x^{2}$ obtained by “contracting” the variables $k$ and $x$ already fails
to be Lipschitz. In fact, the distance between $g(x)$ and $g(x+\epsilon)$ is
bounded by $2|x|\epsilon+\epsilon^{2}$, hence not proportional to $\epsilon$.
Indeed, this kind of issues is due to the fact that $\mathrm{Met}$ is _not_ a
cartesian closed category, that is, a model of full ST$\lambda$C, but only of
its sub-exponential variant $\mathrm{Fuzz}$.

The theory of _differential logical relations_ [13, 23, 28] (in short, DLR),
has been developed to overcome this kind of problems when investigating
approximate transformations in ST$\lambda$C. A DLR is a ternary relation
$\rho\subseteq X\times L\times X$ relating the elements of some set $X$ with
the values of some complete lattice $L$ of “errors over $X$”; intuitively,
$\rho(x,\epsilon,y)$ is to be read as the fact that the error of replacing $x$
by $y$ is bounded by $\epsilon$. As the name suggests, DLR generalize usual
logical relations, which can be seen as DLR where $L$ is the Boolean lattice
$\\{0<1\\}$. Yet, due to the arbitrary choice of $L$, a distance between two
programs needs not be a Boolean nor a positive real (as in metric semantics);
typically, a distance between two functional programs is itself a function,
tracking distances in input into distances in output.

Since $L$ is a complete lattice, for all $x,y\in X$, one can define a distance
function $\|\\_,\\_\|_{\rho}:X\times X\to L$ where
$\|x,y\|=\inf\widetilde{\rho}(x,y)$, with
$\widetilde{\rho}(x,y)=\\{\epsilon\in L\mid\exists\delta\leq\epsilon\text{
s.t. }\rho(x,\delta,y)\\}$. For instance, if we consider the DLR
$(\mathbb{R},\mathbb{R}_{\geq 0}^{\infty},\rho_{\mathrm{Euc}})$, where
$\rho_{\mathrm{Euc}}(r,v,s)$ holds iff $v\geq|r-s|$, the associated distance
function is the Euclidean metric. However, $\|x,y\|_{\rho}$ needs not be a
metric in general: first of all, the self-distances $\|x,x\|_{\rho}$ (that we
note simply as $\|x\|_{\rho}$) need not be zero (i.e. the bottom element of
$L$); moreover, $\|\\_,\\_\|_{\rho}$ needs not satisfy the usual _triangular
law_ of metric spaces (for a detailed comparison between DLR and - generalized
[33] \- metric spaces, see [28]). Here we will restrict our attention to
_separated_ DLR, i.e. such that $\|i\|_{\rho}\in\widetilde{\rho}(i,j)$ (or
$\|j\|_{\rho}\in\widetilde{\rho}(i,j)$) implies $i=j$.

A map of DLR $(X,L,\rho)$ and $(Y,M,\mu)$ is given by a function $f:X\to Y$
(hence no Lipschitz or other continuity conditions are asked) together with an
auxiliary map $\varphi:X\times X\times L\to Y$ which, intuitively, tracks
errors in input into errors in output; more formally, $\varphi$ must satisfy,
for all $x,y\in X$ and $\epsilon\in L$, that if $\rho(x,\epsilon,y)$ holds,
then both $\mu(f(x),\varphi(x,y,\epsilon),f(y))$ and
$\mu(f(x),\varphi(x,y,\epsilon),f(y))$ also hold. (Separated) DLR and their
maps form a cartesian closed category $\mathsf{DLR}$ (see the Appendix, and
[13, 28] for further details).

The presence of the auxiliary map $\varphi$ is what ensures the “transport” of
errors: if $\rho(t,\epsilon,u)$ holds for some $t,u$ of type $A$ and the
context $\mathtt{C}[\ ]:A\to B$ admits an auxiliary map $\varphi$, then
$\varphi(t,u,\epsilon)$ provides an error bound between $\mathtt{C}[t]$ and
$\mathtt{C}[u]$. For example, to the function $g(x)=x^{2}$ one can associate
the auxiliary map $\varphi_{g}(x,y,\epsilon)=2|x|\epsilon+\epsilon^{2}$.

To model $\mathrm{dTT}$ in terms of DLR we will interpret $D_{A}(t,u)$ as the
set $\widetilde{\rho}(t,u)$ of differences between $t$ and $u$; hence, the
self-differences $\partial(t)$ will correspond to $\|t\|_{\rho}$, and
$\mathsf{D}[f]$ will provide each program $f$ with the auxiliary map
$x,y,\epsilon\mapsto\sup\\{\|f(x),f(z)\|_{\mu}\mid z\in
X\land\rho(x,\epsilon,z)\\}$. Moreover, due to the higher-order structure of
DLR (recalled in the Appendix) the DLR models satisfies the extensionality
axioms ($\mathsf{CExt}$) and ($\mathsf{FExt2}$), as well as the equational
rule $\partial(f)=\mathsf{D}[f]$, for $f$ a higher-order function (see [28],
Lemma IV.1).

We provide a sketch of the $\mathrm{dTT}$-category structure of the forgetful
functor $U:\mathsf{DLR}\to\mathrm{Set}$ (given by $U(X,L,\rho)=X$ and
$U(f,\varphi)=f$), described in detail in the Appendix. For any DLR
$(X,L,\rho)$, a pure predicates $P\in\mathscr{P}^{\flat}(X)$ is just a DLR
$(X,L,\rho)$, with $(X\times X\mid P)=\coprod_{x,y\in X}\widetilde{\rho}(x,y)$
and projection $\pi_{X\times X}:(X\times X\mid P)\to X\times X$. For any set
$Y$, $\mathscr{P}(Y)$ is made of pullbacks $\langle f,g\rangle^{\sharp}Q$,
where $Q=(X,L,\rho)\in\mathscr{P}^{\flat}(X)$ and $f,g:Y\to X$, with
$(Y\mid\langle f,g\rangle^{\sharp}Q)=\coprod_{y\in
Y}\widetilde{\rho}(f(y),g(y))$ and associated projection
$\pi_{Y}:(Y\mid\langle f,g\rangle^{\sharp}Q)\to Y$.

For any separated DLR $(X,L,\rho)$, $X^{\mathsf{D}}\in\mathscr{P}^{\flat}(X)$
is $(X,L,\rho)$ itself, with $r_{X}(x)=\langle\langle
x,x\rangle,\|x\|_{\rho}\rangle$; moreover, for any binary predicate $P=\langle
f,g\rangle^{\sharp}P^{\flat}\in\mathscr{P}(X\times X)$ (with $(X\times X\mid
P)=\coprod_{x,y\in X}\widetilde{\mu}(f(x,y),g(x,y))$) and function
$c(x)=\langle\langle x,x\rangle,c^{\prime}(x)\rangle:X\to(X\times X\mid P)$,
so that $c^{\prime}(x)\in\widetilde{\mu}(f(x,x),g(x,x))$, we can define a
diagonal filler $j:(X\times X\mid X^{\mathsf{D}})\to(X\times X\mid P)$ by

$(j(\langle\langle
x,y\rangle,\epsilon\rangle))_{2}=\sup\\{c^{\prime}(x),\inf\widetilde{\mu}(f(x,z),g(x,z))\mid
z\in X\land\rho(x,\epsilon,z)\\}\in\widetilde{\mu}(f(x,y),g(x,y))$

The $\beta$-rule $j(\langle\langle
x,x\rangle,\langle\|x\|_{\rho}\rangle)=c(x)$ follows from the fact that $\rho$
is separated. The $\eta$-rule holds only if $\rho$ is _complete_ , i.e. for
all $x\in X$ and $\epsilon\in L$,
$\sup\\{\inf\widetilde{\rho}(x,y)\mid\rho(x,\epsilon,y)\\}=\epsilon$.

######  Remark 5.1.

When $h:X\to Y$ interprets a program $t\in A\to B$, the predicate
$D_{B}(fx,fy)$ corresponds to the pullback of $D_{B}(x,y)$ along $f(x,y)=h(x)$
and $g(x,y)=h(y)$; moreover, since $\lambda x.\partial(fx)$ is the function
$c^{\prime}(x)=\|h(x)\|_{\mu}$, $\mathsf{D}[t]$ yields then the map
$x,y,\epsilon\mapsto\sup\\{\|h(x),h(z)\|_{\mu}\mid z\in
X\land\rho(x,\epsilon,z)\\}$, as desired.

######  Remark 5.2.

From Theorem 3.2 it follows that given DLR $(X,L,\rho)$ and $(Y,M,\mu)$, any
function $f:X\to Y$ factors as $X\stackrel{{\scriptstyle
i_{f}}}{{\to}}\coprod_{x\in X,y\in
Y}\widetilde{\mu}(f(x),y)\stackrel{{\scriptstyle\pi_{2}\circ\pi_{1}}}{{\to}}Y$
where $i_{f}(x)=\langle\langle x,f(x)\rangle,\|f(x)\|_{\mu}\rangle$.

######  Example 5.1.

Suppose ${\widetilde{\mathtt{H}}}(\vec{x})=(\sum_{i}x_{i})^{2}$, so that its
derivative $\mathsf{D}[{\widetilde{\mathtt{H}}}]$ is interpreted by the
function $\varphi(\vec{x},\vec{\epsilon})=2(\sum
x)(\sum\epsilon)+(\sum_{\epsilon})^{2}$ (where $\sum
y=|\sum_{i=0}^{N}y_{i}|$). Then for any function
$f\in\mathrm{Nat}\to\mathrm{Real}$ with auxiliary map $\psi(n,\theta)$, the
perforation error $b\in D_{\mathrm{Real}}(\mathtt{H}(f),\mathtt{H}(f^{*}))$
from Example 2.1 corresponds to $\varphi([f(i),\psi(i,1)]_{i=0,\dots,N})$.

######  Example 5.2.

By interpreting $\mathrm{Bool}$ as the set $2=\\{0,1\\}$ and
$D_{\mathrm{Bool}}$ as the DLR $(2,2,\rho_{2})$ corresponding to the discrete
metric, the distance function $d_{A}\in(\Pi x,y\in A)D_{A}(x,y)$ from Example
2.2 yields for any DLR $(X,L,\rho)$ the function
$x,y\mapsto\|x,y\|_{\rho}:X\times X\to L$.

##  6 Change Structures and Incremental Computation

In many situations in programming it happens that, after running a program $f$
on some input $i$, one needs to re-run $f$ over some slightly changed input
$i^{\prime}$; incremental computation is about finding ways to optimize this
second computation without having to re-run $f$ from scratch on the novel
input. For example (we take this example from [11]) suppose $f$ computes the
sum of a finite bag of natural numbers $x$. Suppose $f$ has been run on
$x=\\{1,2,3,4\\}$, and now needs to be re-run on $x^{\prime}=\\{2,3,4,5\\}$;
then we can compute $f(x^{\prime})$ incrementally as follows: first, let the
_change_ between $x$ and $x^{\prime}$ be the pair of bags
$\mathsf{d}x=(\\{-1\\},\\{+5\\})$ describing what has to be changed to turn
$x$ into $x$’. Then the change $\mathsf{d}y$ between $f(x)$ and
$f(x^{\prime})$ is the value $\mathsf{d}y=-1+5=+4$, and $f(x^{\prime})$ can be
computed simply by adding $\mathsf{d}y$ to $f(x)$. In particular, the
operation $\mathsf{d}f(x,\mathsf{d}x)$ taking a bag and a change and returning
the change $\mathsf{d}y$ is called (once more!) a _derivative_ of $f$ (we call
it a _change derivative_ for clarity), as it describes the change to get from
$f(x)$ to $f(y)$ as a function of $x$ and the change $\mathsf{d}x$.

In [11] these ideas have been turned into a _change semantics_ for the simply
typed $\lambda$-calculus, which was later generalized and simplified through
the theory of _change actions_ [1, 3]. These approaches have been applied to
model different forms of discrete and automated differentiation [1, 21], and
more recently related to models of the differential $\lambda$-calculus [23].
We focus here on change structures from [11] since they have a natural higher-
order structure.

A _change structure_ (in short, CS) is a tuple $(X,\Delta_{X},\oplus,\ominus)$
where $X$ is a set, for all $x\in X$, $\Delta_{X}x$ is a set of _changes over
$x$_, and $\oplus:X\times\Delta_{X}\to X$ and $\ominus:X\times X\to\Delta_{X}$
are operations satisfying (1) $x\ominus y\in\Delta_{X}y$ and (2)
$x\oplus(y\ominus x)=y$.

Any function $f:X\to Y$ admits a change derivative $\mathsf{d}f:X\times\Delta
X\to\Delta Y$ defined by
$\mathsf{d}f(x,\mathsf{d}x)=f(x\oplus\mathsf{d}x)\ominus f(x)$ and satisfying
$f(x\oplus\mathsf{d}x)=f(x)\oplus\mathsf{d}f(x,\mathsf{d}x)$. In other words,
$\mathsf{d}f(x,\mathsf{d}x)$ describes the change needed to pass from $f(x)$
to $f(x\oplus\mathsf{d}x)$.

For all $x\in X$ we let $\mathbf{0}_{x}=x\ominus x\in D_{X}x$; notice that
$x\oplus\mathbf{0}_{x}=x$ and
$\mathsf{d}f(x,\mathbf{0}_{x})=\mathbf{0}_{f(x)}$. Moreover, whenever
$x\oplus\mathsf{d}x=y$, we let $\ominus\mathsf{d}x:=x\ominus y$. Finally,
given $\mathsf{d}x\in\Delta_{X}x$ and
$\mathsf{d}y\in\Delta_{X}(x\oplus\mathsf{d}x)$, we let
$\mathsf{d}x+\mathsf{d}y:=((x\oplus\mathsf{d}x)\oplus\mathsf{d}y)\ominus x$.

The CS semantics of $\mathrm{dTT}$ will interpret $D_{A}(\\_,\\_)$ as the type
of changes over $A$, and a judgement $a\in D_{A}(t,u)$ as expressing the fact
that $a$ is a change from $t$ to $u$ (i.e. that $t\oplus a=u$). Self-
differences $\partial(t)$ will correspond to the null change $\mathbf{0}_{t}$,
and $\mathsf{D}[f]$ will correspond to the change derivative $\mathsf{d}f$.
Moreover, due to the higher-order structure of change structures (recalled in
the Appendix), this model satisfies the extensionality axiom
($\mathsf{CExt}$).

We provide a sketch of the $\mathrm{dTT}$-category structure of the forgetful
functor $U:\mathsf{CS}\to\mathrm{Set}$, leaving as usual most details to the
Appendix. For any CS $X$, a pure predicate $P\in\mathscr{P}^{\flat}(X)$ is a
CS $P=(X,\Delta_{X},\oplus,\ominus)$, with $(X\times X\mid P)=\coprod_{x,y\in
X}\Delta_{X}(x,y)$ (where $\Delta_{X}(x,y)=\\{\mathsf{d}x\in\Delta_{X}x\mid
x\oplus\mathsf{d}x=y\\}$), and projection $\pi_{X}:(X\times X\mid P)\to
X\times X$. For any CS $Y$, $\mathscr{P}(Y)$ is made of pullbacks $\langle
f,g\rangle^{\sharp}P$, where $P\in\mathscr{P}^{\flat}(X)$ is a CS
$P=(X,\Delta_{X},\oplus,\ominus)$, and $(Y\mid\langle
f,g\rangle^{\sharp}P)=\coprod_{y\in Y}\Delta_{X}(f(y),g(y))$, with associated
projection $\pi_{Y}:(Y\mid\langle f,g\rangle^{\sharp}P)\to Y$.

For any CS $X$, $X^{\mathsf{D}}\in\mathscr{P}^{\flat}(X)$ is $X$ itself, with
$r_{X}(x)=\langle\langle x,x\rangle,\mathbf{0}_{x}\rangle$; moreover, for any
binary predicate $P=\langle f,g\rangle^{\sharp}P^{\flat}\in\mathscr{P}(X\times
X)$ (with $(X\times X\mid P)=\coprod_{x,y\in X}\Delta_{Y}(f(x,y),g(x,y))$) and
function $c:X\to(X\times X\mid P)$, where $c(x)=\langle\langle
x,x\rangle,c^{\prime}(x)\rangle$, with
$c^{\prime}(x)\in\Delta_{Y}(f(x,x),g(x,x))$, a diagonal filler $j:(X\times
X\mid X^{\mathsf{D}})\to(X\times X\mid P)$ is defined by

$\big{(}j(\langle\langle
x,x^{\prime}\rangle,\mathsf{d}x\rangle)\big{)}_{2}=\mathsf{d}f(\langle
x,x\rangle,\langle\mathbf{0}_{x},\ominus\mathsf{d}x\rangle)+c^{\prime}(x)+\mathsf{d}g(\langle
x,x\rangle,\langle\mathbf{0}_{x},\mathsf{d}x\rangle)\in\Delta_{Y}(f(x,y),g(x,y))$

One can check that $(j(\langle\langle
x,x\rangle,\mathbf{0}_{x}\rangle))_{3}=c(x)$; the validity of the $\eta$-rule
requires the further assumption that for all $x,y$, $y\ominus x$ is the
_unique_ change from $x$ to $y$.

######  Remark 6.1.

When $h:X\to Y$ interprets some program $f\in A\to B$, the interpretation of
$\mathsf{D}[t]$ corresponds to constructing a diagonal filler as above with
$f(x,y)=h(x)$, $g(x,y)=h(y)$ and $c^{\prime}(x)=\mathbf{0}_{h(x)}$; then one
obtains the map $x,y,\mathsf{d}x\mapsto\mathsf{d}h(x,\mathsf{d}x)$ as desired.

######  Remark 6.2.

From Theorem 3.2 it follows that given change structures on $X,Y$, any
function $f:X\to Y$ factors as $X\stackrel{{\scriptstyle
i_{f}}}{{\to}}\coprod_{x\in X,y\in
Y}\Delta_{Y}(f(x),y)\stackrel{{\scriptstyle\pi_{2}\circ\pi_{1}}}{{\to}}Y$
where $i_{f}(x)=\langle\langle x,f(x)\rangle,\mathbf{0}_{f(x)}\rangle$.

######  Example 6.1.

Consider the change structure on $\mathrm{Real}$ where
$\Delta_{\mathrm{Real}}x=\mathbb{R}$, $\oplus$ is addition and $\ominus$ is
subtraction. Let $f,g:\mathrm{Nat}\to\mathrm{Real}$ be such that $g$
“increments” on $f$ through some function
$F:\mathrm{Nat}\times\mathrm{Nat}\to\mathrm{Real}$ (i.e. $g(x)=f(x)+F(x,0)$).
In $\mathrm{dTT}$ $F$ yields then an element of
$D_{\mathrm{Nat}\to\mathrm{Real}}(f,g)$. By reasoning as in Example 2.1 we can
construct the increment from $\mathtt{H}(f)$ to $\mathtt{H}(g)$; if
$\mathtt{H}(f)$ is as in Example 4.2, this corresponds then to
$1/N\cdot\sum_{i=0}^{N}F(i,0)$.

##  7 Cartesian Differential Categories

We conclude our sketch of differential models of $\mathrm{dTT}$ with the
axiomatization of program derivatives provided by cartesian differential
categories (CDC). The introduction of the _differential $\lambda$-calculus_
[14], an extension of the $\lambda$-calculus with a _differential_ operator
$\mathsf{d}t$, has motivated much research on abstract axiomatizations of
differentiation that generalize the usual derivatives from calculus to higher-
order programming languages [9, 10, 8]. CDC can be seen as a common ground for
all these approaches, as they provide basic algebraic rules for derivatives in
a cartesian setting.

We recall that a cartesian category $\mathbb{C}$ is _left-additive_ when the
Hom-objects of $\mathbb{C}$ are monoids, with the monoidal operations $0,+$
commuting with the cartesian structure (e.g. $f+(g\times
h)=(f+g)\times(f+h)$), and satisfies left-additivity, i.e. $0\circ f=0$ and
$(g+h)\circ f=(g\circ f)+(h\circ f)$. A CDC is a cartesian left-additive
category endowed with a derivative operator $\mathsf{d}$ such that for all
$f:X\to Y$, $\mathsf{d}f:X\times X\to Y$, satisfying a few axioms (D1)-(D7)
(recalled in the Appendix). Intuitively, $\mathsf{d}f(x,y)$ describes the
differential $f^{\prime}(x)\cdot y$ of $f$ at $x$, so it should be a _linear_
function in $y$. This is reflected by the axiom (D2) stating, informally, that
$\mathsf{d}f$ is additive in its second variable, i.e. $\mathsf{d}f(x,0)=0$
and $\mathsf{d}f(x,y+y^{\prime})=\mathsf{d}f(x,y)+\mathsf{d}f(x,y^{\prime})$.
Among the other axioms for $\mathsf{d}f$ we find analogs of axioms
($\mathsf{D}\mathrm{chain}$) (the chain rule) as well as axioms expressing the
commutation of $\mathsf{d}f$ with the cartesian structure, plus some other
axioms concerning second derivatives. When a CDC is cartesian closed, one
usually adds also axiom ($\mathsf{J}\lambda 1b$) (called $D$-Curry in [10]),
and one speaks of a _differential $\lambda$-category_.

We now describe the interpretation of $\mathrm{dTT}$ in a differential
$\lambda$-category. In fact, everything works in any CDC if we forget about
the higher-order structure.666Since Euclidean spaces $\mathbb{R}^{n}$ and
smooth functions form a CDC [9] this shows in particular that one can
consistently interpret $\mathsf{D}[f]$ as the “true” derivative from analysis.
We will interpret $D_{A}(t,u)$ as a sort of “tangent space” of $t$ (notice
that we ignore $u$); the self-difference $\partial(t)$ will correspond to the
zero vector $0$, and the derivative $\mathsf{D}[f]$, which sends “vectors
tangent to $x$” into “vectors tangent to $fx$”, will correspond to
$\mathsf{d}f$. Moreover, the resulting model satisfies the extensionality
axioms ($\mathsf{CExt}$) and ($\mathsf{FExt1}$) (see the Appendix for
details).

Let $\mathbb{C}$ be a differential $\lambda$-category. We sketch the
$\mathrm{dTT}$-structure on the identity functor
$\mathrm{id}:\mathbb{C}\to\mathbb{C}$, leaving all details to the Appendix.
The classes $\mathscr{P}^{\flat}(X)$ contain all objects of the form $X^{n}$
(where $X^{0}=1$, $X^{n+1}=X^{n}\times X$), with $(X^{2}\mid
X^{n})=X^{2}\times X^{n}$ and projection $\pi_{X}:X^{2}\times X^{n}\to X^{2}$.
$\mathscr{P}(Y)$ is made of pullbacks $\langle f,g\rangle^{\sharp}X^{n}$, for
arrows $f,g:Y\to X$, with $(Y\mid\langle f,g\rangle^{\sharp}X^{n})=Y\times
X^{n}$ and projection $\pi_{Y}:(Y\mid\langle f,g\rangle^{\sharp}X^{n})\to Y$.

For any object $X$, the pure predicate
$X^{\mathsf{D}}\in\mathscr{P}^{\flat}(X)$ is just $X$, and $r_{X}:X\to X^{3}$
is $r_{X}=\langle\langle\mathrm{id_{X}},\mathrm{id}_{X}\rangle,0\rangle$.
Moreover, for any binary predicate $P=\langle
f,g\rangle^{\sharp}Z^{n}\in\mathscr{P}(X^{2})$, where $f,g:X^{2}\to Z$, for
any arrow $c:X\to(X^{2}\mid P)=X^{2}\times Z^{n}$, where
$c=\langle\mathrm{id}_{X},\mathrm{id}_{X},c^{\prime}\rangle$, with
$c^{\prime}:X\to Z^{n}$, we can define a diagonal filler $j:X^{3}\to
X^{2}\times Z^{n}$ by letting

$j=\langle\langle\pi_{1}\circ\pi_{1},\pi_{2}\circ\pi_{1}\rangle,c^{\prime}\circ(\pi_{1}\circ\pi_{1})+\langle\mathsf{d}f\circ\langle\pi_{1}\circ\pi_{1},\pi_{2}\rangle\rangle^{n}\rangle$

Observe that $(j\circ r_{X})_{2}=c$ and moreover, if $Z^{n}=X$,
$f=\mathrm{id}_{X}$ and $c=r_{X}$, then $j=\mathrm{id}_{X\times X}$, so both
the $\beta$\- and $\eta$-rules are satisfied.

######  Remark 7.1.

When $h:X\to Y$ interprets $t\in A\to B$, $\mathsf{D}[h]$ corresponds to a
diagonal filler with $f=h\circ\pi_{1},g=\pi_{2}$ and
$c=\langle\mathrm{id}_{X},0\rangle$, yielding the map $\mathsf{d}h:X\times
X\to Y$.

######  Remark 7.2.

From Theorem 3.2 it follows that the classes
$\mathcal{L}_{\mathscr{P}},\mathcal{R}_{\mathscr{P}}$ form a WFS in
$\mathbb{C}$, where $f:X\to Y$ factors as $X\stackrel{{\scriptstyle
i_{f}}}{{\to}}(X\times Y)\times
Y\stackrel{{\scriptstyle\pi_{2}\circ\pi_{1}}}{{\to}}X$, with
$i_{f}=\langle\langle\mathrm{id}_{X},f\rangle,0\rangle$.

##  8 Conclusions

### Related Work

$\mathrm{dTT}$ is definitely not the first proof system proposed to formalize
relational reasoning for higher-order programs (nor the first one based on
dependent types, e.g. [32]). Among the many existing systems we can mention
the logics for parametricity and logical relations [29, 22], the refinement
type systems for cryptography [6], differential privacy [7] and relational
cost analysis [12], Relational Hoare Type Theory [32] and Relational Higher-
Order Logic [12]. In particular, it is tempting to look at $\mathrm{dTT}$ as a
_proof-relevant_ variant of (some fragment of) RHOL, since the latter is based
on judgements of the form $\Gamma\mid\Psi\vdash t:A\sim u:B\mid\varphi$, where
$\Gamma\vdash t:A,u:B$ are typings in ST$\lambda$C, and $\Psi,\varphi$ are
logical formulas depending on the variables in $\Gamma$ as well as $t$ and
$u$. Indeed, the main difference between $\mathrm{dTT}$ and such systems is
that program differences are represented as proof objects. This looks a rather
natural choice at least for those semantics (like e.g. DLR and CS) where
program differences can be seen as being themselves some kind of programs.

Neither we are the first to observe formal correspondences between various
notions of program derivative. For instance, a formalization of change
structures in the context of DLR is discussed in [23]; connections between
metric semantics and DLR are studied in [17, 28], based on _generalized_
metric spaces and _quantaloid_ -enriched categories [33]. In particular, the
DLR model sketched in Section 5 can be used to provide a “quantaloid-
interpretation” of $D_{A}(\\_,\\_)$ (to be compared with the groupoid
structure of the identity type in full ITT). Recently, _cartesian difference
categories_ [2] have been proposed as a general framework for program
derivatives (unifying cartesian differential categories with approaches
related to both discrete derivatives and incremental computation). It seems
that our model in Section 5 can be extended to such categories in a
straightforward way.

### Future Work

The main goal of this paper was to provide evidence that ITT could serve the
purpose of formalizing differential reasoning. Yet, examples were left
necessarily sketchy and more substantial formalization work (as well as
implementations) needs to be addressed.

As $\mathrm{dTT}$ is a fragment of ITT, syntactic results like strong
normalization follow. Yet, the problem should be addressed whether such
results are stable also when further equations for derivatives (as those
described in Section 2) are added. Moreover, it is well-known that a suitable
formulation of 2-dimensional ITT satisfies a _canonicity_ condition [25]: a
closed normal term of type $\mathrm{Bool}$ is either $\mathbf{0},\mathbf{1}$;
it would be interesting to see whether this result can be scaled to the
fragment $\mathrm{dTT}$.

Finally, it seems worth exploring extensions of $\mathrm{dTT}$ with further
structure, for instance with dependent types at the base level (e.g. following
work on dependent types for differential privacy [15]), as well as with
primitives for probabilistic reasoning (as in [30, 7, 6]).

## References

  * [1] Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, and C.-H. Luke Ong.  Fixing incremental computation.  In Luís Caires, editor, Programming Languages and Systems, pages 525–552, Cham, 2019. Springer International Publishing.
  * [2] Mario Alvarez-Picallo and Jean-Simon Pacaud Lemay.  Cartesian difference categories.  In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures (FoSSaCS 2020), pages 57–76, Cham, 2020. Springer International Publishing.
  * [3] Mario Alvarez-Picallo and C.-H. Luke Ong.  Change actions: Models of generalised differentiation.  In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures (FoSSaCS 2019), pages 45–61, Cham, 2019. Springer International Publishing.
  * [4] Steve Awodey and Michael A. Warren.  Homotopy theoretic models of identity types.  Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45–55, 2009.  doi:10.1017/S0305004108001783.
  * [5] Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui.  A semantic account of metric preservation.  In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, page 545?556, New York, NY, USA, 2017. Association for Computing Machinery.  URL: https://doi.org/10.1145/3009837.3009890, doi:10.1145/3009837.3009890.
  * [6] Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin.  Probabilistic relational verification for cryptographic implementations.  In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pages 193–205, New York, NY, USA, 2014. Association for Computing Machinery.  URL: https://doi.org/10.1145/2535838.2535847, doi:10.1145/2535838.2535847.
  * [7] Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella Béguelin.  Probabilistic relational reasoning for differential privacy.  In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’12. ACM Press, 2012.  URL: http://dx.doi.org/10.1145/2103656.2103670, doi:10.1145/2103656.2103670.
  * [8] Richard F. Blute, Robin Cockett, J.S.P. Lemay, and R.A.G. Seely.  Differential categories revisited.  Applied Categorical Structures, 28:171–235, 2020.
  * [9] Richard F. Blute, Robin Cockett, and R.A.G. Seely.  Cartesian Differential Categories.  Theory and Applications of Categories, 22(23):622–672, 2009.
  * [10] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto.  Categorical models for simply typed resource calculi.  Electronic Notes in Theoretical Computer Science, 265:213 – 230, 2010.  Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010).  URL: http://www.sciencedirect.com/science/article/pii/S1571066110000927, doi:https://doi.org/10.1016/j.entcs.2010.08.013.
  * [11] Y. Cai, P.G. Giarrusso, T. Rendel, and K. Ostermann.  A theory of changes for higher-order languages: incrementalizing $\lambda$-calculi by static differentiation.  ACM SIGPLAN Not., 49:145–155, 2014.
  * [12] Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann.  Relational cost analysis.  In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 316–329, New York, NY, USA, 2017\. Association for Computing Machinery.  URL: https://doi.org/10.1145/3009837.3009858, doi:10.1145/3009837.3009858.
  * [13] Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu.  Differential logical relations, part I: the simply-typed case.  In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, pages 111:1–111:14, 2019.  URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.111, doi:10.4230/LIPIcs.ICALP.2019.111.
  * [14] Thomas Ehrhard and Laurent Regnier.  The differential lambda-calculus.  Theoretical Computer Science, 309(1):1–41, December 2003.  doi:10.1016/S0304-3975(03)00392-X.
  * [15] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce.  Linear dependent types for differential privacy.  In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’13. ACM Press, 2013.  URL: http://dx.doi.org/10.1145/2429069.2429113, doi:10.1145/2429069.2429113.
  * [16] Nicola Gambino and Richard Garner.  The identity type weak factorisation system.  Theoretical Computer Science, 409(1):94–109, 2008.
  * [17] Guillaume Geoffroy and Paolo Pistone.  A partial metric semantics of higher-order types and approximate program transformations.  In Computer Science Logic 2021 (CSL 2021), volume 183 of LIPIcs–Leibniz International Proceedings in Informatics, pages 35:1–35:18, 2021\.
  * [18] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott.  Bounded linear logic: A modular approach to polynomial time computability.  Theoretical Computer Science, 97:1–66, 1992.  Extended abstract in Feasible Mathematics, S. R. Buss and P. J. Scott editors, Proceedings of the MCI Workshop, Ithaca, NY, June 1989, Birkhauser, Boston, pp. 195–209.
  * [19] Mark Hovey.  Model Categories, volume 63 of Mathematical Surveys and Monographs.  American Mathematical Society, 1999.
  * [20] Bart Jacobs.  Categorical logic and type theory, volume 141 of Studies in Logic and Foundations of Mathematics.  Elsevier, 1999.
  * [21] Robert Kelly, Barak A. Pearlmutter, and Jeffrey Mark Sisking.  Evolving the incremental $\lambda$-calculus into a model of forward automatic differentiation (AD).  ArXiv https://arxiv.org/abs/1611.03429, 2016.
  * [22] Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal.  A relational model of types-and-effects in higher-order concurrent separation logic.  SIGPLAN Not., 52(1):218–231, January 2017.  URL: https://doi.org/10.1145/3093333.3009877, doi:10.1145/3093333.3009877.
  * [23] Ugo Dal Lago and Francesco Gavazzo.  Differential logical relations part II: increments and derivatives.  In Gennaro Cordasco, Luisa Gargano, and Adele A. Rescigno, editors, Proceedings of the 21st Italian Conference on Theoretical Computer Science, Ischia, Italy, September 14-16, 2020, volume 2756 of CEUR Workshop Proceedings, pages 101–114. CEUR-WS.org, 2020.  URL: http://ceur-ws.org/Vol-2756/paper_10.pdf.
  * [24] Joachim Lambek and Philip J. Scott.  Introduction to higher order categorical logic.  Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1988.
  * [25] Daniel R. Licata and Robert Harper.  Canonicity for 2-dimensional type theory.  In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pages 337–348, New York, NY, USA, 2012. Association for Computing Machinery.  URL: https://doi.org/10.1145/2103656.2103697, doi:10.1145/2103656.2103697.
  * [26] Per Martin-Löf.  An intuitionistic theory of types: predicative part.  In Proceedings of the Logic Colloquium 1973, Bristol, volume 80 of Studies in logic and the foundations of mathematics, pages 73–118. North-Holland, 1975.
  * [27] Damiano Mazza and Michele Pagani.  Automatic differentiation in pcf.  Proceedings of the ACM on Programming Languages, 5(POPL:28), 2021\.
  * [28] Paolo Pistone.  On generalized metric spaces for the simply typed lambda-calculus.  In to appear in Proceedings of LICS 2021, 2021.
  * [29] Gordon Plotkin and Martin Abadi.  A logic for parametric polymorphism.  In TLCA ’93, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361–375. Springer Berlin Heidelberg, 1993.
  * [30] Jason Reed and Benjamin C. Pierce.  Distance makes the types grow stronger.  Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP ’10, 2010.  URL: http://dx.doi.org/10.1145/1863543.1863568, doi:10.1145/1863543.1863568.
  * [31] Stelios Sidiroglou-Douskos, Sasa Misailovic, Henry Hoffmann, and Martin Rinard.  Managing performance vs. accuracy trade-offs with loop perforation.  In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering, ESEC/FSE ’11, pages 124–134, New York, NY, USA, 2011.
  * [32] Gordon Stewart, Anindya Banerjee, and Aleksandar Nanevski.  Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures.  In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP ’13, pages 145–156, New York, NY, USA, 2013\. Association for Computing Machinery.  URL: https://doi.org/10.1145/2505879.2505895, doi:10.1145/2505879.2505895.
  * [33] Isar Stubbe.  An introduction to quantaloid-enriched categories.  Fuzzy Sets and Systems, 256:95 – 116, 2014.  Special Issue on Enriched Category Theory and Related Topics (Selected papers from the 33rd Linz Seminar on Fuzzy Set Theory, 2012).  doi:https://doi.org/10.1016/j.fss.2013.08.009.
  * [34] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [35] Benno van den Berg and Richard Garner.  Topological and simplicial models of identity types.  ACM Trans. Comput. Logic, 13(1), January 2012.  URL: https://doi.org/10.1145/2071368.2071371, doi:10.1145/2071368.2071371.
  * [36] Edwin Westbrook and Swarat Chaudhuri.  A semantics for approximate program transformations.  https://arxiv.org/abs/1304.5531, 2013.

##  Appendix A Type Systems: Details

The typing rules of $\mathrm{dTT}$ can be divided into the rules for typing
program terms and the rules for typing difference terms.

### Simple Types

In its basic formulation, the rules for typing program terms are the standard
typing rules of ST$\lambda$C, recalled in Fig. 3. In Section 4 we considered a
variant of $\mathrm{dTT}$ with affine simple types and an exponential
$!_{r}A$, for all $r\in\mathbb{R}_{\geq 0}$, corresponding to a fragment of
$\mathrm{Fuzz}$ [30]. We describe the rules of this fragment, that we call
ST$\lambda$C!, in Fig. 4. The terms are generated by the grammar:

$t,u:=x\mid\lambda x.t\mid tu\mid!t\mid\mathbf{let}\ !x=t\ \mathbf{in}\
u\mid(t,u)\mid\mathbf{let}\ (x,y)=t\ \mathbf{in}\ u$

For the purposes of this article we limited ourselves to a minimal fragment of
this language. For a more practical language see [30, 5]. Simple types are
generated by the grammar below:

$A,B:=X\mid!_{r}A\quad(r\in\mathbb{R}_{\geq 0})\mid A\multimap B\mid A\otimes
B$

Type judgements are of the form $\Phi\vdash t:A$, where a context $\Phi$ is a
list of declarations of the form $x\in_{r}A$, for some $r\in\mathbb{R}_{\geq
0}$. We define the following operation $\Phi+\Psi$ as follows:

$\displaystyle()+()$ $\displaystyle=()$
$\displaystyle(\Phi,x\in_{r}A)+(\Psi,x\in_{s}A)$
$\displaystyle=(\Phi+\Psi),x\in_{r+s}A$ $\displaystyle(\Phi,x\in_{r}A)+\Psi$
$\displaystyle=(\Phi+\Psi),x\in_{r}A\qquad(x\notin\Psi)$
$\displaystyle\Phi+(\Psi,x\in_{r}A)$
$\displaystyle=(\Phi+\Psi),x\in_{r}A\qquad(x\notin\Phi)$

Moreover, we let $s\Phi$ be the context made all judgmenets $x\in_{sr}A$,
where $(x\in_{r}A)\in\Phi$.

Observe that one can always type an affine term like e.g. $\lambda xy.x$ with
a linear type $A\multimap B\multimap A$. Instead, a term like $\lambda
xy.x(xy)$ containing two occurrences of $x$ cannot be given the linear type
$(A\multimap A)\multimap(A\multimap A)$ but a type of the form
$!_{2}(A\multimap A)\multimap(A\multimap A)$.

There exists a “forgetful” translation ∗ from ST$\lambda$C! to ST$\lambda$C
given on terms by

$\displaystyle x^{*}=x\qquad(\lambda x.t)^{*}=\lambda
x.t^{*}\qquad(tu)^{*}=t^{*}u^{*}$
$\displaystyle(!t)^{*}=t^{*}\qquad(\mathbf{let}\ !x=t\ \mathbf{in}\
u)^{*}=(\lambda x.t^{*})u^{*}$ $\displaystyle(t,u)^{*}=\langle
t^{*},u^{*}\rangle\qquad(\mathbf{let}\ (x,y)=t\ \mathbf{in}\ u)^{*}=(\lambda
xy.u^{*})\pi_{1}(t^{*})\pi_{2}(t^{*})$

and on types by

$\displaystyle X^{*}=X\qquad(!_{r}A)^{*}=A^{*}\qquad(A\multimap
B)^{*}=A^{*}\to B^{*}\qquad(A\otimes B)^{*}=A^{*}\times B^{*}$

This translation can be used to define the functor $H$ from Section 3 from the
context category $\mathsf{Ctx}^{!}_{0}$ of ST$\lambda$C! to $\mathsf{Ctx}$.

$x\in A\in\Phi$ $\Phi\vdash x\in A$
$\Phi,x\in A\vdash t\in B$ $\Phi\vdash\lambda x.t\in A\to B$ $\Phi\vdash t\in
A\to B$ $\Phi\vdash u\in A$ $\Phi\vdash tu\in B$ $\Phi\vdash t\in A$
$\Phi\vdash u\in B$ $\Phi\vdash\langle t,u\rangle\in A\times B$ $\Phi\vdash
t\in A_{1}\times_{2}$ $\Phi\vdash\pi_{i}(t)\in A_{i}$

Figure 3: Typing rules for ST$\lambda$C.

$x\in_{r}A\in\Phi$ $\Phi\vdash x\in A$
$\Phi,x\in_{1}A\vdash t\in B$ $\Phi\vdash\lambda x.t\in A\multimap B$
$\Phi\vdash t\in A\multimap B$ $\Phi\vdash u\in A$ $\Phi\vdash tu\in B$
$\Phi\vdash t\in A$ $\Psi\vdash u\in B$ $\Phi+\Psi\vdash(t,u)\in A\otimes B$
$\Phi\vdash t\in A\otimes B$ $\Psi,x\in_{r}A,y\in_{r}B\vdash u:C$
$\Phi+\Psi\vdash\mathbf{let}\ (x,y)=t\ \mathbf{in}\ u\in C$ $\Phi\vdash t\in
A$ $s\Phi\vdash!t\in\ !_{s}A$ $\Phi\vdash t\in!_{s}A$ $\Psi,x\in_{rs}A\vdash
u:C$ $r\Phi+\Psi\vdash\mathbf{let}\ !x=t\ \mathbf{in}\ u\in C$

Figure 4: Typing rules for ST$\lambda$C!.

### Difference Types

As discussed in Section 2, the rules for difference terms are the standard
rules of ITT, restricted to the language of $\mathrm{dTT}$. We illustrate in
Fig. 5 the rules for the difference type (where, compared to the rules
sketched in Section 2, we highlight the role of contexts), and all other rules
in Fig. 6. Finally, we illustrate $\beta$\- and $\eta$-rules in Fig. 7.

$\mathbf{x}\in\Phi_{0}\vdash t\in A$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash\partial(t)\in
D_{A}(t,t)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x},t,u))\vdash
a\in D_{A}(t,u)$ $(\mathbf{x}\in\Phi_{0},x,y\in
A\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x},x,y))\vdash\mathcal{C}(\mathbf{x},x,y)\in\mathrm{dType}$
$(\mathbf{x}\in\Phi_{0},x\in
A\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x},x,x))\vdash
b\in\mathcal{C}(\mathbf{x},x,x)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x},t,u))\vdash\mathsf{J}(t,u,a,[x]b)\in\mathcal{C}(\mathbf{x},t,u)$

Figure 5: Typing rules for the difference type.

$(\mathbf{x}\in\Phi_{0},x\in
A\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
a\in\mathcal{A}(\mathbf{x},x)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash\lambda
x.a\in(\Pi x\in A)\mathcal{A}(\mathbf{x},x)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
a\in(\Pi x\in A)\mathcal{A}(\mathbf{x},x)$ $(\mathbf{x}\in\Phi_{0})\vdash t\in
A$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
at\in\mathcal{A}(\mathbf{x},t)$
$(\mathbf{x}\in\Phi_{0},x,y\in
A\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}),\epsilon\in D_{A}(x,y)\vdash
a\in\mathcal{A}(\mathbf{x},x,y)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash\lambda
xy\epsilon.a\in(\Pi x,y\in A)(D_{A}(x,y)\to\mathcal{A}(\mathbf{x},x,y))$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
a\in(\Pi x,y\in A)(D_{A}(x,y)\to\mathcal{A}(\mathbf{x},x,y))$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
b\in D_{A}(t,u)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
atub\in\mathcal{A}(\mathbf{x},t,u)$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
a\in\mathcal{A}$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
b\in\mathcal{A}$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash\langle
a,b\rangle\in\mathcal{A}\times\mathcal{B}$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash
a\in\mathcal{A}_{1}\times\mathcal{A}_{2}$
$(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\vdash\pi_{i}(a)\in\mathcal{A}_{i}$

Figure 6: Typing rules of $\mathrm{dTT}$.

$\displaystyle(\lambda x.a)t$ $\displaystyle\simeq_{\beta}a[t/x]$
$\displaystyle(\lambda x.ax)$
$\displaystyle\simeq_{\eta}a\quad(x\notin\mathrm{FV}(a))$
$\displaystyle(\lambda xy\epsilon.a)tub$
$\displaystyle\simeq_{\beta}a[t/x,u/y,b/\epsilon)$ $\displaystyle(\lambda
xy\epsilon.axy\epsilon)$
$\displaystyle\simeq_{\eta}a\quad(x,y,\epsilon\notin\mathrm{FV}(a))$
$\displaystyle\pi_{i}(\langle a_{1},a_{2}\rangle)$
$\displaystyle\simeq_{\beta}a_{i}$
$\displaystyle\langle\pi_{1}(a),\pi_{2}(a)\rangle$
$\displaystyle\simeq_{\eta}a$ $\displaystyle\mathsf{J}(t,t,\partial(t),[x]b)$
$\displaystyle\simeq_{\beta}b[t/x]$ $\displaystyle\ J(t,u,a,[x]\partial(x))$
$\displaystyle\simeq_{\eta}a$

Figure 7: $\beta$\- and $\eta$-rules for difference terms.

###### Proof.

Proof of Lemma 2.1

  * •

if $\mathcal{C}(\mathbf{z})=D_{C}(t,u)$, then
$(t,u):(\mathbf{z}\in\Phi_{0})\to(y,y^{\prime}\in C)$ we let $\Psi_{0}=C$ and
$\mathcal{C}^{\flat}(y,y^{\prime})=D_{C}(y,y^{\prime})$.

  * •

if
$\mathcal{C}(\mathbf{z})=\mathcal{C}_{1}(\mathbf{z})\times\mathcal{C}_{2}(\mathbf{z})$,
then by induction hypothesis there exist pure predicates $(x,y\in
A_{1})\mathbf{C}_{1}^{\flat},(x,y\in A_{2})\mathbf{C}_{2}^{\flat}$, and terms
$(t_{1},u_{1}):(\mathbf{z}\in\Phi_{0})\to(x,y\in A_{1})$ and
$(t_{2},u_{2}):(\mathbf{z}\in\Phi_{0})\to(x,y\in A_{2})$ such that
$\mathcal{C}_{1}(\mathbf{z})=\mathcal{C}_{1}^{\flat}(t_{1},u_{1})$ and
$\mathcal{C}_{2}(\mathbf{z})=\mathcal{C}_{2}^{\flat}(t_{2},u_{2})$. We can let
then $A=A_{1}\times A_{2}$, $t=\langle t_{1},\mathbf{t}_{2}\rangle$,
$u=\langle u_{1},u_{2}\rangle$ and
$\mathcal{C}^{\flat}(w,w^{\prime})=\mathcal{C}_{1}^{\flat}(\pi_{1}(w),\pi^{\prime}(w^{\prime}))\times\mathcal{C}_{2}^{\flat}(\pi_{2}(w),\pi_{2}(w^{\prime}))$.

  * •

if $\mathcal{C}(\mathbf{z})=(\Pi w\in D)\mathcal{B}(\mathbf{z},w)$ then by
induction hypothesis there exists a pure predicate $(x,y\in
A^{\prime})\mathcal{B}^{\flat}(x,y)$ and terms
$(t^{\prime},u^{\prime}):(\mathbf{z}\in\Phi_{0},w\in D)\to(x,y\in A^{\prime})$
such that
$\mathcal{B}(\mathbf{z},w)=\mathcal{B}^{\flat}(t^{\prime},u^{\prime})$. We let
then $A=D\to A^{\prime}$, $\mathcal{C}^{\flat}(x,y)=(\Pi w\in
A)\mathcal{B}^{\flat}(xw,yw)$ and $t=\lambda w.t^{\prime}$, $u=\lambda
w.u^{\prime}$.

  * •

if $\mathcal{C}(\mathbf{z})=(\Pi w,w^{\prime}\in
C)(D_{C}(w,w^{\prime})\to\mathcal{B}(\mathbf{z},w,w^{\prime})$ then by
induction hypothesis there exists a pure predicate $(x,y\in
A^{\prime})\mathcal{B}^{\flat}(x,y)$ and terms
$t^{\prime},u^{\prime}:(\mathbf{z}\in\Phi_{0},w,w^{\prime}\in A)\to(x,y\in
A^{\prime})$ such that
$\mathcal{B}(\mathbf{z},w,w^{\prime})=\mathcal{B}^{\flat}(t^{\prime},u^{\prime})$.
We let then $A=C\to(C\to A^{\prime})$, $\mathcal{C}^{\flat}(x,y)=(\Pi
w,w^{\prime}\in
C)(D_{A}(w,w^{\prime})\to\mathcal{B}^{\flat}(xww^{\prime},yww^{\prime}))$ and
$t=\lambda ww^{\prime}.t^{\prime}$, $u=\lambda ww^{\prime}.u^{\prime}$.

∎

##  Appendix B Equational Rules for Derivatives: Details

We list a few equational rules for the operators $\mathsf{J}$ and
$\mathsf{D}$, that make sense under the validity of some of the extensionality
axioms.

  * •

in presence of ($\mathsf{CExt}$) one can consider the following rules:

$\displaystyle\partial(\langle t,u\rangle)$
$\displaystyle=\langle\partial(t),\partial(u)\rangle$ ($\mathsf{J}\times a$)
$\displaystyle\mathsf{J}(t,u,a,[x]\langle b,c\rangle)$
$\displaystyle=\langle\mathsf{J}(t,u,a,[x],b),\mathsf{J}(t,u,a,[x],b)\rangle$
($\mathsf{J}\times b$) $\displaystyle\mathsf{J}(t,u,a,[x]\pi_{i}(b))$
$\displaystyle=\pi_{i}\big{(}\mathsf{J}(t,u,a,[x]b)\big{)}$ ($\mathsf{J}\times
c$)

These rules say that the difference structure commutes with the cartesian
structure.

  * •

in presence of ($\mathsf{FExt1}$) one can consider the following rules:

$\displaystyle\partial(\lambda x.t)$ $\displaystyle=\lambda x.\partial(t)$
($\mathsf{J}\lambda 1a$) $\displaystyle\mathsf{J}(t,u,a,[x]\lambda y.b(x,y))$
$\displaystyle=\lambda y.\mathsf{J}(\langle t,y\rangle,\langle
u,y\rangle,\langle a,\partial(y)\rangle,[z]b(\pi_{1}(z),\pi_{2}(z))$
($\mathsf{J}\lambda 1b$)

from which it follows that the derivative “in $x$” $\mathsf{D}[\lambda
xy.f(x,y)]$ of some binary function $f(x,y)$ is the same as the derivative “in
$z=\langle x,y\rangle$”, i.e. $\mathsf{D}[\lambda
z.f(\pi_{1}(z),\pi_{2}(z))]$, where the error on $y$ is its self-difference,
i.e. $\lambda xx^{\prime}\delta y.\mathsf{D}[\lambda
z.f(\pi_{1}(z),\pi_{2}(z))]\langle x,y\rangle\langle
x^{\prime},y\rangle\langle\epsilon,\partial(y)\rangle$ (when $\partial(y)$ is
interpreted as the null error $0$, this coincides with axiom $D$-curry from
[10]);

  * •

in presence of ($\mathsf{FExt2}$) and ($\mathsf{CExt}$) one can consider the
following rules:

$\displaystyle\partial(\lambda x.t)$ $\displaystyle=\mathsf{D}[\lambda x.t]$
($\mathsf{J}\lambda 2a$) $\displaystyle\mathsf{J}(t,u,a,[x]\lambda y.b)$
$\displaystyle=\lambda yy^{\prime}\delta.\mathsf{J}\Big{(}\langle
t,y\rangle,\langle u,y^{\prime}\rangle,\langle
a,\delta\rangle,[z]\big{(}b[\pi_{1}(z)/x,\pi_{2}(z)/y]\big{)}\Big{)}$
($\mathsf{J}\lambda 2b$)

This shows that the axioms ($\mathsf{FExt1}$) and ($\mathsf{FExt2}$) might
give rise to derivative with a rather different operational semantics. In
particular, Eq. ($\mathsf{J}\lambda 2a$) says that the self-difference of a
function coincides with its derivative (this will be the case in the models
from Sec. 5 and 6); moreover, ($\mathsf{J}\lambda 2b$) says that the
derivative “in $x$” of a binary function $f(x,y)$ actually derives also in the
variable $y$. In particular one can deduce that $\mathsf{D}[\lambda
xy.t(x,y)]xx^{\prime}\epsilon yy^{\prime}\delta$ is the same as
$\mathsf{D}[\lambda z.t(\pi_{1}(z),\pi_{2}(z))]\langle x,y\rangle\langle
x^{\prime}y^{\prime}\rangle\langle\epsilon,\delta\rangle$.

##  Appendix C $\mathrm{dTT}$-Categories: Details

In this section we define in detail the notion of $\mathrm{dTT}$-category that
was sketched in Section 3. Throughout this section we suppose
$U:\mathbb{C}_{0}\to\mathbb{C}$ to be a strict monoidal functor, where
$\mathbb{C}_{0}$ is a symmetric monoidal category and $\mathbb{C}$ is a
cartesian category. Moreover, we suppose that for any object $\Gamma$ of
$\mathbb{C}_{0}$ the following data is given:

  * •

a collection $\mathscr{P}(\Gamma)$ of predicates over $\Gamma$, and for each
$P\in\mathscr{P}(\Gamma)$ an object $\Gamma\mid P$ and an arrow
$\pi_{\Gamma}:\Gamma\mid P\to U\Gamma$; we further require that:

    * –

for all $P\in\mathscr{P}(\Gamma)$ and $f:U\Delta\to U\Gamma$, the pullback
$f^{\sharp}P$ exists and is in $\mathscr{P}(\Delta)$;

    * –

when the monoidal product of $\mathbb{C}_{0}$ is not cartesian, we furthermore
require that:

      * *

for all $P\in\mathscr{P}(\Gamma)$, the pullback $\pi_{U\Gamma}^{\sharp}P$
exists and is in $\mathscr{P}(\Delta.\Gamma)$, where
$\pi_{U\Gamma}:U\Delta\times U\Gamma\to U\Gamma$;

      * *

for all $P\in\mathscr{P}(\Gamma.\Gamma)$, the pullback
$\delta_{U\Gamma}^{\sharp}P$ exists and is in $\mathscr{P}(\Gamma)$, where
$\delta_{U\Gamma}:U\Gamma\to U\Gamma\times U\Gamma$;

    * –

we require all mentioned pullbacks to be associative and unital;

    * –

for all $P,Q\in\mathscr{P}(\Gamma)$, a predicate $P\times
Q\in\mathscr{P}(\Gamma)$ exists such that $\Gamma\mid P\times Q$ is the
cartesian product of $\Gamma\mid P$ and $\Gamma\mid Q$ in the _slice category_
$\mathbb{C}_{\mathscr{P}}^{\Gamma}$, i.e. in the category of predicates in
$\mathscr{P}(\Gamma)$ and _vertical_ arrows (see Section 3), i.e. those arrows
$h:\Gamma\mid P\to\Gamma\mid Q$ making the diagram below commute

${\Gamma\mid P}$${\Gamma\mid
Q}$${U\Gamma}$${U\Gamma}$$\scriptstyle{\pi_{\Gamma}}$$\scriptstyle{h}$$\scriptstyle{\pi_{\Gamma}}$

  * •

a sub-collection
$\mathscr{P}^{\flat}(\Gamma)\subseteq\mathscr{P}(\Gamma.\Gamma)$ of _pure
predicates_ generating $\mathscr{P}$, (i.e. such that any
$P\in\mathscr{P}(\Gamma)$ is of the form $f^{\sharp}P^{\flat}$, where
$P^{\flat}\in\mathscr{P}^{\flat}(\Delta)$ and
$f\in\mathbb{C}_{0}(\Delta,\Gamma.\Gamma)$), together with a chosen pure
predicate $\Gamma^{\mathsf{D}}\in\mathscr{P}^{\flat}(\Gamma)$, and closed with
respect to the following conditions:

    * –

for all pure predicates $P,Q\in\mathscr{P}^{\flat}(\Gamma)$, $P\times
Q\in\mathscr{P}^{\flat}(\Gamma)$;

    * –

for all objects $\Delta,\Gamma$ of $\mathbb{C}_{0}$ and pure predicate
$P\in\mathscr{P}^{\flat}(\Gamma)$, a pure predicate
$\Pi_{\Delta}P\in\mathscr{P}^{\flat}(\Gamma^{\Delta}.\Gamma^{\Delta})$ such
that for all $Q\in\mathscr{P}(\Sigma)$ there is a bijection

$\mathbb{C}\big{(}\Delta.\Sigma\mid\pi_{\Sigma}^{\sharp}Q\ ,\Gamma.\Gamma\mid
P\big{)}\simeq\mathbb{C}\big{(}\Sigma\mid Q\ ,\
\Gamma^{\Delta}.\Gamma^{\Delta}\mid\Pi_{\Delta}P\big{)}$

where $\pi_{\Sigma}$ is the projection $\Delta.\Sigma\to\Sigma$. Moreover, we
require that dependent products commute with pullbacks, i.e. for all
$f\in\mathbb{C}_{0}(\Gamma^{\prime},\Gamma)$,
$f^{\sharp}(\Pi_{\Delta}P)=\Pi_{\Delta}(f^{\sharp}P)$.

    * –

for all objects $\Delta,\Gamma$ of $\mathbb{C}_{0}$ and pure predicate
$P\in\mathscr{P}^{\flat}(\Gamma.\Gamma)$ a pure predicate
$P^{\left(\Delta^{\mathsf{D}}\right)}\in\mathscr{P}^{\flat}(\Gamma^{\Delta.\Delta})$
such that for all $Q\in\mathscr{P}(\Sigma)$ there is a bijection

$\mathbb{C}\big{(}\Delta.\Delta.\Sigma\mid\pi_{\Sigma}^{\sharp}Q\times\Delta^{\mathsf{D}}\
,\ \Gamma.\Gamma\mid P\big{)}\simeq\mathbb{C}\big{(}\Sigma\mid Q\ ,\
\Gamma^{\Delta.\Delta}.\Gamma^{\Delta.\Delta}\mid
P^{\left(\Delta^{\mathsf{D}}\right)}\big{)}$

where $\pi_{\Sigma}$ is the projection $\Delta.\Delta.\Sigma\to\Sigma$.
Moreover, we require that for all
$f\in\mathbb{C}_{0}(\Gamma^{\prime},\Gamma)$,
$f^{\sharp}\left(P^{\left(\Delta^{\mathsf{D}}\right)}\right)=(f^{\sharp}P)^{\left(\Delta^{\mathsf{D}}\right)}$.

We will make extensive use of the following constructions: for all objects
$\Gamma,\Delta$ of $\mathbb{C}_{0}$ there exists

  * •

a functor
$\pi_{\Delta.\Gamma}^{\sharp}:\mathbb{C}_{\mathscr{P}}^{\Delta.\Gamma}\to\mathbb{C}_{\mathscr{P}}^{\Delta.\Gamma.\Gamma}$
induced by the projection
$\pi_{\Delta.\Gamma}:\Delta.\Gamma.\Gamma\to\Delta.\Gamma$ which deletes the
third component of $\Delta.\Gamma.\Gamma$, together with an arrow
$\pi_{\Delta.\Gamma}^{+}:\Delta.\Gamma.\Gamma\mid\pi_{\Delta.\Gamma}^{\sharp}(P)\to\Delta.\Gamma\mid
P$ making the pullback diagram below commute:

${\Delta.\Gamma.\Gamma\mid\pi_{\Delta.\Gamma}^{\sharp}(P)}$${\Delta.\Gamma\mid
P}$${U\Delta.U\Gamma.U\Gamma}$${U\Delta.U\Gamma}$$\scriptstyle{\pi_{\Delta.\Gamma.\Gamma}}$$\scriptstyle{\pi_{\Delta.\Gamma}^{+}}$$\scriptstyle{\pi_{\Delta.\Gamma}}$$\scriptstyle{\pi_{\Delta.\Gamma}}$

  * •

a functor $\delta_{\Delta.\Gamma\mid
Q}^{\sharp}:\mathbb{C}_{\mathscr{P}}^{\Delta.\Gamma.\Gamma}\to\mathbb{C}_{\mathscr{P}}^{\Delta.\Gamma}$
induced by the arrow
$\delta_{\Delta.\Gamma}:\Delta.\Gamma\to\Delta.\Gamma.\Gamma$ which duplicates
the second component of $\Delta.\Gamma$, together with an arrow
$\delta_{\Delta.\Gamma\mid Q}^{+}:\Delta.\Gamma\mid\delta_{\Delta.\Gamma\mid
Q}^{\sharp}(P)\to\Delta.\Gamma\mid Q\times P$ making the pullback diagram
below commute:

${\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(P)}$${\Delta.\Gamma.\Gamma\mid
P}$${U\Delta.U\Gamma}$${U\Delta.U\Gamma.U\Gamma}$$\scriptstyle{\pi_{\Delta.\Gamma}}$$\scriptstyle{\delta_{\Delta.\Gamma}^{+}}$$\scriptstyle{\pi_{\Delta.\Gamma.\Gamma}}$$\scriptstyle{\delta_{\Delta,\Gamma}}$

Moreover, one has
$\delta_{\Delta.\Gamma}^{\sharp}\circ\pi_{\Delta.\Gamma}^{\sharp}=\mathrm{id}_{\mathbb{C}_{\mathscr{P}}^{\Delta.\Gamma}}$.

In $\mathsf{Ctx}$ the operation $\pi_{\Delta.\Gamma}^{\sharp}$ turns a
predicate $\mathcal{C}(z,x)$ into a predicate
$\mathcal{C}^{{\dagger}}(z,x,y)=\mathcal{C}(z,x)$ by adding a “dummy” variable
$y$; the operation $\delta_{\Delta.\Gamma}^{\sharp}$ turns a predicate
$\mathcal{C}(z,x,y)$ into a predicate
$\mathcal{C}^{{\ddagger}}(z,x)=P(z,x,x)$. Notice that
$(\mathcal{C}^{{\dagger}})^{{\ddagger}}=\mathcal{C}$.

The difference structure is provided by the following data:

  * •

for all objects $\Gamma,\Delta$ of $\mathbb{C}_{0}$ and for all predicate
$Q\in\mathscr{P}(\Delta.\Gamma.\Gamma)$, an arrow $r_{\Delta,\Gamma\mid
Q}:\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)\to\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}$, such that the composition of
$r_{\Delta,\Gamma\mid Q}$ with the projection
$\pi_{1}:\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}\to\Delta.\Gamma.\Gamma\mid Q$ coincides with
$\delta_{\Delta,\Gamma}^{+}:\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)\to\Delta.\Gamma.\Gamma\mid
Q$

  * •

for all objects $\Delta,\Gamma$ of $\mathbb{C}_{0}$, predicates
$Q\in\mathscr{P}(\Delta.\Gamma.\Gamma)$ and
$P=f^{\sharp}P^{\flat}\in\mathscr{P}(\Delta.\Gamma.\Gamma)$, and for any arrow
$c:\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)\to\Delta.\Gamma.\Gamma\mid
Q\times P$ making the diagram below commute

${\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)}$${\Delta.\Gamma.\Gamma\mid
Q\times P}$${\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}}$${\Delta.\Gamma.\Gamma\mid
Q}$$\scriptstyle{r_{\Delta,\Gamma\mid
Q}}$$\scriptstyle{c}$$\scriptstyle{\pi_{1}}$$\scriptstyle{\pi_{1}}$

(notice that this implies that $c$ is of the form
$\langle\delta_{\Delta,\Gamma}^{+}(Q),c^{\prime}\rangle$) a choice of a
diagonal filler $j_{\Delta,\Gamma,Q,f,P,c}$ making both triangles commute.

We require the data above to satisfy a few coherence conditions, namely that
for all $g\in\mathbb{C}_{0}(\Sigma,\Delta)$ and vertical morphism
$h\in\mathbb{C}_{\mathscr{P}}^{\Delta.\Gamma.\Gamma}(R,Q)$,
$\Gamma^{\mathsf{D}}=(g.\Gamma.\Gamma)^{\sharp}\Gamma^{\mathsf{D}}$, and the
pullback diagrams below commute:

${\Sigma.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(g^{\sharp}Q)}$${\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)}$${\Sigma.\Gamma.\Gamma\mid
g^{\sharp}Q\times\Gamma^{\mathsf{D}}}$${\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}}$$\scriptstyle{r_{\Sigma,\Gamma\mid
Q}}$$\scriptstyle{\delta_{\Delta.\Gamma}^{\sharp}(g^{+})}$$\scriptstyle{r_{\Delta,\Gamma\mid
Q}}$$\scriptstyle{(Ug.\Gamma.\Gamma)^{+}}$
${\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(R)}$${\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)}$${\Delta.\Gamma.\Gamma\mid
R\times\Gamma^{\mathsf{D}}}$${\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}}$$\scriptstyle{r_{\Delta,\Gamma\mid
R}}$$\scriptstyle{\delta_{\Delta.\Gamma}^{\sharp}(h)}$$\scriptstyle{r_{\Delta,\Gamma\mid
Q}}$$\scriptstyle{h\times\Gamma^{\mathsf{D}}}$ ${\Sigma.\Gamma.\Gamma\mid
g^{\sharp}Q\times\Gamma^{\mathsf{D}}}$${\Sigma.\Gamma.\Gamma\mid
g^{\sharp}Q\times g^{\sharp}P}$${\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}}$${\Delta.\Gamma.\Gamma\mid Q\times
P}$$\scriptstyle{j_{\Sigma,\Gamma,g^{\sharp}Q,gf,P,c^{*}}}$$\scriptstyle{g.\Gamma.\Gamma^{+}}$$\scriptstyle{g.\Gamma.\Gamma^{+}}$$\scriptstyle{j_{\Delta,\Gamma,Q,f,P,c}}$
${\Delta.\Gamma.\Gamma\mid
R\times\Gamma^{\mathsf{D}}}$${\Delta.\Gamma.\Gamma\mid R\times
P}$${\Delta.\Gamma.\Gamma\mid
Q\times\Gamma^{\mathsf{D}}}$${\Delta.\Gamma.\Gamma\mid Q\times
P}$$\scriptstyle{j_{\Delta,\Gamma,R,f,\langle\delta_{\Delta,\Gamma}^{+},c^{\prime}\circ
h\rangle}}$$\scriptstyle{h\times\Gamma^{\mathsf{D}}}$$\scriptstyle{h\times
P}$$\scriptstyle{j_{\Delta,\Gamma,Q,f,P,c}}$

where the arrow
$c^{*}:\Sigma.\Gamma\mid\delta_{\Sigma.\Gamma}^{\sharp}(g^{\sharp}Q)\to\Sigma.\Gamma.\Gamma\mid
g^{\sharp}Q\times g^{\sharp}P$ is given by the universality of the pullback
along $g$:

${\Sigma.\Gamma\mid\delta_{\Sigma.\Gamma}^{\sharp}(g^{\sharp}Q)}$${\Delta.\Gamma\mid\delta_{\Delta.\Gamma}^{\sharp}(Q)}$${\Sigma.\Gamma.\Gamma\mid
g^{\sharp}Q\times g^{\sharp}P}$${\Delta.\Gamma.\Gamma\mid Q\times
P}$${\Sigma.\Gamma.\Gamma\mid
g^{\sharp}Q}$${\Sigma.\Gamma.\Gamma}$${\Delta.\Gamma.\Gamma}$$\scriptstyle{(g.\Gamma.\Gamma)^{+}}$$\scriptstyle{\delta_{\Sigma.\Gamma}^{+}}$$\scriptstyle{c^{*}}$$\scriptstyle{c}$$\scriptstyle{\pi_{\Sigma.\Gamma.\Gamma}}$$\scriptstyle{(g.\Gamma.\Gamma)^{+}}$$\scriptstyle{\pi_{\Delta.\Gamma.\Gamma}}$$\scriptstyle{\pi_{\Sigma.\Gamma.\Gamma}}$$\scriptstyle{g.\Gamma.\Gamma}$

These (admittedly complicated) conditions essentially say that
$\Gamma^{\mathsf{D}}$, $r_{\Delta,\Gamma}$ and $j_{\Delta,\Gamma,Q,f,P,c}$ “do
not depend on” $\Delta$ and $Q$, i.e. are invariant under substitutions of the
variables in $\Delta$ and $Q$. In other words, they assure the soundness of
the equations below for the substitution operation:

$\displaystyle\partial(t)[v/y]$ $\displaystyle=\partial(t[v/y])$
$\displaystyle\partial(t)[c/\epsilon]$ $\displaystyle=\partial(t)$
$\displaystyle\mathsf{J}(t,u,a,[x]b)[v/y]$
$\displaystyle=\mathsf{J}(t[v/y],u[v/y],a[v/y],[x]b[v/y])$
$\displaystyle\mathsf{J}(t,u,a,[x]b)[c/\epsilon]$
$\displaystyle=\mathsf{J}(t,u,a[c/\epsilon],[x]b[c/\epsilon])$

###### Proof of Proposition 3.1.

The definition of the functor
$\llbracket\\_\rrbracket_{m}:\mathsf{Ctx}_{0}\to\mathbb{C}_{0}$ is standard.
The functor $\llparenthesis\\_\rrparenthesis_{m}:\mathsf{Ctx}\to\mathbb{C}$ is
defined as follows:

  * •

to any pure predicate $(x,y\in A)\mathcal{C}(x,y)$ we associate
$\llparenthesis\mathcal{C}\rrparenthesis_{m}\in\mathscr{P}^{\flat}(\llbracket
A\rrbracket_{m})$ by induction as follows:

    * –

if $\mathcal{C}(x,y)=D_{A}(x,y)$, then $\llparenthesis
A\rrparenthesis_{m}=(\llbracket A\rrbracket_{m})^{\mathsf{D}}$;

    * –

if
$\mathcal{C}(x,y)=\mathcal{C}_{1}(\pi_{1}(x),\pi_{1}(y))\times\mathcal{C}_{2}(\pi_{2}(x),\pi_{2}(y))$,
then
$\llparenthesis\mathcal{C}\rrparenthesis_{m}=\pi_{1}^{\sharp}\llparenthesis\mathcal{C}_{1}\rrparenthesis_{m}\times\pi_{2}^{\sharp}\llparenthesis\mathcal{C}_{2}\rrparenthesis_{m}$;

    * –

if $\mathcal{C}(x,y)=(\Pi z\in B)\mathcal{C}^{\prime}(xz,yz)$, then
$\llparenthesis\mathcal{C}\rrparenthesis_{m}=\Pi_{\llbracket
B\rrbracket_{m}}\llparenthesis\mathcal{C}^{\prime}\rrparenthesis_{m}$;

    * –

if $\mathcal{C}(x,y)=(\Pi w,w^{\prime}\in
B)(D_{B}(w,w^{\prime})\to\mathcal{C}^{\prime}(xww^{\prime},yww^{\prime}))$,
then
$\llparenthesis\mathcal{C}\rrparenthesis_{m}=\llparenthesis\mathcal{C}^{\prime}\rrparenthesis_{m}^{\left(\llbracket
B\rrbracket_{m}^{\mathsf{D}}\right)}$.

  * •

For any arrow $(\mathbf{t}\mid
a):(\mathbf{x}\in\Phi_{0}\mid\boldsymbol{\epsilon}\in\Phi_{1}(\mathbf{x}))\to(\mathbf{y}\in\Psi_{0}\mid\delta\in\mathcal{C}(\mathbf{y}))$
we define an arrow $(\llbracket t\rrbracket_{m}\mid\llparenthesis
a\rrparenthesis_{m}):(\llbracket\Phi_{0}\rrbracket_{m}\mid\llparenthesis\Phi_{1}\rrparenthesis_{m})\to(\llbracket\Psi_{0}\rrbracket_{m}\mid(\llbracket
t\rrbracket_{m})^{\sharp}\llparenthesis\mathcal{C}\rrparenthesis_{m})$ in
$\mathbb{C}$, where $\llparenthesis a\rrparenthesis_{m}$ is a vertical
morphism in $\mathbb{C}_{\mathscr{P}}^{\llbracket\Phi_{0}\rrbracket_{m}}$, by
induction on $a$. We here only mention the cases related to the difference
type:

    * –

if $a=\partial(t)$, where $(\mathbf{x}t\in A$, $\llparenthesis
a\rrparenthesis_{m}=r_{\llbracket\Phi^{\prime}_{0}\rrbracket_{m},\llbracket
A\rrbracket_{m}\mid\llparenthesis\Phi_{1}\rrparenthesis_{m}}\circ\llbracket
t\rrbracket_{m}$, where
$\mathbf{x}\in\Phi_{0}=\mathbf{x}^{\prime}\in\Phi^{\prime}_{0},x\in A$;

    * –

if $a=\mathsf{J}(t,u,b,[x]c)$, where $a\in D_{A}(t,u)$,
$(\mathbf{x},\mathbf{y}\in\Phi_{0})\mathcal{C}(\mathbf{x},\mathbf{y})=\mathcal{C}^{\flat}(\mathbf{t}(\mathbf{x},\mathbf{y}))$
and $(x\in A)c\in\mathcal{C}(x,x)$, then $\llparenthesis
a\rrparenthesis=j_{\llbracket\Phi_{0}\rrbracket_{m},\llbracket
A\rrbracket_{m},\llbracket\Phi_{1}\rrbracket_{m},\llbracket\mathbf{t}\rrbracket_{m},\llparenthesis\mathcal{C}^{\flat}\rrparenthesis_{m},\llparenthesis
c\rrparenthesis_{m}}$.

∎

###### Proof of Theorem 3.2.

We must show that $i_{f}\in\mathcal{L}_{\mathscr{P}}$, so let
$P\in\mathscr{P}(\Sigma)$ be a predicate. The problem of finding a diagonal
filler for a commutative diagram of the form

${\Gamma}$${\Sigma\mid
P}$${\Gamma.\Delta\mid\Delta_{f}}$${\Sigma}$$\scriptstyle{i_{f}}$$\scriptstyle{d}$$\scriptstyle{\pi_{\Sigma}}$$\scriptstyle{h}$

can be reduced, by pulling back along $h$, to that of finding a diagonal
filler $j$ for a diagram of the form

${\Gamma}$${\Gamma.\Delta\mid
Q}$${\Gamma.\Delta\mid\Delta_{f}}$${\Gamma.\Delta}$$\scriptstyle{i_{f}}$$\scriptstyle{c}$$\scriptstyle{\pi_{\Gamma.\Delta}}$$\scriptstyle{\pi_{\Gamma.\Delta}}$

(with $Q=h^{\sharp}P$). We will obtain $j$ by putting together a few
commutative diagrams:

  1. 1.

${\Gamma}$${\Gamma.\Delta\mid\Delta_{f}.Q}$${\Gamma.\Delta\mid\Delta_{f}}$${\Gamma.\Delta.\Delta\mid\pi_{\Gamma.\Delta}^{\sharp}(\Delta_{f}).\pi_{\Gamma.\Delta}^{\sharp}(Q).\Delta^{\mathsf{D}}}$$\scriptstyle{i_{f}.c}$$\scriptstyle{i_{f}}$$\scriptstyle{r_{\Gamma\mid\Delta_{f}.Q,\Delta}}$$\scriptstyle{\delta_{\Delta}^{+}.(\delta_{\Delta}^{+}\circ
c).r_{\Gamma.\Delta}}$

  2. 2.

${\Gamma}$${\Gamma.\Delta\mid
Q}$${\Gamma.\Delta\mid\Delta_{f}.Q}$${\Gamma.\Delta.\Delta\mid\pi_{\Gamma.\Delta}^{\sharp}(\Delta_{f}).\pi^{\sharp}_{\Gamma.\Delta}(Q).\pi^{\sharp}_{\Gamma.\Delta}(Q)}$$\scriptstyle{i_{f}.c}$$\scriptstyle{c}$$\scriptstyle{\delta_{\Delta}^{+}.(\delta_{Q}\circ\delta_{\Delta}^{+})}$$\scriptstyle{\pi_{\Gamma.\Delta}^{+}\circ\pi_{3}}$

where $\pi_{\Gamma.\Delta}$ is the projection
$\Gamma.\Delta.\Delta\to\Gamma.\Delta$ and we use the fact that
$\delta_{\Delta}^{\sharp}(\pi_{\Gamma.\Delta}^{\sharp}(\Delta_{f}))=\Delta_{f}$
and $\delta_{\Delta}^{\sharp}(\pi_{\Gamma.\Delta}^{\sharp}(Q))=Q$, so that
$\delta_{\Delta}^{+}:\Gamma.\Delta\mid\Delta_{f}\to\Gamma.\Delta.\Delta\mid\pi^{\sharp}_{\Gamma.\Delta}(\Delta_{f})$
and $(\delta_{\Delta})^{+}:\Gamma.\Delta\mid
Q\to\Gamma.\Delta.\Delta\mid\pi_{\Gamma.\Delta}^{\sharp}(Q)$.

  3. 3.

${\Gamma.\Delta.\Delta\mid\pi_{\Gamma.\Delta}^{\sharp}(\Delta_{f}).\pi_{\Gamma.\Delta}^{\sharp}(Q).\pi_{\Gamma.\Delta}^{\sharp}(Q)}$${\Gamma.\Delta\mid\Delta_{f}.Q}$${\Gamma.\Delta.\Delta}$${\Gamma.\Delta}$$\scriptstyle{\pi_{\Gamma.\Delta.\Delta}}$$\scriptstyle{(\pi_{\Gamma.\Delta}^{+}\circ\pi_{2}).(\pi_{\Gamma.\Delta}^{+}\circ\pi_{3})}$$\scriptstyle{\pi_{\Gamma.\Delta}}$$\scriptstyle{\pi_{\Gamma.\Delta}}$

By putting all this together we can obtain a diagonal filler from the diagram
illustrated in Fig. 8, where
$e=\delta_{\Delta}^{+}.(\delta_{Q}\circ\delta_{\Delta}^{+}$, and where the
central diagonal filler exists by hypothesis.

If $h\in\mathscr{P}$, then by definition of $\mathcal{L}_{\mathscr{P}}$ it has
the right-lifting property with respect to all
$f\in\mathcal{L}_{\mathscr{P}}$; we deduce then
$\mathscr{P}^{*}\subseteq\mathcal{R}_{\mathscr{P}}$. This proves that
$p_{f}\in\mathcal{R}_{\mathscr{P}}$.

Since $\mathcal{L}_{\mathscr{P}}^{\pitchfork}=\mathcal{R}_{\mathscr{P}}$ holds
by definition, it remains to prove that
$\mathcal{L}_{\mathscr{P}}=^{\pitchfork}\mathcal{R}_{\mathscr{P}}$. On the one
hand, from $\mathscr{P}\subseteq\mathcal{R}_{\mathscr{P}}$, we deduce
${}^{\pitchfork}\mathcal{R}_{\mathscr{P}}\subseteq^{\pitchfork}\mathscr{P}\subseteq\mathcal{L}_{\mathscr{P}}$.
For the converse direction, by the Retract Argument (Lemma 1.1.9 in [19]), any
$g\in\mathcal{R}_{\mathscr{P}}$ is a retract of a projection: from
$g=p_{g}\circ i_{g}$, and the fact that $g$ has the right lifting property
with respect to $i_{g}$, we deduce that there exists $h$ (a diagonal filler of
$p_{g}\circ i_{g}=g\circ\mathrm{id}_{X}$) such that $g\circ h=p_{g}$. This
implies in particular that there is a diagram of the form

${X}$${A}$${X}$${Y}$${Y}$${Y}$$\scriptstyle{\mathrm{id}_{X}}$$\scriptstyle{g}$$\scriptstyle{i_{g}}$$\scriptstyle{p_{g}}$$\scriptstyle{h}$$\scriptstyle{g}$

Using this we can show that given a diagram of the form

${C}$${X}$${D}$${Y}$$\scriptstyle{f}$$\scriptstyle{k}$$\scriptstyle{g}$$\scriptstyle{k^{\prime}}$

where $f\in\mathcal{L}_{\mathscr{P}}$, we can construct a diagram

${C}$${X}$${A}$${X}$${D}$${Y}$${Y}$${Y}$$\scriptstyle{f}$$\scriptstyle{k}$$\scriptstyle{1_{X}}$$\scriptstyle{g}$$\scriptstyle{i_{g}}$$\scriptstyle{h}$$\scriptstyle{p_{g}}$$\scriptstyle{g}$$\scriptstyle{j}$$\scriptstyle{k^{\prime}}$

where the diagonal filler $j$ exists since $f$ has the left-lifting property
with respect to $p_{g}$, and from which we obtain a diagonal filler
$j^{\prime}=h\circ j$ for the original diagram. We have thus shown that any
$f\in\mathcal{L}_{\mathscr{P}}$ has the left-lifting property with respect to
any $g\in\mathcal{R}_{\mathscr{P}}$, and thus
$\mathcal{L}_{\mathscr{P}}\subseteq^{\pitchfork}\mathcal{R}_{\mathscr{P}}$. ∎

${(2)}$${\Gamma}$${\Gamma.\Delta\mid\Delta_{f}.Q}$${\Gamma.\Delta.\Delta\mid\pi_{\Gamma.\Delta}^{\sharp}(\Delta_{f}).\pi_{\Gamma.\Delta}^{\sharp}(Q).\pi_{\Gamma.\Delta}^{\sharp}(Q)}$${\Gamma.\Delta\mid\Delta_{f}.Q}$${(1)}$${(3)}$${\Gamma.\Delta\mid\Delta_{f}}$${\Gamma.\Delta.\Delta\mid\pi_{\Gamma.\Delta}^{\sharp}(\Delta_{f}).\pi^{\sharp}_{\Gamma.\Delta}(Q).\Delta^{\mathsf{D}}}$${\Gamma.\Delta.\Delta}$${\Gamma.\Delta}$$\scriptstyle{c}$$\scriptstyle{i_{f}}$$\scriptstyle{i_{f}.c}$$\scriptstyle{i_{\Gamma\mid\Delta_{f}.Q,\Delta}}$$\scriptstyle{e}$$\scriptstyle{\pi_{\Gamma.\Delta.\Delta}}$$\scriptstyle{(\pi_{\Gamma.\Delta}^{+}\circ\pi_{2}).(\pi_{\Gamma.\Delta}^{+}\circ\pi_{3})}$$\scriptstyle{\pi_{\Gamma.\Delta}}$$\scriptstyle{\pi_{\Gamma.\Delta}}$$\scriptstyle{\delta_{\Delta}^{+}.(\delta_{Q}\circ
c).i_{\Gamma.\Delta}}$$\scriptstyle{j_{\Gamma\mid\pi^{\sharp}_{\Gamma.\Delta}(\Delta_{f}.Q),\Delta,Q,e}}$$\scriptstyle{\pi_{\Gamma.\Delta.\Delta}}$$\scriptstyle{\pi_{\Gamma.\Delta}}$

Figure 8: Construction of the diagonal filler.

##  Appendix D Metric Preservation: Details

We will need the following generalization of the notion of metric space: a
_parameterized (pseudo-)metric space_ (PMS) is a triple $(X,K,a)$, where
$a:X\times X\to(\mathbb{R}_{\geq 0})^{K}$ satisfies, for all $k\in K$:

$\displaystyle a(x,x)(k)$ $\displaystyle=0$ $\displaystyle a(x,y)(k)$
$\displaystyle=a(y,x)(k)$ $\displaystyle a(x,y)(k)$ $\displaystyle\leq
a(x,z)(k)+a(z,y)(k)$

Usual (pseudo-)metric spaces can be identified with PMS $(X,K,a)$ where $K$ is
a singleton.

We recall that $\mathrm{Met}$ is the category of pseudo-metric spaces and non-
expansive map. $\mathrm{Met}$ is symmetric monoidal closed; its monoidal
product is $(X,a)\otimes(Y,b)=(X\times Y,a+b)$ and the right-adjoint to
$\otimes$ is $[(X,a),(Y,b)]=(\mathrm{Met}(X,Y),b_{\sup})$, where
$b_{\sup}(f,g)=\sup\\{b(f(x),g(x))\mid x\in X\\}$. It is a standard fact that
$\mathrm{Met}$ has enough structure to interpret ST$\lambda$C!, with $!_{r}A$
corresponding to the rescaling of a metric space by $r$.

We now describe the $\mathrm{dTT}$-structure associated with the forgetful
functor $U:\mathrm{Met}\to\mathrm{Set}$.

For any set $X$, the class of pure predicates $\mathscr{P}^{\flat}(X)$ is made
of all PMS of the form $P=(X,K,a)$, with $(X\otimes X\mid
P)=\coprod_{x,x^{\prime}\in X}\prod_{k\in K}\widetilde{a}(x,x^{\prime})(k)$
and projection $\pi_{X}:(X\otimes X\mid P)\to X\times X$. The class
$\mathscr{P}(X)$ contains all pullbacks $\langle f,g\rangle^{\sharp}P$, for
all $P=(X,K,a)\in\mathscr{P}^{\flat}(X)$ and $\langle
f,g\rangle\in\mathrm{Met}(Y,X\otimes X)$, with $(Y\mid\langle
f,g\rangle^{\sharp}P)=\coprod_{y\in Y}\prod_{k\in
K}\widetilde{a}(f(y),g(y))(k)$ and projection $\pi_{Y}:(Y\mid\langle
f,g\rangle^{\sharp}P)\to Y$.

Observe that for any projection $\pi:X\times Y\to X$ and PMS $(X,K,a)$,
$(X,K,\pi^{\sharp}a)$ is still a PMS, where
$\pi^{\sharp}a(u,v)(k)=a(\pi_{1}(u),\pi_{1}(v))(k)$ (in fact,
$\pi^{\sharp}a(u,u)=a(\pi_{1}(u),\pi_{1}(u))=0$,
$\pi^{\sharp}a(u,v)=a(\pi_{1}(u),\pi_{1}(v))=a(\pi_{1}(v),\pi_{1}(u))=\pi^{\sharp}a(v,u)$,
and $\pi^{\sharp}a(u,v)=a(\pi_{1}(u),\pi_{1}(v))\leq
a(\pi_{1}(u),\pi_{1}(w))+a(\pi_{1}(w),\pi_{1}(v))=\pi^{\sharp}a(u,w)+\pi^{\sharp}a(w,v)$).

Moreover, for all PMS $(X\times X,K,a)$, also $(X,K,\delta_{X}^{\sharp}a)$ is
a metric space, where $\delta_{X}^{\sharp}a(x,y)(k)=a(\langle
x,x\rangle,\langle y,y\rangle)(k)$ ( in fact
$\delta_{X}^{\sharp}a(x,x)(k)=a(\langle x,x\rangle,\langle x,x\rangle)(k)=0$,
$\delta_{X}^{\sharp}a(x,y)(k)=a(\langle x,x\rangle,\langle
y,y\rangle)(k)=a(\langle y,y\rangle,\langle
x,x\rangle)(k)=\delta_{X}^{\sharp}a(y,x)(k)$, and
$\delta_{X}^{\sharp}a(x,y)(k)=a(\langle x,x\rangle,\langle y,y\rangle)(k)\leq
a(\langle x,x\rangle,\langle z,z\rangle)(k)+a(\langle z,z\rangle,\langle
y,y\rangle)(k)=\delta_{X}^{\sharp}a(x,z)(k)+\delta_{X}^{\sharp}a(z,y)(k)$).

An arrow in the slice category $\mathrm{Set}_{\mathscr{P}}^{X}$ between
$\coprod_{x\in X}\prod_{k\in K}\widetilde{a}(f(x),g(x))(k)$ and
$\coprod_{x\in X}\prod_{h\in H}\widetilde{b}(f^{\prime}(x),g^{\prime}(x))(h)$
is given by a function $\varphi:X\times(\mathbb{R}_{\geq 0})^{K}\times
H\to\mathbb{R}_{\geq 0}$ such that
$\varphi(x,\phi,h)\in\widetilde{b}(f^{\prime}(x),g^{\prime}(x))(h)$. Given PMS
$P=(Y,K,a)$ and $Q=(Z,H,b)$, let $P*Q=(Y\times Z,K+H,a+b)$, where $a+b(\langle
y,z\rangle,\langle y^{\prime},z^{\prime}\rangle)(\langle
0,k\rangle)=a(y,y^{\prime})(k)$ and $a+b(\langle y,z\rangle,\langle
y^{\prime},z^{\prime}\rangle)(\langle 1,h\rangle)=b(z,z^{\prime})(k)$. One can
check that:

  * •

for all predicates $P=\langle f,g\rangle^{\sharp}P^{\prime}$ and $Q=\langle
f^{\prime},g^{\prime}\rangle^{\sharp}Q^{\prime}\in\mathscr{P}(X)$, where
$P^{\prime}\in\mathscr{P}^{\flat}(Y)$ and
$Q^{\prime}\in\mathscr{P}^{\flat}(Z)$ are the PMS $(Y,K,a)$ and $(Z,H,b)$, the
product $P\times Q\in\mathscr{P}(X)$ is $\langle\langle
f,f^{\prime}\rangle,\langle g,g^{\prime}\rangle\rangle^{\sharp}(P*Q)$, with
$(X\mid P\times Q)=\coprod_{x\in X}\prod_{u\in
K+H}(\widetilde{a}(f(x),g(x))+\widetilde{b}(f^{\prime}(x),g^{\prime}(x)))(u)$.
Observe that if $P,Q\in\mathscr{P}^{\flat}(X)$, then $P\times
Q=P*Q\in\mathscr{P}^{\flat}(X)$.

  * •

for any pure predicate $P=(X,K,a)\in\mathscr{P}^{\flat}(X)$ and set $I$, the
dependent product $\Pi_{I}P\in\mathscr{P}^{\flat}(X^{I})$ is the PMS
$(X^{I},I\times K,\Pi_{I}a)$ where $(\Pi_{I}a)(f,g)(\langle
i,k\rangle)=a(f(i),g(i))(k)$;

  * •

for all PMS $P=(X,K,a)$ and $Q=(Y,K,b)\in\mathscr{P}(Y)$, the dependent
product $Q^{\left(X^{\mathsf{D}}\right)}\in\mathscr{P}^{\flat}(Y^{X\times X})$
is the PMS $(Y^{X\times X},H\times(X\otimes X\mid P),\mathfrak{p}_{a,b})$,
where $\mathfrak{p}_{a,b}(f,g)(\langle h,\langle\langle
x,y\rangle,\phi\rangle\rangle)=b(f(x,y),g(x,y))(h)$.

The difference structure is as follows:

  * •

for all metric spaces $(X,a)$, $X^{\mathsf{D}}\in\mathscr{P}^{\flat}(X)$ is
$(X,a)$ itself, seen as a PMS;

  * •

for all metric spaces $(X,a)$, and set $Y$, predicate $P=\langle
f,g\rangle^{\sharp}P^{\prime}\in\mathscr{P}(Y\otimes(X\otimes X))$, (with
$(Y\otimes X\otimes X\mid P)=\coprod_{y\in Y,x,x^{\prime}\in X}\prod_{k\in
K}\widetilde{a}(f(y,x,x^{\prime}),g(y,x,x^{\prime}))$, the pullback $(Y\otimes
X\mid\delta_{X}^{\sharp}P)$ is $\coprod_{y\in Y,x\in X}\prod_{k\in
K}\widetilde{a}(f(y,x,x),g(y,x,x))$; the morphism $r_{Y,X\mid P}:(Y\otimes
X\mid\delta^{\sharp}_{X}P)\to(Y\otimes X\otimes X\mid P\times X^{\mathsf{D}})$
is given by $r_{Y,X\mid P}(\langle\langle
y,x\rangle,\phi\rangle)(k)=\langle\langle y,x,x\rangle,\phi+0\rangle$.

  * •

for all metric spaces $(X,a)$, $(Y,b)$ predicate $P=\langle
m,n\rangle^{\sharp}P^{\prime}\in\mathscr{P}(Y\otimes X\otimes X)$ (with
$(Y\otimes X\otimes X\mid P)=\coprod_{y\in Y,x,x^{\prime}\in X}\prod_{h\in
H}\widetilde{b}(m(y,x,x^{\prime}),n(y,x,x^{\prime}))(h)$, pure predicate
$Q=(Z,K,e)\in\mathscr{P}^{\flat}(Z)$, non-expansive functions $\langle
f,g\rangle\in\mathrm{Met}(Y\otimes X\otimes X,Z\otimes Z)$ and for any
function $c:(Y^{\prime}\otimes X\mid\delta_{X}^{\sharp}P)\to(Y\otimes X\otimes
X\mid P\times\langle f,g\rangle^{\sharp}Q)$ satisfying $c(\langle\langle
y,x\rangle,\phi\rangle)=\langle\langle
y,x,x\rangle,c^{\prime}(y,x,\phi)\rangle$, with
$c^{\prime}(y,x,\phi):H+K\to\mathbb{R}_{\geq 0}$ satisfying
$c^{\prime}(y,x,\phi)(\langle 0,k\rangle)=\phi(k)$ and
$c^{\prime}(y,x,\phi)(\langle 1,h\rangle)\in\widetilde{e}(f(y,x,x),g(y,x,x))$,
for all $y\in Y^{\prime}$, $x,x^{\prime}\in X$, $\phi\in(\mathbb{R}_{\geq
0})^{K}$ with $\phi(k)\geq b^{\prime}(x,x^{\prime})(k)$ and $r\geq
a(x,x^{\prime})$, we let $\big{(}j_{Y,X,Q,\langle
f,g\rangle,P,c}(\langle\langle
y,x,x^{\prime}\rangle,\langle\phi,r\rangle\rangle)\big{)}_{2}=\psi_{y,x,x^{\prime},\phi,r}:H+K\to\mathbb{R}_{\geq
0}$, where $\psi_{y,x,x^{\prime},\phi,r}(\langle 0,k\rangle)=\phi(k)$, and
$\psi_{y,x,x^{\prime},\phi,r}(\langle 1,h\rangle)=c^{\prime}(y,x,\phi)(\langle
1,h\rangle)+r$.

In fact, since $\phi(k)\geq b^{\prime}(x,x^{\prime})(k)\geq
b^{\prime}(x,x)(k)$, we have $c^{\prime}(y,x,\phi)(\langle 1,h\rangle)\geq
e(f(y,x,x),g(y,x,x))(h)$; moreover, from $\langle
f,g\rangle\in\mathrm{Met}(Y\otimes X\otimes X,Z\otimes Z)$ it follows
$e(f(y,x,x^{\prime}),f(y,x,x))+e(g(y,x,x),g(y,x,x^{\prime}))\leq
b(y,y)+a(x,x)+a(x,x^{\prime})=a(x,x^{\prime})\leq r$; then, using the
triangular law, we deduce $c^{\prime}(y,x,\phi)(\langle 1,h\rangle)+r\geq
e^{\prime}(f(y,x,x^{\prime}),g(y,x,x^{\prime})(h)$.

Observe that $((j_{Y,X,Q,\langle f,g\rangle,P,c}\circ r_{Y,X\mid
P})(x,y,\phi))_{2}=c^{\prime}(y,x,\phi)$. Moreover, when $Q=X^{\mathsf{D}}$,
$f(y,x,x^{\prime})=x$, $g(y,x,x^{\prime})=x^{\prime}$ and
$c^{\prime}(y,x,\phi)(\langle 1,h\rangle)=0$, we deduce that $j_{Y,X,Q,\langle
f,g\rangle,P,c}=\mathrm{id}_{Y\times X\times X\mid Q\times X^{\mathsf{D}}}$.
Hence both the $\beta$\- and $\eta$-rules are valid.

We leave to the reader to check that the validity of all required coherence
conditions.

### Extensionality

This model does not satisfy any of the extensionality axioms discussed in
Section 2. In fact, the type $D_{A\otimes B}$ is interpreted by the PMS
corresponding to the monoidal product in $\mathrm{Met}$ of (the interpretation
of) $D_{A}$ and $D_{B}$, which does _not_ coincide with the product in
$\mathscr{P}(\llbracket A\rrbracket\times\llbracket B\rrbracket)$.

Similarly, the type $D_{A\multimap B}$ is interpreted by the PMS corresponding
to the right-adjoint to the monoidal product in $\mathrm{Met}$, which does
_not_ coincide with either of the two dependent products of predicates.

##  Appendix E Differential Logical Relations: Details

A DLR is a triple $(X,L,\rho)$ where $X$ is a set, $L$ is a complete lattice
and $\rho\subseteq X\times L\times X$. A map of DLR $(X,L,\rho)$ and
$(Y,M,\mu)$ is a pair $(f,\varphi)$, where $f:X\to Y$ and $\varphi:X\times
X\times L\to M$ is such that $\rho(x,\epsilon,y)$ implies
$\mu(f(x),\varphi(x,y,\epsilon),f(y))$ and
$\mu(f(y),\varphi(x,y,\epsilon),f(x))$. This notion of map is a slight
variation with respect to [13], where the auxiliary map $\varphi$ goes from
$X\times L$ to $M$. Yet, this change does not affect the higher-order
structure of DLR (see below), and the two families of maps are related by a
retraction ${M^{X\times L}}$${M^{X\times X\times
L}}$$\scriptstyle{h}$$\scriptstyle{k}$ where
$h(\varphi)(x,y,\epsilon)=\varphi(x,\epsilon)$ and
$k(\psi)(x,\epsilon)=\sup\\{\psi(x,y,\epsilon)\mid y\in
X\land\rho(x,\epsilon,y)\\}$.

DLR and their maps form a category $\mathsf{DLR}$, where the identity of a DLR
$(X,L,\rho)$ is the map $(f,\lambda xy\epsilon.\epsilon)$, and composition of
$(f,\varphi)$ and $(g,\psi)$ is $(g\circ
f,x,y,\epsilon\mapsto\psi(f(x),f(y),\psi(x,y,\epsilon))$.

$\mathsf{DLR}$ is cartesian closed, with the product and exponential of DLR
$(X,L,\rho)$ and $(Y,M,\mu)$ being the DLR $(X\times Y,L\times
M,\rho\times\mu)$ and $(Y^{X},M^{X\times X\times L},\rho^{(X\times
X\times\mu)})$, where $\rho^{(X\times X\times\mu)}(f,\varphi,g)$ holds if
$\rho(x,\epsilon,y)$ implies $\mu(f(x),\varphi(x,y,\epsilon),f(y))$,
$\mu(f(x),\varphi(x,y,\epsilon),g(y))$, $\mu(g(x),\varphi(x,y,\epsilon),f(y))$
and $\mu(g(x),\varphi(x,y,\epsilon),g(y))$.

We now describe the $\mathrm{dTT}$-structure associated with the forgetful
functor $U:\mathsf{DLR}\to\mathrm{Set}$.

For any set $X$, $\mathscr{P}^{\flat}(X)$ is made of all DLR of the form
$P=(X,L,\rho)$, with $X\times X\mid P=\coprod_{x,x^{\prime}\in
X}\widetilde{\rho}(x,x^{\prime})$, and projection $\pi_{X}:(X\times X\mid
P)\to X\times X$. $\mathscr{P}(Y)$ is made of all pullbacks $\langle
f,g\rangle^{\sharp}P$, where $P=(X,L,\rho)\in\mathscr{P}^{\flat}(X)$, and
$f,g:Y\to X$, with $(Y\mid\langle f,g\rangle^{\sharp}P)=\coprod_{y\in
Y}\widetilde{\rho}(f(y),g(y))$ and projection $\pi_{Y}:(Y\mid\langle
f,g\rangle^{\sharp}P)\to Y$.

An arrow in the slice category $\mathrm{Set}_{\mathscr{P}}^{X}$ between
$\coprod_{x\in X}\widetilde{\rho}(f(x),g(x))$ and $\coprod_{x\in
X}\widetilde{\mu}(f^{\prime}(x),g^{\prime}(x))$ (for given DLR $(X,L,\rho)$
and $(Y,M,\mu)$) is given by a function $\varphi:X\times L\to M$ such that
$\rho(f(x),\epsilon,g(x))$ implies
$\mu(f^{\prime}(x),\varphi(x,\epsilon),g^{\prime}(x))$. One can check that:

  * •

for all predicates $P=\langle f,g\rangle^{\sharp}P^{\prime}\in\mathscr{P}(X)$
and $Q=\langle
f^{\prime},g^{\prime}\rangle^{\sharp}Q^{\prime}\in\mathscr{P}(X)$, their
product is the predicate $\langle\langle f,f^{\prime}\rangle,\langle
g,g^{\prime}\rangle\rangle^{\sharp}(P^{\prime}\times
Q^{\prime})\in\mathscr{P}(X)$. Observe that if $P$ and $Q$ are in
$\mathscr{P}^{\flat}(X)$, then $P\times Q\in\mathscr{P}^{\flat}(X)$;

  * •

for all pure predicate $P=(X,L,\rho)\in\mathscr{P}^{\flat}(X)$ and set $I$,
the dependent product $\Pi_{I}P\in\mathscr{P}^{\flat}(X^{I})$ is the DLR
$(X^{I},L^{I},\rho^{I})$, where $\rho^{I}(f,\varphi,g)$ iff $\forall i\in I$,
$\rho(f(i),\varphi(i),g(i))$;

  * •

for all DLR $(X,L,\rho)$ and pure predicate
$Q=(Y,M,\mu)\in\mathscr{P}^{\flat}(Y)$, the dependent product
$P^{\left(X^{\mathsf{D}}\right)}\in\mathscr{P}(Y^{X\times X})$ is the
exponential of $(X,L,\rho)$ and $Q$ in $\mathsf{DLR}$.

The difference structure is as follows:

  * •

for all DLR $(X,L,\rho)$, $X^{\mathsf{D}}\in\mathscr{P}^{\flat}(X)$ is just
$(X,L,\rho)$;

  * •

for all DLR $(X,L,\rho)$, set $Y$ and predicate $P=\langle
f,g\rangle^{\sharp}P^{\prime}\in\mathscr{P}(Y\times X\times X)$, where
$(Y\times X\times X\mid P)=\coprod_{y\in Y,x,x^{\prime}\in
X}\widetilde{\mu}(f(y,x,x^{\prime}),g(y,x,x^{\prime}))$, the pullback
$(Y\times X\mid\delta_{X}^{\sharp}P)$ is $\coprod_{y\in Y,x\in
X}\widetilde{\mu}(f(y,x,x),g(y,x,x))$, while $(Y\times X\times X\mid P\times
X^{\mathsf{D}})$ is $\coprod_{y\in Y,x,x^{\prime}\in
X}\widetilde{\mu}(f(y,x,x^{\prime}),g(y,x,x^{\prime}))\times\widetilde{\rho}(x,x^{\prime})$;
we let then $r_{Y,X\mid P}(\langle\langle y,x\rangle,s\rangle)=\langle\langle
y,x,x\rangle,\langle s,\|x\|_{\rho}\rangle\rangle$;

  * •

for all DLR $(X,L,\rho)$, sets $Y,Z,W$, predicate $Q=\langle
m,n\rangle^{\sharp}Q^{\prime}\in\mathscr{P}(Y\times X\times X)$, with
$(Y\times X\times X\mid Q)=\coprod_{y\in Y,x,x^{\prime}\in
X}\widetilde{\lambda}(m(y,x,x^{\prime}),n(y,x,x^{\prime}))\in\mathscr{P}(Y\times
X\times X)$, pure predicate $P=(Z,M,\mu)\in\mathscr{P}^{\flat}(Z)$ and arrows
$f,g:Y\times X\times X\to Z$, for all morphisms $c:(Y\times
X\mid\delta_{X}^{\sharp}Q)\to(Y\times X\times X\mid Q\times\langle
f,g\rangle^{\sharp}P)$ such that $c(\langle\langle
y,x\rangle,s\rangle)=\langle\langle y,x,x\rangle,\langle
s,c^{\prime}(y,x,s)\rangle\rangle$, with
$c^{\prime}(y,x,s)\in\widetilde{\mu}(f(y,x,x),g(y,x,x))$, we can define a
diagonal filler $j:(Y\times X\times X\mid Q\times X^{\mathsf{D}})\to(Y\times
X\times X\mid Q\times\langle f,g\rangle^{\sharp}P)$ by

$(j(\langle\langle y,x,x^{\prime}\rangle,\langle
s,r\rangle\rangle))_{2}=\langle
s,\sup\\{c^{\prime}(y,x,s),\inf\widetilde{\mu}(f(y,x,w),g(y,x,w))\mid w\in
X\land\rho(x,r,w)\\}\rangle$

We have that $((j\circ r_{Y,X\mid Q})(\langle y,x\rangle))_{2}=\langle
s,c^{\prime}(y,x,s)\rangle$, since by separatedness $\rho(x,\|x\|_{\rho},w)$
implies $w=x$, and
$\inf\widetilde{\mu}(f(y,x,x),g(y,x,x))=\|f(y,x,x),g(y,x,x)\|_{\mu}\leq
c^{\prime}(y,x,s)$.

We leave to the reader to check the validity of all required coherence
conditions.

### Extensionality

The DLR model of $\mathrm{dTT}$ satisfies the extensionality axioms
($\mathsf{CExt}$) and ($\mathsf{FExt2}$). In fact, given simple types $A,B$,
the interpretation of $D_{A\times B}$ is generated by the cartesian product in
$\mathsf{DLR}$ of the interpretations of $D_{A}$ and $D_{B}$, which coincides
with the product in $\mathscr{P}(\llbracket A\rrbracket)$. Moreover, the
interpretation of $D_{A\to B}$ is generated by the exponential of $D_{A}$ and
$D_{B}$ in $\mathsf{DLR}$, which coincides with the pullback along $\langle
h,h\rangle$ of the dependent product of the interpretation of $D_{B}$ and $A$,
where $h,h:Y^{X}\to Y^{X\times X}$ is given by $h(f)(x,y)=f(x)$, and this in
turn coincides with the interpretation of the type $(\Pi x,y\in
A)(D_{A}(x,y)\to D_{B}(f(x),g(y)))$.

One can also check that derivatives satisfy the equational rules
($\mathsf{J}\times a$), ($\mathsf{J}\times b$),($\mathsf{J}\times c$),
($\mathsf{J}\lambda 2a$) and ($\mathsf{J}\lambda 2b$).

##  Appendix F Change Structures: Details

Change structures (as defined in Section 6) and functions form a category
$\mathsf{CS}$ which is cartesian closed. In particular, given CS
$(X,\Delta_{X},\oplus,\ominus)$ and
$(Y,\Delta_{Y},\oplus^{\prime},\ominus^{\prime})$, their cartesian product is
$(X\times
Y,\Delta_{X}\times\Delta_{Y},\oplus\times\oplus^{\prime},\ominus\times\ominus^{\prime})$,
and their exponential
is$(Y^{X},(\Delta_{Y})^{X\times\Delta_{X}},\oplus^{*},\ominus^{*})$, where
$(\Delta_{Y})^{X\times\Delta_{X}}(f)$ contains all functions
$\varphi:X\times\Delta_{X}\to\Delta_{Y}$, such that for all $x\in X$ and
$\mathsf{d}x\in\Delta_{X}x$, $\varphi(x,\mathsf{d}x)\in\Delta_{X}f(x)$,
$(f\oplus^{*}\varphi)(x)=f(x)\oplus^{\prime}\varphi(x,\mathbf{0}_{x})$ and
$(f\ominus^{*}g)(x,\mathsf{d}x)=f(x\oplus\mathsf{d}x)\ominus g(x)$.

We now describe the $\mathrm{dTT}$-structure associated with the forgetful
functor $U:\mathsf{CS}\to\mathrm{Set}$.

For any set $X$, $\mathscr{P}^{\flat}(X)$ is made of CS with base set $X$,
where for a CS $P=(X,\Delta_{X},\oplus,\ominus)$, $(X\times X\mid
P)=\coprod_{x,x^{\prime}\in X}\Delta_{X}(x,x^{\prime})$, with projection
$\pi_{X}:X\times X\mid P\to X\times X$. $\mathscr{P}(Y)$ is made of all