The Cartesian Closed Bicategory
of Thin Spans of Groupoids

Pierre Clairambault
Aix Marseille Univ, Université
de Toulon, CNRS, LIS, Marseille

Email<EMAIL_ADDRESS>Simon Forest
Aix Marseille Univ, CNRS, I2M, Marseille, France

Email<EMAIL_ADDRESS>
Recently, there has been growing interest in bicategorical models of
programming languages, which are “proof-relevant” in the sense that
they keep distinct account of execution traces leading to the same
observable outcomes, while assigning a formal meaning to reduction paths
as isomorphisms.

In this paper we introduce a new model, a bicategory called thin
spans of groupoids. Conceptually it is close to Fiore et al.'s
generalized species of structures and to Melliès' homotopy
template games, but fundamentally differs as to how
replication of resources and the resulting symmetries are treated.
Where those models are saturated – the interpretation is
inflated by the fact that semantic individuals may carry arbitrary
symmetries – our model is thin, drawing inspiration
from thin concurrent games: the interpretation of
terms carries no symmetries, but semantic individuals satisfy a subtle
invariant defined via biorthogonality, which guarantees their
invariance under symmetry.

We first build the bicategory $\Thin$ of thin spans of groupoids. Its
objects are certain groupoids with additional structure, its morphisms
are spans composed via plain pullback with identities the identity
spans, and its $2$-cells are span morphisms making the induced
triangles commute only up to natural isomorphism. We then equip $\Thin$
with a pseudocomonad $\oc$, and finally show that the Kleisli
bicategory $\Thin_{\oc}$ is cartesian closed.

§ INTRODUCTION

The relational model [1] is one of
the most basic and elementary denotational models for linear logic or
the $\lambda$-calculus. At its heart, it is simply an interpretation of
formulas / types as sets and proofs / programs as relations,
i.e. in the category $\Rel$. Despite its simplicity the
relational model is ubiquitous: it is the basic substrate for the
spectrum of so-called web-based models of linear logic, including
coherence or finiteness spaces [2]. It
faithfully predicts reduction time
[3]. It supports quantitative
extensions such as in probabilistic coherence spaces
[4], the weighted relational model
[5], and even up to quantum computation
[6] – quantitative extensions which enjoy
powerful full abstraction results
[7, 8].
Presented syntactically, the relational model exactly corresponds to
non-idempotent intersection types
[9], a currently active research
topic in its own right (see e.g.
[10, 11])
which enables a syntactic methodology to addressing semantic questions.
Finally, it has a tight connection with game semantics
[12, 13],
of which it appears as a desequentialization (see e.g.
[14, 15, 16, 8]).
In short, it is at the crossroads of multiple topics, past and current,
of the denotational semantics universe.

Another recent trend in denotational semantics is the adoption of
bicategorical models [17] where the
familiar categorical laws hold only up to certain $2$-cells
satisfying coherence conditions – in particular, Fiore and
Saville have recently thoroughly explored cartesian closed
bicategories [18]. In such models, the
denotation is no longer an invariant of reduction: two convertible
terms yield merely isomorphic objects, and reduction
paths have a genuine interpretation as specific isomorphisms
[19] –
thus bringing reduction into the categorical model. There are still
not many concrete bicategorical models, and we are aware of only three
(families of) such models that can deal with non-linear computation, in
chronological order: firstly, Fiore, Gambino, Hyland and Winskel's
cartesian closed bicategory of generalized species of structure
[20]; secondly, Castellan, Clairambault and
Winskel's thin concurrent games
[21] (as established by Paquet
[22]); thirdly, Melliès'
homotopy template games [23]. Of
these three, the first is by far the most studied with various works
including generalizations and application to semantics
[24, 25, 26],
links with intersection types and Taylor expansion
[27, 28], or
applications to the pure $\lambda$-calculus [29]. Beyond
giving a non-degenerated interpretation to reduction paths, those
concrete bicategorical models are “proof-relevant”, in the sense that
they keep distinct semantic witnesses for the possibly multiple
evaluation traces with the same observable behaviour and thus keep a
clear, branching account of non-determinism.

These models have something else in common: in their construction, the
main subtlety has to do with replication, i.e. the
modality $\oc$ of linear logic. In the relational model, $\oc A$ is
the set $\Mf(A)$ of finite multisets of elements of $A$, or
alternatively, the free monoid $A^*$ quotiented by permutations.
In bicategorical models, this is replaced by a
categorification of $\Mf(A)$: a category (or groupoid) whose
objects keep separate individual resource usages (e.g.
$A^*$). Its morphisms are explicit permutations, often called
symmetries in this paper. Individuals in the model must refer to
specific resources (e.g. $a_i$ in $a_1 \dots a_n \in A^*$), but
the categorical laws expected for models of programming languages
requires that their behaviour should still be invariant under symmetry.
In both generalized species of structure and template games, this is
done by saturating the set of witnesses with respect to
symmetries: intuitively, the behaviour of an individual cannot depend
on the specific identity of resources, because those resources are seen
through the “noise” of all possible symmetries – this shall be
reviewed gently in <Ref>. This saturation
complicates models and their construction, though for good
reasons.  But this contrasts with thin concurrent
games, which handles symmetry with a mechanism inspired by
Abramsky-Jagadeesan-Malacaria games
[12] and Melliès' orbital
games [15]: strategies are not
saturated, but their invariance under “Opponent's
symmetries” is ensured by a subtle bisimulation-like structure – we
call this the thin approach.

We believe that the thin approach is helpful at least for applications
to semantics: the absence of symmetries on witnesses allow a more concrete
flavour which may help when ordering individuals allowing continuous
reasoning[For instance, in [29], the
generalization from finite to infinite computation is not simply by
continuity as per usual in denotational semantics, because of the
quotient involved in the management of saturation.], or
simplify quantitative extensions such as
[24]. But more fundamentally, there is a
clear tension between these two worlds that deserves investigation. Are
proof-relevant relational models inherently saturated? Is the thin
approach only possible in games thanks to the presence of time and
causality? These fundamental questions may be of interest beyond denotational
semantics, as the handling of symmetry in such models is
deeply connected to algebraic combinatorics [20]
and homotopy theory [23].

Contributions We introduce the bicategory $\Thin$ of thin
spans of groupoids: its objects are certain groupoids with additional
structure, its morphisms certain spans, and its $2$-cells certain
weak span morphisms, i.e. making the induced triangles
commute up to chosen natural isos. Identities are
identity spans, and composition of spans is by plain pullback.

Of course, plain pullbacks are too weak to support the horizontal
composition of weak span morphisms. To address this, we first define
uniform spans via a biorthogonality construction, ensuring that
the composition pullbacks also satisfy the bipullback universal
property. This allows us to compose $2$-cells horizontally, but that
horizontal composition is still not canonically defined and fails to
give a bicategory.

For the next step, we import from thin concurrent games and from
Melliès' orbital games a decomposition of symmetries into
positive symmetries (due to the program), and negative
symmetries (due to the environment). We then define thin spans
via a second biorthogonality construction, which ensures that the
horizontal composition of weak span morphisms are canonically defined
as long as we consider positive weak span morphisms, where the
chosen iso only involves positive symmetries. We show this results in a
bicategory $\Thin$. Furthermore, we equip $\Thin$ with a pseudocomonad
$\oc$, and show that the Kleisli bicategory $\Thin_{\oc}$ is cartesian

Outline In <Ref> we start with a
gentle introduction to the relational model and its proof-relevant
extensions. In <Ref> we introduce the bicategory
$\Thin$, deploying first the uniform orthogonality and then the thin
orthogonality. In <Ref> we introduce the
pseudocomonad $\oc$, and show that the Kleisli bicategory $\Thin_{\oc}$
is cartesian closed.

§ RELATIONAL MODELS, SPANS, SPECIES

§.§ The Relational Model

The relational model is one of the simplest denotational models
of the $\lambda$-calculus, linear logic, or simple programming
languages such as $\PCF$. It consists in simply interpreting every type
$A$ as a set $\intr{A}$, and a program $\vdash M : A$ as a subset of
$\intr{A}$. This set $\intr{A}$ is often called the web
seeing that it is the first component of the so-called web-based models
of linear logic such as coherence spaces and their extensions. One may
think of elements of $\intr{A}$ as completed executions (which is
straightforward enough for ground types such as booleans or natural
numbers but may be more complex for higher-order types), and of
$\intr{M} \subseteq \intr{A}$ as simply the collection of all the
completed executions that $M$ may achieve.

The ground type for booleans is interpreted as $\intr{\tbool} =
\{\ttrue, \tfalse\}$, and the constant $\vdash \ttrue : \tbool$ as
$\intr{\ttrue} = \{\ttrue\}$.

The interpretation of a program $M$ is computed compositionally,
following the methodology of denotational semantics, organized
by the categorical structure of sets and relations.

§.§.§ Basic categorical structure

There is a category $\Rel$ with sets as objects, and as morphisms
the relations from $A$ to $B$, i.e. subsets $R
\subseteq A \times B$. The identity on $A$ is the diagonal relation
$\{(a, a) \mid a \in A\} \subseteq A \times A$, and the composition of
$R \subseteq A \times B$ and $S \subseteq B \times C$ consists in all
pairs $(a, c) \in A\times B$ such that $(a, b) \in R$ and $(b, c) \in
S$ for some $b \in B$.

Besides, $\Rel$ has a monoidal structure given by the cartesian product
on objects, and for $R_i \in \Rel(A_i, B_i)$, $R_1 \times R_2 \in
\Rel(A_1 \times A_2, B_1 \times B_2)$ set as comprising all $((a_1, a_2),
(b_1, b_2))$ when $(a_i, b_i) \in R_i$ – the unit $I$ is a fixed
singleton set, say $\{*\}$. Additionally, $\Rel$ is compact
closed: each set $A$ has a dual $A^*$ defined simply as $A$ itself,
and there are relations $\eta_A \in \Rel(I, A\times A)$ and $\epsilon_A
\in \Rel(A\times A, I)$, both diagonal relations, satisfying coherence
conditions [30].
In particular, $\Rel$ is $\star$-autonomous and as such a model
of multiplicative linear logic, and the linear $\lambda$-calculus: the
linear arrow type is interpreted as $\intr{A \lin B} =
\intr{A} \times \intr{B}$. Finally, $\Rel$ has finite products, with the
binary product of sets $A$ and $B$ given by the disjoint union
$A + B = \{1\} \times A \uplus \{2\} \times B$.

§.§.§ The exponential modality
The exponential modality of
$\Rel$ is based on finite multisets. If $A$ is a set, we write
$\Mf(A)$ for the set of finite multisets on $A$. To denote specific
multisets we use a list-like notation, as in e.g. $[0, 1, 1] \in
\Mf(\mathbb{N})$ – we write $[] \in \Mf(A)$ for the empty multiset.

For $A$ a set, its bang $\oc A$ is simply the set $\Mf(A)$.
This extends to a comonad on $\Rel$, satisfying the required
conditions to form a so-called Seely category – in particular,
there is

\[
\Mf(A + B) \iso \Mf(A) \times \Mf(B)
\]

a bijection providing the Seely isomorphism. Altogether, this
makes $\Rel$ a model of intuitionistic linear logic; and this makes the
Kleisli category $\Rel_{\oc}$ cartesian closed so that we may interpret
(among others) the simply-typed $\lambda$-calculus.

Considering the term $\vdash M : \tbool \to \tbool$ of $\PCF$

\[
\begin{array}{l}
\vdash \lambda
\hspace{50pt}\mathtt{else}\,\mathtt{if}\,x\,\mathtt{then}\,\tfalse\,\mathtt{else}\,\ttrue : \tbool
\to \tbool\,,
\end{array}
\]

we have $\intr{M} = \{([\ttrue, \ttrue], \ttrue), ([\ttrue,
\tfalse], \tfalse), ([\tfalse, \tfalse], \ttrue)\}$.

Here we can observe that the model is quantitative, in that it
records how many resources each execution consumes: one may observe
output $\ttrue$ either with two evaluations of $x$ to $\ttrue$, or with
two evaluations of $x$ to $\tfalse$. One may observe output $\tfalse$
with two evaluations of $x$, one to $\ttrue$ and one to $\tfalse$.
Recall that in $[\ttrue, \tfalse] = [\tfalse, \ttrue]$, the order is irrelevant.

The relational model also supports the interpretation of
non-determinism: if $\vdash \choice : \tbool$ is a new
primitive evaluating non-deterministically to $\ttrue$ or $\tfalse$,
then we may simply set

\[
\intr{\choice} = \{\ttrue, \tfalse\}\,.
\]

§.§.§ Extensions of the relational model
The relational
model is extremely flexible, and can be extended in multiple different
ways. In one direction one may add to the objects a coherence
relation and restrict to compatible morphisms – we obtain in this way
(multiset-based) coherence semantics.

Another extension is the weighted relational model
[31, 5] where
a term $\vdash M : A$, instead of denoting a subset of $\intr{A}$ –
i.e. a function $\intr{M} : \intr{A} \to \{0, 1\}$ – denotes a

\[
\intr{M} : \intr{A} \to \R
\]

assigning to each point of the web $a \in \intr{A}$ a weight
$\intr{M}_a \in \R$. The weight may be used to record additional
information about executions. One may record the number of distinct
non-deterministic branches leading to a certain result: for instance,
if $\R = \mathbb{N} \cup \{+\infty\}$, then
= 2$.
With $\R = \rp = \mathbb{R}_+ \cup \{+\infty\}$, we may track the
probability with which a certain result occurs, obtaining a
model fully abstract for probabilistic $\PCF$
[7]. The paper
[5] contains other examples:
resource consumption, must convergence, etc.

It is natural to go one step further and make the relational model
“proof-relevant”. This means not merely recording a weight or
counting non-deterministic branches, but keeping track of a set
$\intr{M}_a \in \Set$
of witnesses
of the execution of $M$ to $a$, for each $\vdash M : A$ and $a \in
\intr{A}$. There are well-documented ways to do that which we shall
review later on, but for now let us attempt this naively.

§.§ The Bicategory of Spans

A first idea is to simply replace relations with spans.

§.§.§ Spans

Recall that if $\C$ is a category with pullbacks, then we form
$\Span(\C)$ has having as objects those of $\C$, and as morphisms from
$A$ to $B$ triples $(S, \display^S_A, \display^S_B)$ forming a diagram

\[
\quad \stackrel{\display^S_A}{\leftarrow} \quad
\quad \stackrel{\display^S_B}{\rightarrow} \quad
\]

where intuitively $S$ is a set of internal witnesses, projected
to $A$ and $B$ via the maps $\display^S_A$ and $\display^S_B$. For $\C
= \Set$ one obtains a relation by collecting the pairs
$(\display^S_A(s), \display^S_B(s))$ for $s \in S$, but we have more:
for each pair $(a, b) \in A \times B$ we have

\[
\wit^S(a, b) = \{s \in S \mid \display^S_A(s) = a~\&~\display^S_B(s)
= b\}\,,
\]

a set of witnesses that $a$ and $b$ are related – hence this
indeed provides a notion of a proof-relevant relational model.

Writing $\mathbb{B} = \{\ttrue, \tfalse\}$ and $1 = \{*\}$, we may
represent the program $\vdash
\mathtt{if}\,\choice\,\mathtt{then}\,\ttrue\,\mathtt{else}\,\ttrue$ as

\[
\quad \stackrel{\partial_l}{\leftarrow} \quad
\{a, b\}
\quad \stackrel{\partial_r}{\rightarrow} \quad
\tbool
\]

a span, where $\partial_l(a) = \partial_l(b) = *$, $\partial_r(a) =
\partial_r(b) = \ttrue$.

Thus, the evaluation of the program to $\ttrue$ has two witnesses.

§.§.§ A bicategory

The exact identity of $S$ does not matter
– the same span above with $S' = \{a', b'\}$ should not be treated
distinctly. A morphism between spans is $f\co S \to S'$ making

\[
\begin{tikzcd}[cramped,rsbo=1.3em]
& S	\ar[dl,"\display^S_A"']
\ar[dr,"\display^S_B"]
\ar[dd,"f"]
\\
&S'	\ar[ul,"\display^{S'}_A"]
\ar[ur,"\display^{S'}_B"']
\end{tikzcd}
\]

commute; an isomorphism of span is an invertible morphism.

The identity span on $A$ is simply $A \leftarrow A \rightarrow
A$ with two identity maps.
The composition of $A \leftarrow S \rightarrow B$ and $B \leftarrow T
\rightarrow C$ is obtained by first forming the pullback

\begin{equation}
\begin{tikzcd}[cramped,csbo=large,rsbo=normal]
T \odot S
\ar[dl,"\pl"']
\ar[dr,"\pr"]
\phar[dd,"\dcorner",very near start]
\\
S	\ar[dl,"\display^S_A"']
\ar[dr,"\display^S_B"]
\ar[dl,"\display^T_B"']
\ar[dr,"\display^T_C"]
\\
\end{tikzcd}
\label{eq:pbcomp}
\end{equation}

and setting $\display^{T\odot S}_A = \display^S_A \circ \pl$ and
$\display^{T\odot S}_C = \display^T_C \circ \pr$ – for
$\Span(\Set)$, this means that $T\odot S$ has elements all pairs $(s,
t)$ such that $\display^S_B(s) = \display^T_B(t)$, projected to $A$ and
$C$ via $\display^{T\odot S}_A((s, t)) = \display^S_A(s)$ and
$\display^{T\odot S}_C((s, t)) = \display^T_C(t)$.

This composition need not be associative on the nose,
but the universal property of pullbacks entails that it is associative
up to canonical isomorphism – forming a bicategory:

If $\C$ has pullbacks, then $\Span(\C)$ defined with

\[
\begin{array}{rl}
\text{\emph{objects:}} & \text{objects of $\C$,}\\
\text{\emph{morphisms:}} & \text{spans $A \leftarrow S \rightarrow B$,}\\
\text{\emph{$2$-cells:}} & \text{morphisms of spans,}
\end{array}
\]

forms a bicategory, denoted $\Span(\C)$.

In fact, $\Span(\C)$ is a compact closed bicategory
[32], and thus a model of the linear
$\lambda$-calculus. In particular, $\Span(\Set)$ shares much structure
with $\Rel$: it has the same objects and the operation sending a span
$A \leftarrow S \rightarrow B$ to the pairs $(\display^S_A(s),
\display^S_B(s))$ for $s \in S$ is a functor, establishing
$\Span(\Set)$ as a natural candidate for a proof-relevant relational

§.§.§ The exponential

However, the exponential of $\Rel$ does
not directly transport to $\Span$. The operation $\Mf(-)$ does yield a
functor on $\Set$ obtained by setting, for $f : A \to B$,

\[
\Mf(f)([a_1, \dots, a_n]) = [f(a_1), \dots, f(a_n)]
\]

defining $\Mf(f) : \Mf(A) \to \Mf(B)$. But $\Mf(f)$ does not lift to
$\Span(\Set)$ as it does not preserve pullbacks. Indeed, the diagram
obtained by image of the composition pullback

\[
\begin{tikzcd}[cramped,rsbo=normal,csbo=5.5em]
\Mf(T\odot S)
\ar[dl,"\Mf(\pl)"']
\ar[dr,"\Mf(\pr)"]
\\
\Mf(S)
\ar[dr,"\Mf(\display^S_B)"']
\Mf(T)
\ar[dl,"\Mf(\display^T_B)"]
\\
\end{tikzcd}
\]

is no pullback: this would need a bijection of $\Mf(T\odot S)$

\[
\{(\mu, \nu) \in \Mf(S) \times \Mf(T) \mid \Mf(\display^S_B)(\mu) =
\Mf(\display^T_B)(\nu) \}\,,
\]

which fails in general. If $S = T = \tbool$ and $B = 1$, the pair of
multisets $([\ttrue, \tfalse], [\ttrue, \tfalse])$ does not uniquely
specify who is synchronized with whom: it may correspond to
both multisets $[(\ttrue, \ttrue), (\tfalse, \tfalse)]$ and $[(\ttrue,
\tfalse), (\tfalse, \ttrue)]$ in $\Mf(T\odot S)$.

This might be expected: a finite multiset only remembers the
multiplicity of elements, but does not track distinct individual
occurrences. This is in tension with the goal of a proof-relevant
relational semantics, for which specific witnesses are naturally
associated with individual resource occurrences.

§.§.§ Categorifying objects
If the exponential is to track
individual resource occurrences, that means avoiding the quotient of
finite multisets: an element of $\oc A$ may for instance be a
list, or a word $a_1 \dots a_n \in A^*$ of elements of
$A$. We must of course still account for reorderings, which turn $A^*$
into a groupoid – in fact, it is an instance of the
construction of the free symmetric monoidal category $\Sym(A)$
over a category $A$: its objects are finite words $a_1 \dots a_n$ of
objects of $A$, and a morphism from $a_1 \dots a_n$ to $a'_1 \dots
a'_n$ consists of a permutation $\pi \in \Perm{n}$, and a family $(f_i
\in A(a_i, a_{\pi(i)}))_{1\leq i \leq n}$.

Thus, objects are not mere sets but categories, which means that we move
from $\Span(\Set)$ to $\Span(\Cat)$. Indeed, $\Cat$ also has
pullbacks, and so the exact same construction as above yields a
bicategory $\Span(\Cat)$ – except that now the functor
$\Sym : \Cat \to \Cat$ preserves pullbacks and thus lifts to

\[
\Sym : \Span(\Cat) \to \Span(\Cat)\,.
\]

However, in this categorification, the Seely isomorphism $\Mf(A +
B) \iso \Mf(A) \times \Mf(B)$ is lost. Instead, we only get

\[
\Sym(A + B) \simeq \Sym(A) \times \Sym(B)
\]

an equivalence of categories. In order to lift it to spans, we
observe that given a functor $F : A \to B$ we get a span

\[
\hat{F}
\quad = \quad
\begin{tikzcd}[cramped,rsbo=normal,csbo=large]
\ar[dr,"F"]
\ar[dl,"\Id_A"']
\\
\end{tikzcd}
\quad \in \quad
\Span(\Cat)(A, B)
\]

so that lifting an equivalence $F : A \simeq B : G$ to spans requires
us to provide a family of $2$-cells, i.e. for each category $A$:

\[
\begin{tikzcd}[cramped,rsbo=normal]
\ar[dl,"\Id_A"']
\ar[dr,"GF"]
\ar[dd,dotted,"?"{description}]
\\
\\
\ar[ul,"\Id_A"]
\ar[ur,"\Id_A"']
\end{tikzcd}
\]

however whatever our choice for the mediating map is, one of the
triangles fails to commute on the nose but only up to isomorphism,
which the $2$-cells of $\Span(\Cat)$ are too
strict to accommodate. This invites weakening the $2$-cells to:

A weak morphism from $A \leftarrow S \rightarrow B$ to $A
\leftarrow S' \rightarrow B$ is a triple $(F, F^A, F^B)$ where

\[
\begin{tikzcd}[cramped,rsbo=normal]
S	\ar[dll,"\display^S_A"']
\ar[drr,"\display^S_B"]
\ar[dd,"F"{description}]
\\
F^A\!\Downarrow\hspace{-15pt} && \hspace{-15pt}\Downarrow \! F^B&B\\
\ar[ull,"\display^{S'}_A"]
\ar[urr,"\display^{S'}_B"']
\end{tikzcd}
\]

with $F^A : \display^S_A \Rightarrow \display^{S'}_A \circ F$ and $F^B :
\display^S_B \Rightarrow \display^{S'}_B \circ F$ natural isos. We call this a
strong morphism if $F^A$ and $F^B$ are identities.

Adopting weak morphisms seems to solve the problem above, but
only to run into a much more subtle one: in $\Span(\Cat)$, the
horizontal composition of $2$-cells $F : S \Rightarrow S'$ and $G : T
\Rightarrow T'$ as required by the bicategorical structure follows from
the universal property of the pullback $T' \odot S'$:

\begin{equation}
\begin{tikzcd}[cramped,rsbo={1.5em},csbo={4.5em}]
T \odot S
\ar[dl]
\ar[dr]
\phar[dd,"\dcorner",very near start]
\ar[dddd,dotted,bend left=64,"G\odot F"{description}]
\\
\ar[dl]
\ar[dd,dotted,"F"{description}]
\ar[dr]
\ar[dl]
\ar[dd,dotted,"G"{description}]
\ar[dr]
\\
\\
\ar[ul]
\ar[ur]
\ar[ul]
\ar[ur]
\\
T' \odot S'
\ar[ul]
\ar[ur]
\phar[uu,"\ucorner",very near start]
\end{tikzcd}
\label{eq:horcomp}
\end{equation}

but this universal property is powerless to compose horizontally weak
morphisms. We cannot have the cake and eat it too: if our method to
compose spans ignores the $2$-categorical nature of $\Cat$, then we
cannot hope composition to preserve an equivalence between spans that
relies on it, as required for a model of linear logic. So it seems
that this road to a proof-relevant relational model is doomed – except
that this is exactly what we shall do in this paper!

Before we delve into that, we review existing solutions.

§.§ Proof-Relevant Relational Models, and Other Related Work

As plain pullbacks are “too $1$-dimensional”, it is natural to
compose spans with a $2$-dimensional version.

§.§.§ Bipullbacks
There are multiple variants for weakened
versions of pullbacks in a $2$-category. In this paper, a central
notion will be that of a bipullback:[According to the
nlab, its proper name is a bi-iso-comma-object.]

\[
\adjustbox{scale=.8,center}{%
\begin{tikzcd}
& P	\ar[dl,swap,"\pl"]
\ar[dr,"\pr"]\\
S	\ar[dr,swap,"u"]
\phar[rr,"\xTo{\mu}"]&&
T	\ar[dl,"v"]\\
\end{tikzcd}}
\]

A bipullback

\[
\adjustbox{scale=.8,center}{%
\begin{tikzcd}
& X     \ar[dl,swap,"l'"]
\ar[dr,"r'"]\\
S       \ar[dr,swap,"u"]
\phar[rr,"\xTo{\nu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}}
\]

Alternative square

In a $2$-category $\C$, a bipullback of the cospan $S \xto{u} B
\xot{v} T$ is a square commuting up to an invertible $2$-cell as in
<Ref>, such that for any square as in <Ref>:

*  There is a morphism $h : X \to P$ and
$2$-cells $\alpha$ and $\beta$ s.t.:

\[
\adjustbox{scale=.8}{%
\begin{tikzcd}
& X	\ar[ddl,bend right=30, "l'"',myname=lp]
\ar[ddr,bend left=30, "r'",myname=rp]
\ar[d,"h"{description}]\\
& P     \ar[dl,"\pl"']
\ar[dr,"\pr"]
\phar[to=rp,"\xTo{\beta}"]
\phar[from=lp,"\xTo{\alpha}"]\\
S       \ar[dr,"u"']
\phar[rr,"\xTo{\mu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}}
\qquad=\qquad
\adjustbox{scale=.8}{%
\begin{tikzcd}
& X     \ar[ddl,bend right=30, "l'"',myname=lp]
\ar[ddr,bend left=30, "r'",myname=rp]\\\\
S       \ar[dr,"u"']
\phar[rr,"\xTo{\nu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}}
\]

*  $h, \alpha, \beta$ are unique up to
unique $2$-cell – see <Ref>.

The important observation is that this alternative universal property is
sufficient to extend the definition of the horizontal composition in
(<ref>) to weak morphisms – with the proviso that
this defines horizontal composition only up to iso; as (b) does
not guarantee uniqueness of $h$ on the nose.

§.§.§ Hoffnung's monoidal tricategory
[33] constructs a categorification of $\Span(\Cat)$
following this idea. He exploits that $\Cat$ actually has
pseudo-pullbacks[According to the nlab, its proper name
is an iso-comma-object.], which are a special case of the
definition above where $\alpha$ and $\beta$ are required to be
identities and $h$ is unique on the nose – making horizontal
composition of weak morphisms of spans a well-defined function once a
choice of pseudo-pullbacks is fixed.

Concretely, a pseudo-pullback of a cospan $S \xto{u} B \xot{v} T$ may be
constructed as a category with objects triples $(s, \theta, t)$ where $\theta
\in B(u(s), v(t))$. So for instance, if $S = T = \Sym(\tbool)$ and $B =
\Sym(1)$, the pseudo-pullback would have two objects synchronizing $[\ttrue,
\tfalse] \in S$ and $[\ttrue, \tfalse] \in T$: $([\ttrue, \tfalse], \id,
[\ttrue, \tfalse])$ and $([\ttrue, \tfalse, \swap, [\ttrue, \tfalse])$. The
issue of <Ref> is avoided by adding new witnesses
carrying all possible symmetries. This is a fundamental phenomenon in models of
linear logic, which we refer to as saturation.

Because saturation inflates the number of witnesses at each
composition, spans composed by pseudo-pullbacks no longer form a
bicategory. In particular, the post-composition of a span $A \ot S \to
B$ with the identity span $B \ot B \to B$ yields an inflated $S'$ much
bigger than $S$. So neutrality of identity no longer holds up to
isomorphism, but only up to equivalence factoring in maps
between maps of spans. Accordingly, Hoffnung actually constructs a
monoidal tricategory of categorical spans with weak morphisms,
i.e. a one-object tetracategory!

§.§.§ Melliès' template games
Recently, Melliès introduced
template games [34], in an
attempt to unify various games models. This is essentially a
model of categorical spans where categories are regarded as games and
structured by a projection to a category called the  template,
capturing the mechanisms of synchronization and scheduling between
Though [34] was developped in a purely
linear setting with spans related by strong morphisms, Melliès
proposed a non-linear extension, forming a model of differential linear
logic [23].

Melliès' contribution puts into play notions from homotopy
theory: he starts not with $\Cat$, but from any $2$-category $\S$
equipped with a Quillen model structure (with additional conditions).
Spans are composed by mere pullbacks, but a span

\[
A \xot{u} S \xto{v} B
\]

must satisfy a fibration property to the effect that
symmetries in $A$ and $B$ can be lifted uniquely in $S$ – in
our terminology, $S$ is saturated. Saturation ensures that
pullbacks between those spans are actually homotopy pullbacks,
and thus that they may be used for the horizontal composition of weak
morphisms. The higher dimensional structure seen in Hoffnung
[33] is then managed by the homotopy-theoretic
operation of localization, formally inverting weak equivalences.
This yields an actual bicategory of objects of
$\S$ related by homotopy spans.

This elegant construction gives a model of differential linear logic,
showing that the symmetries implicit in linear logic may be naturally
managed via the tools of homotopy theory.

§.§.§ Generalized Species of Structures

Last but not least, the most well-studied proof-relevant extension
of $\Rel$ is definitely Fiore, Gambino, Hyland and Winskel's cartesian
closed bicategory of generalized species of structure
[20]. Relations from $A$ to $B$ are
replaced with
distributors or profunctors:

\[
F : A^{\op} \times B \to \Set
\]

for $A$ and $B$ categories. This forms a
(compact closed) bicategory $\Dist$ of (small) categories, distributors and
natural transformations between them. The free symmetric monoidal
construction $\Sym(-)$ yields a pseudocomonad on $\Dist$, whose Kleisli
bicategory $\Esp$ is cartesian closed.

As for the span-based approaches above, the way in which $\Dist$ and
$\Esp$ handle symmetries is saturated. This may first be seen in the
identity distributor which is defined to be

\[
A[-, -] : A^{\op} \times A \to \Set
\]

the Yoneda embedding,
which associates as witnesses over a pair $(a, a)$ the homset
$A[a, a]$, including all symmetries on $a$.

Composition of distributors is via the coend formula

\[
G \odot F = \int^{b \in B} F(-, b) \times G(b, -)
\]

which sets witnesses in $(G\odot F)(a, c)$ to be pairs $(s, t) \in F(a,
b) \times G(b, C)$ quotiented by a relation identifying the action of a
morphism in $B$ on $s$ or on $t$.

Accordingly, when computing the interpretation of a program $\vdash M :
A$ in $\Esp$, for every $a \in \intr{A}$ we get $\intr{M}(a)$ a set of
witnesses carrying around explicit symmetries, quotiented by an
equivalence relation letting symmetries flow around – this is
described syntactically elegantly by Olimpieri
[28]. The treatment of symmetry in
$\Esp$ is, again, saturated.

§.§.§ Game semantics
To our knowledge, this saturation
phenomenon in models of linear logic first appears in Baillot, Danos,
Ehrhard and Regnier's (BDER) version [35]
of Abramsky-Jagadeesan-Malacaria (AJM) games

In AJM games, the moves of a game $\oc A$ are defined as pairs
$(i, a)$ of $i \in \mathbb{N}$ a copy index, and $a \in A$ a
move in $A$ – a fundamental difficulty in setting up the games model,
is that of uniformity: ensuring that the behaviour of
strategies does not depend on the specific choice of copy indices
(which is the game semantics analogue of composition preserving weak
morphisms). In BDER, uniformity is guaranteed by requiring strategies
to be saturated: they are morally wrapped by copycat processes
exchanging non-deterministically all copy indices. This “noise”
prevents strategies from seeing specific copy indices, let alone
depending on them – this is analogous to the saturation phenomenon above.

But in AJM games there is another choice: in the original AJM setting
[12], strategies carry a
deterministic choice of copy indices. Instead of saturation, uniformity
is guaranteed by requiring that strategies satisfy a bisimulation-like
property, which ensures that whenever Opponent swaps their copy
indices, Player can swap theirs accordingly, leaving the behaviour
“up to copy indices” invariant. In contrast to the “saturated”
approach to uniformity, we refer to this as the “thin” approach.
Similar ideas are at play in other
game models based on copy indices: in Melliès' orbital games
[15], and more recently in thin
concurrent games[The first version of concurrent
games with symmetry was saturated [36].]

Thin concurrent games are a particularly striking related work, because
just as $\Esp$, they also form a cartesian closed bicategory as
proved by Paquet [22], and also generalize the
relational model [37]. In thin
concurrent games, strategies are composed by pullback. But it is a
theorem that this pullback is also a bipullback, which can be used to
compose horizontally weak morphisms even though strategies are not
saturated. But this bipullback property follows from a subtle
interactive reindexing mechanism between strategies, relying crucially
on the fact that we have access to time – it seems hard to replicate
it purely statically as in a relational model.

§ THE BICATEGORY OF THIN SPANS

This long discussion lets us state the main question in this
paper: can we construct a thin version of
categorical spans?

§.§ Pullbacks and Bipullbacks in Groupoids

For simplicity, we focus on spans of groupoids
rather than categories, which are sufficient for the
interpretation of types – we write $\Gpd$ for the small $2$-category
of groupoids.
So we aim to construct a bicategory whose objects are small groupoids,
whose morphisms are spans $A \ot S \to B$ with identity the identity
span $A \ot A \to A$, whose composition is plain
pullback and yet, whose $2$-cells are weak morphisms.

§.§.§ Notations and terminology
A span $A \ot S \to B$ may be
presented as a functor $S \to A \times B$, so it is convenient not to focus on
spans, but on functors $S \to A$ over a groupoid $A$. We refer to those with
terminology inspired from game semantics. A prestrategy on groupoid $A$
is a pair $(S, \display^F)$ where $\display^F : S \to A$ is called the
display map. We often refer to the prestrategy only with $S$, and write
$\PreStrat(A)$ for the set of prestrategies on $A$. A prestrategy from
$A$ to $B$ is a prestrategy on $A \times B$ – then, we write $\display^F_A :
S \to A$ and $\display^F_B : S \to B$ for the two display maps. If $S$ is a
prestrategy from $A$ to $B$ and $T$ a prestrategy from $B$ to $C$, we write $T
\odot S$ for the prestrategy from $A$ to $C$ obtained as in
<Ref>. We often refer to morphisms in groupoids as
symmetries and write e.g. $\varphi : s \sym_S s'$ instead of
$\varphi \in S(s, s')$.

We write $1$ for the groupoid with one object $*$, and only the
identity morphism; and $o$ for the groupoid with one object $\bullet$
and only the identity morphism. If $A, B$ are groupoids, then we
use $A \vdash B$ and $A \lin B$ as synonyms for $A \times B$,
with objects respectively denoted by $a \vdash b$ and
$a \lin b$ – likewise, their morphisms have form $\theta_A \vdash
\theta_B \in (A \lin B)(a \lin b, a' \lin b')$ for $\theta_A \in A(a,
a')$ and $\theta_B \in B(b, b')$ and likewise for $\theta_A \lin
\theta_B$.  We find these purely notational distinctions useful to read
examples, since they coincide with familiar type constructors.

§.§.§ Indexed families
As explained earlier, types of
$\lambda$-calculi may be interpreted as groupoids – but in a linear
language, these groupoids remain discrete: only the exponential
introduces non-trivial morphisms. As those symmetries play a
crucial role, we introduce early our version of the
exponential construction.
If $X$ is a set, then we write $\Fam(X)$ the set of families indexed by
finite sets of natural numbers, i.e. of $(x_i)_{i\in I}$
where $I \subseteq_f \N$ and for all $i \in I$, $x_i \in X$.

Consider $A$ a (small) groupoid.
The (small) groupoid $\BFam(A)$ has:
objects, the set $\Fam(A)$; morphisms from $(a_i)_{i\in
I}$ to $(b_j)_{j\in J}$, pairs $(\pi, (f_i)_{i\in I})$ of a bijection
$\pi : I \bij J$ and for each $i \in I$, $f_i \in A(a_i, b_{\pi(i)})$.

This yields a functor $\BFam : \Gpd \to \Gpd$ in the obvious way.
For $(A_i)_{i\in I} \in \Fam(A)$, we call elements of $I$
copy indices. A family $(a_i)_{i\in I} \in
\Fam(A)$ is more “intensional” than $A^*$ (which is more
intensional than $\Mf(A)$): it gives a presentation of a multiset in
$\Mf(A)$ not only providing a sequence, but assigning to each element a
distinct “address”.

Just as multisets are connected to non-idempotent intersection types,
families are connected with Vial's sequence types
[38] – thus we often write families using Vial's
notation, e.g.

\[
[2 \cdot a_2, 4 \cdot a_4, 12\cdot a_{12}] \in \Fam(A)
\]

for $(a_i)_{i\in \{2, 4, 12\}}$ – in the particular case where $A =
o$, we only write $[i_1, \dots, i_n]$ for $[i_1 \cdot \bullet, \dots,
i_n \cdot \bullet]$.

For any groupoid $A$, $\BFam(A)$ and $\Sym(A)$ are equivalent. However,
using $\BFam(A)$ is crucial in our model construction: it allows the
interpretation of programs to use copy indices as identifiers
for resource accesses, that are independent of other concurrent
resource accesses.
We give a few examples:

For a groupoid $A$, the dereliction span $\bder_A$ is

\[
\BFam(A) \xot{\der_A} A \xto{\id_A} A
\]

where $\der_A : A \to \BFam(A)$ sends $a$ to $[0\cdot a]$.

In models of linear logic, the role of dereliction is to extract a
single instance of a replicable resource. In our model – as in
AJM games [12] and thin concurrent
games [21] – dereliction does so by
picking a copy index (here $0$), chosen in advance once and for all.
The specific choice is irrelevant; in fact for any $n$ the span using
$n$ instead of $0$ will be turn out to be isomorphic to $\bder_A$. But,
the span must comprise a choice.

The interpretation of the term $M$ of <Ref> in thin spans
shall have head groupoid that with four objects

\[
\begin{array}{ll}
\,[0 \cdot \ttrue, 1 \cdot \ttrue] \lin \ttrue\,,
\qquad
&[0 \cdot \tfalse, 1\cdot \tfalse] \lin \ttrue\,,\\
\,[0 \cdot \ttrue, 1 \cdot \tfalse] \lin \tfalse\,,
\qquad
&[0 \cdot \tfalse, 1 \cdot \ttrue] \lin \ttrue\,,
\end{array}
\]

morphisms reduced to identities, and display map the identity.

The use of
specific copy indices allows one to observe which occurrence of $x$
evaluates to $\ttrue$ or $\tfalse$, hence associating distinct points
to the two evaluations leading to $\tfalse$.

§.§.§ Bipullbacks of groupoids
If composition-by-pullback is
to allow us to compose horizontally weak morphisms, we must ensure that every
composition pullback is also a bipullback.

It is useful to understand a bit better the shape of bipullbacks in $\Gpd$. A
first useful fact is that condition <Ref> of
<Ref> (uniqueness up to iso) automatically holds in
the case of $\Gpd$; furthermore, we can characterise those pullbacks that are
also bipullbacks (see <Ref>):

A pullback square in $\Gpd$, of the form

\[
\begin{tikzcd}[cramped,rsbo=2em,csbo=2.5em]
\ar[ld,"\pl"']
\ar[rd,"\pr"]
\phar[dd,"\dcorner",very near start]
\\
\ar[rd,"f"']
\ar[ld,"g"]
\\
\end{tikzcd}
\]

is a bipullback if and only if it satisfies the following property: for
all $s \in S$, $t \in T$ and $\theta \in B(fs, gt)$, there is $\varphi
\in S(s, s')$ and $\psi \in T(t', t)$ such that $f s' = g t'$ and
$\theta = f\psi \circ g\varphi$.

Let us comment on this. We regard triples of the form

\[
s \in S\,,
\qquad
\theta \in B(f s, g t)\,,
\qquad
t \in T
\]

as pairs of states $(s, t)$ that match up to symmetry – we call
this a reindexing problem. The lemma above says that given a
reindexing problem, we can always find $s'$ symmetric to $s$ and $t'$
symmetric to $t$ matching on the nose, in a way compatible with

– called a solution to the reindexing problem. Thus, the
lemma above may be reformulated to say that a pullback is a bipullback
iff all its reindexing problems have a solution.

We show a concrete example of this reindexing process:

Take $B = \BFam(o) \lin \BFam(o)$, with objects

\[
[i_1,  \dots, i_n] \lin [j_1, \dots, j_k]\,.
\]

Take $S$ the sub-groupoid of $B$ with objects $[i_1, \dots,
i_n] \lin [i_1, \dots, i_n]$ and morphisms all $\theta \lin \theta$ for
$\theta$ in $\BFam(o)$; and $T$ the full sub-groupoid of $B$
with objects $[j_1, \dots, j_n] \lin [0]$.

The pullback of $S \to B \ot T$ is a bipullback.
For instance,

\[
\theta
\in
B([2] \lin [2],
[1] \lin [0])
\]

is a reindexing problem that may be solved by first applying

\[
\varphi \in S([2] \lin [2], [0] \lin [0])
\]

in $S$. We are reduced to finding morphisms in $S$ and $T$

\[
\theta' \in
B([0] \lin [0],
[1] \lin [0])
\]

Now, applying $\psi \in T([0] \lin [0], [1] \lin [0])$ in $T$, we have

\[
\varphi \in S([2] \lin [2], [0] \lin [0])\,,
\quad
\psi \in T([0] \lin [0], [1] \lin [0])
\]

a solution to the reindexing problem, as in <Ref>.

That the pullback of two prestrategies forms a bipullback is not a
property of either: in this example neither strategy is a fibration as
in [23], and solving the reindexing problem
requires reindexing in both groupoids. So it is a
property emerging from the harmonious interaction between two
prestrategies. In an appropriate game semantics setting
[21], one can prove that
under reasonable assumptions, such interactive reindexing always
succeeds. However, this is a gradual process progressing over
time – which we do not have access to here.

§.§ Orthogonality and Uniform Groupoids

§.§.§ Definition

In the literature on models of linear
logic, there is a technique for choreographing models where one only
composes pairs of morphisms satisfying a given interactive property:
The first step is to specify the desired interactive property via an
orthogonality relation:

Take $(S, \display^S)$ and $(T, \display^T)$ prestrategies on

We say they are uniformly orthogonal, written $S \perp T$, iff
the pullback of the cospan $S \to B \ot T$ is also a bipullback.

If $\bS\subseteq \PreStrat(B)$, then its uniform orthogonal is
set to:

\[
\bS^\perp = \{T \in \PreStrat(B) \mid \forall S \in \bS,~ S \perp T\}\zbox.
\]

As usual with orthogonality, this automatically entails a
number of properties: for all $\bS \subseteq \PreStrat(B)$, we have
$\bS \subseteq \bS^{\perp \perp}$, and $\bS^\perp = \bS^{\perp \perp
\perp}$. We are particularly interested in sets of the form
$\bS^\perp$, which are invariant under biorthogonal:

A uniform groupoid is a pair $(A, \U_A)$ where $A$ is a
groupoid and $\U_A \subseteq \PreStrat(A)$ is s.t.
$\U_A^{\perp\perp} = \U_A$.

We often refer to a uniform groupoid $(A, \U_A)$ just with $A$ when it
is clear from the context that it is a uniform groupoid.

§.§.§ Constructions
The uniform groupoid $1$ is the terminal
groupoid equipped with $\U_1 = \PreStrat(1)$. If $A$ and $B$ are
uniform groupoids, their tensor $A \tensor B$ is the groupoid
$A \times B$ equipped with
the set $\U_{A \tensor B} = (\U_A \tensor \U_B)^{\perp \perp}$, writing

\[
\U_A \tensor \U_B = \{(S \times T, \display^S \times \display^T) \mid S \in \U_A,~T \in \U_B\}
\]

with $\display^S \times \display^T : S \times T \to A \times B$. The
dual $A^\perp$ of $A$ is $(A, \U_{A^\perp})$ with
$\U_{A^\perp} = \U_A^\perp$. The par of $A$ and $B$

\[
\U_{A \parr B} = (\U_A^\perp \tensor \U_B^\perp)^\perp
\]

yielding the De Morgan duality $(A \tensor B)^\perp = A^\perp \parr
From this we derive the linear arrow $A \lin B = A^\perp \parr

A uniform prestrategy on uniform groupoid $A$ is simply any $S
\in \U_A$. If $A, B$ are uniform groupoids, then a uniform
prestrategy from $A$ to $B$ is a uniform prestrategy on $A \lin

§.§.§ Uniform composition
We claim that whenever composing $S
\in \U_{A\lin B}$ with $T \in \U_{B \lin C}$, we have the orthogonality

\[
(S, \display^S_B) \perp (T, \display^T_B)
\]

so that the composition pullback is a bipullback.

If $S$ is a prestrategy on $A$ and $T$ is a prestrategy from $A$ to
$B$, we write $T@S$ from the prestrategy on $B$ obtained by

\[
\begin{tikzcd}[cramped,rsbo=2em,csbo=3em]
T\odot S
\phar[dd,"\dcorner",very near start]
\ar[dl]
\ar[dr]
\\
\ar[dr]
\ar[dl]
\ar[dr]
\\
\end{tikzcd}
\]

called the application of $T$ to $S$. This lets us state:

Consider $(A, \U_A)$ and $(B, \U_B)$ uniform groupoids, and $T$ a
prestrategy from $A$ to $B$; consider furthermore a class $\SU \subseteq
\U_A$ s.t. $(A, \id_A) \in \SU$ and $\U_A = \SU^{\perp \perp}$.

Then $T \in \U_{A \lin B}$ iff
the following two conditions hold:

*  for all $S \in \SU$, $T@S \in \U_B$,

*  $(T, \display^T_A) \in \U_A^\perp$.

Unfolding the definitions, one encounters a few diagram chasing lemmas on
pullbacks that are also bipullbacks – themselves proved via
<Ref>. See <Ref>.

The apparent asymmetry is intriguing: by definition $A^\perp \parr B = A^\perp
\parr B^{\perp \perp}$, so that $T \in \U_{A\lin B}$ iff the span $B \ot T \to
A$ denoted by $T^\star$ obtained by reversing the two legs, is in $\U_{B^\perp
\lin A^\perp}$. A similar phenomenon appears in the orthogonality used by
Ehrhard for his extensional collapse [39].

Now, observe that $(A, \id_A) \in \U_A$ always – not the identity span, but the
identity functor regarded as a prestrategy on $A$. Indeed, if $S \in
\U_A^\perp$, then the pullback of $A \to A \ot S$ is clearly a bipullback, so
$(A, \id_A) \in \U_A^{\perp\perp} = \U_A$. But now this lets us instantiate
<Ref> with $\SU = \U_A$. Then given $S \in \U_{A\lin B}$, the
application $S@(A, \id_A)$ is (up to iso) the right leg $(S, \display^S_B)$,
which must by (1) be in $\U_B$. Likewise, if $T \in \U_{B \lin C}$, the
left leg $(T, \display^T_B)$ is in $\U_B^\perp$. Hence,

\[
(S, \display^S_B) \quad \perp \quad (T, \display^T_B)
\]

and thus the composition pullback of $S$ and $T$ is a bipullback.

<Ref> has more consequences, all obtained in the particular case
where $\SU = \U_A$: we saw above that $(A, \id_A) \in \U_A$, but the same
argument goes to show $(A, \id_A) \in \U_A^\perp$ as well – so the identity
span satisfies condition (2). Since it also satisfies (1), we have
$(A \ot A \to A) \in \U_{A\lin A}$ as expected. Likewise, if $A \ot S \to B$ and
$B \ot T \to C$ are uniform prestrategies, then it follows fairly easily that
the composition $A \ot T\odot S \to C$ is indeed in $\U_{A\lin C}$ (see

§.§.§ Horizontal composition of $2$-cells

We have an identity uniform prestrategy in $\U_{A\lin A}$, and a
well-defined composition of $S \in \U_{A\lin B}$ and $T \in \U_{B \lin
C}$ such that the composition pullback is always a bipullback. So given
weak morphisms

\[
\begin{tikzcd}[cramped,rsbo=1.6em,csbo=2.4em]
S	\ar[dll,"\display^S_A"']
\ar[drr,"\display^S_B"]
\ar[dd,"F"{description}]
\\
F^A\!\!\Downarrow\hspace{-15pt} && \hspace{-15pt}\Downarrow \!\! F^B&B\\
\ar[ull,"\display^{S'}_A"]
\ar[urr,"\display^{S'}_B"']
\end{tikzcd}
\qquad
\begin{tikzcd}[cramped,rsbo=1.6em,csbo=2.4em]
T	\ar[dll,"\display^T_B"']
\ar[drr,"\display^T_C"]
\ar[dd,"G"{description}]
\\
G^B\!\!\Downarrow\hspace{-15pt} && \hspace{-15pt}\Downarrow \!\! G^C&C\\
\ar[ull,"\display^{T'}_B"]
\ar[urr,"\display^{T'}_C"']
\end{tikzcd}
\]

by the bipullback property of $T' \odot S'$ there are a functor $H$ and
natural isos $\alpha$ and $\beta$ such that we have the equality

\[
\adjustbox{scale=.8}{%
\begin{tikzcd}[cramped,row sep=10pt, column sep=20pt]
& T \odot S
\ar[dl]
\ar[dr]
\cphar[ddd,"=",pos=0.33]
\\
S	\ar[d]
\ar[ddr,bend left=30,myname=lp]&&
T	\ar[d]
\ar[ddl,bend right=30,myname=rp]\\
S'	\ar[dr]
\phar[to=lp,"\xTo{(F^{\!B})^{-1}\!\!}"]&&
T'	\ar[dl]
\phar[from=rp,"\xTo{G^{\!B}\!\!}"]\\
\end{tikzcd}}
\quad=\quad
\adjustbox{scale=.8}{%
\begin{tikzcd}[cramped,row sep=10pt, column sep=20pt]
& T \odot S
\ar[dl]
\ar[dr]
\ar[d,"H"]\\
S	\ar[d]
\phar[r,"\xTo{\alpha}"]&
T'\odot S'
\ar[dl]
\ar[dr]
\phar[r,"\xTo{\beta}"]
\cphar[dd,"="]
T	\ar[d]\\
S'	\ar[dr]&&
T'	\ar[dl]\\
\end{tikzcd}}
\]

altogether yielding a weak morphism as in the diagram:

\[
\adjustbox{scale=.8}{%
\begin{tikzcd}[cramped,row sep=10pt, column sep=25pt]
&S	\ar[dl,"\partial^S_A"']
\ar[dd,myname=ds,"F"]&
T\odot S\ar[l]
\ar[dd,myname=dh,"H"]
\ar[r]&
T	\ar[dd,myname=dg,"G"']
\ar[dr,"\partial^T_C"]\\
A	\phar[to=ds,"\Downarrow\!\scalebox{.8}{$F^A$}"]&
~	\phar[to=dh,"\Downarrow\!\scalebox{.8}{$\alpha$}"]&
~	\phar[to=dg,"\Downarrow\!\scalebox{.8}{$\beta^{-1}$}"]&&C
\phar[to=dg,"\Downarrow\!\scalebox{.8}{$G^C$}"]\\
&S'	\ar[ul,"\partial^{S'}_A"]&
T'\odot S'
\ar[l]
\ar[r]&
T'	\ar[ur,"\partial^{T'}_C"']
\end{tikzcd}}\,.
\]

However, $H, \alpha, \beta$ are not unique: though <Ref>
guarantees the existence of solutions to all reindexing problems, those may not
be unique.

We only know by condition (b) of <Ref> that different
choices of $H, \alpha, \beta$ yield isomorphic weak morphisms of uniform
prestrategies, by which we mean isomorphic morphisms of the $2$-category

Consider $A$ a uniform groupoid.

The $2$-category $\Unif(A)$ has: objects $\U_A$,
i.e. uniform prestrategies on $A$; morphisms from $S$ to
$T$ the weak morphisms, i.e. pairs $(F : S \to T, \phi :
\display^S \Rightarrow \display^T F)$;
$2$-cells from $(F, \phi)$ to $(G, \psi)$ the natural
transformations $\mu : F \Rightarrow G$ such that:

\[
\adjustbox{scale=.8}{
\begin{tikzcd}
S	\ar[rr,bend left=20,"G",myname=G]
\ar[dr]&&
T	\ar[dl]\\
&A	\phar[from=G,"\xTo{\psi}"]
\end{tikzcd}}
\quad = \quad
\adjustbox{scale=.8}{
\begin{tikzcd}
S	\ar[rr,bend left=20,"G",myname=G]
\ar[rr,bend right=20,"F"{description},myname=F]
\phar[from=F,to=G,"\Uparrow\!\mu"]
\ar[dr]&&
T	\ar[dl]\\
&A	\phar[from=F,"\xTo{\phi}"]
\end{tikzcd}}\,.
\]

Thus, although bipullbacks guarantee the existence of a fitting weak
morphism for horizontal composition, there is a priori no canonical
choice. One could pick a choice of horizontal composition, but there is
no reason why an arbitrary choice would satisfy the coherence
conditions for a bicategory.

§.§ Thin Spans of Groupoids

In fact, if formulated in the adequate way, the reindexing problems
that arise from the interpretation of programming languages do
have a unique solution – as in <Ref>.
But to prove that, we shall need to add more structure to uniform groupoids,
starting with polarized sub-groupoids:

§.§.§ Polarized sub-groupoids

Consider the groupoid

\[
\BFam(o) \lin \BFam(o)
\]

of <Ref>, interpreting the formula $\oc o \lin \oc o$ of
intuitionistic linear logic. Here, the two occurrences of $\oc$ are intuitively
very different: on the left-hand side, as in <Ref> the
program performs the copying – in game semantics the copy index would be
carried by a Player move. In contrast, for the right hand side exponential, the
environment does the copying – in game semantics, the copy index would
be carried by an Opponent move. This assigns a polarity to certain symmetries,
very clear in game semantics: those reindexing copy indices only for
exponentials in covariant position (resp. contravariant position) are
negative (resp. positive). We enrich the groupoids interpreting
types to keep track of these special symmetries:

A polarized groupoid is a groupoid $A$ with two
sub-groupoids $A_-$ and $A_+$, with the same objects as $A$.

It would be natural to require additional conditions for this structure (in
particular, see conditions (a) and (b) in
<Ref>). We omit them here, as they shall hold automatically
once we introduce the more complete notion of a thin groupoid.

If $\theta \in A_-(a_1, a_2)$, we write $\theta : a_1 \sym_A^- a_2$ and
likewise for positive symmetries.  Usual constructions on groupoids
extend to polarized groupoids componentwise. The dual of $(A,
A_-, A_+)$ is defined as $(A, A_+, A_-)$, exchanging the two
sub-groupoids.  Finally, we set $(\oc A)_- = \BFam(A_-)$ and $(\oc A)_+
= \BFam^{\id}(A_+)$, which has morphisms from $(a_i)_{i\in I}$ to
$(b_j)_{j\in J}$ those $(\pi, (\theta_i)_{i\in I})$ such that $I = J$
and $\pi = \id_I$ – thus we see indeed that Player cannot reindex copy
indices from the outer $\oc$ in $\oc A$, as it appears in covariant

§.§.§ Thinness
Solutions to reindexing problems may be computed
interactively as in <Ref>. Intuitively, the uniqueness of the
solution relies on the fact that at each stage, there is a unique choice of
reindexing. This is captured by the definition of thin below, imported
from thin concurrent games:

Consider $A$ a polarized groupoid, and $S$ a prestrategy on $A$.
We say that $S$ is thin iff for all $\varphi : s \sym_S s'$,
if $\display^S \varphi$ is positive then $s = s'$ and $\varphi =
\id_s$.

Intuitively, this captures that positive copy indices are
selected deterministically from negative ones – so a
non-trivial symmetry $\varphi : s \sym_S s'$ cannot display to a purely
positive symmetry on $A$. This is in contrast with the saturated case,
where spans must be able to reach all positive symmetries.

We show how thinness addresses uniqueness for the resolution of reindexing
problems. Call a solution to a reindexing problem $\varphi, \psi$ as in
<Ref> positive if writing $\display^S \varphi =
\varphi_A \vdash \varphi_B$ and $\display^T \psi = \psi_B \vdash \psi_C$, we
have $\varphi_A \vdash \psi_C$ positive.

Consider $A, B, C$ polarized uniform groupoids, $S \in \U_{A\lin B}$
and $T \in \U_{B \lin C}$ s.t. $T \odot S \in \U_{A\lin C}$ is

Then, any reindexing problem in the composition pullback of $S$ and $T$
has at most one positive solution.

Consider a reindexing problem $s \in S, t \in T, \theta :
\display^S_B s \sym_B \display^T_B t$ with solutions $\varphi_1 : s
\sym_S s'_1$ and $\psi_1 : t'_1 \sym_T t$ with $\display^S_B s'_1 =
\display^T_B t'_1$ and $\display^T_B \psi_1 \circ \display^S_B
\varphi_1 = \theta$, and $\varphi_2 : s \sym_S s'_2$ and $\psi_2 : t'_2
\sym_T t$ with $\display^S_B s'_2 = \display^T_B t'_2$ and
$\display^T_B \psi_2 \circ \display^S_B \varphi_1 = \theta$.

Then, $\display^S(\varphi_2 \circ \varphi_1^{-1}) = \display^T(\psi_2
\circ \psi_1^{-1})$, so that we have

\[
\Omega = (\varphi_2 \circ \varphi_1^{-1}, \psi_2 \circ \psi_1^{-1})
: (s'_1, t'_1) \sym_{T \odot S} (s'_2, t'_2)\,,
\]

whose display to $A \vdash C$ is positive since $\varphi_1, \psi_1$ and
$\varphi_2, \psi_2$ are positive solutions. Hence, by thin,
$\Omega$ is an identity map which entails $\varphi_1 = \varphi_2$ and
$\psi_1 = \psi_2$ as required.

Thus, thinness allows us to find canonical solutions to reindexing
problems by insisting on finding positive solutions.

However, this relies on thinness not of $S$ and $T$, but of $T \odot
S$. Again in thin concurrent games, this follows by induction on
the causal structure. In the absence of a handle on
causality, we must as for uniformity treat the fact that $T
\odot S$ is thin as an interactive property, again handled by

§.§ Thin Spans

§.§.§ The thin orthogonality
We observe that for $A$ a
polarized groupoid, a prestrategy $S$ on $A$ is thin iff
the pullback

\begin{equation}
\begin{tikzcd}[cramped,rsbo=1.5em,csbo=2.8em]
\phar[dd,"\dcorner",very near start]
\ar[dl]
\ar[dr]
\\
\ar[dr]
\ar[dl,"\id^+_A"]
\\
\end{tikzcd}
\label{eq:pbplus}
\end{equation}

is discrete, i.e. all the morphisms in $P$ are
identities. We shall base our orthogonality on this observation, and

For $A$ a polarized uniform groupoid, $S \in \U_A$, and $T \in
\U_A^\perp$, we say $S$ and $T$ are thinly orthogonal, written

\[
S \pperp T
\]

iff the pullback $T \odot S$ is discrete.

Note that this is already assuming that $S$ and $T$ are uniformly
orthogonal. If $\bS \subseteq \U_A$, then its thin orthogonal

\[
\bS^{\pperp} = \{T \in \U_A^{\perp} \mid \forall S \in \bS,~S \pperp T\}\,,
\]

and as before we have $\bS \subseteq \bS^{\pperp \pperp}$ (note that
this typechecks only because $\U_A^{\perp \perp} = \U_A$) and
$\bS^{\pperp} = \bS^{\pperp \pperp \pperp}$ for all $\bS \subseteq \U_A$.

§.§.§ Thin groupoids

As before, we are interested in sets of uniform prestrategies
closed under bi-thin-orthogonal:

A thin groupoid is a polarized uniform groupoid with
a set $\T_A \subseteq \U_A$ of strategies s.t. $\T_A^{\pperp \pperp} =
\T_A$, and such that $(A_-, \id_A) \in \T_A$ and $(A_+, \id_A) \in
\T_A^{\pperp}$.

If $S \in \T_A$ then $S$ is automatically thin in the sense of <Ref>:
as $(A_+, \id_A) \in \T_A^{\pperp}$ the pullback (<ref>) is discrete.

This also entails properties of the polarized symmetries:

Consider $A$ a thin groupoid. Then we have:

if $\theta : a \sym^-_A a'$ and $\theta : a \sym_A^+ a'$, then $a = a'$
and $\theta = \id_a$.

if $\theta : a \sym_A a'$, then there are unique $a''$ along with $\theta_- :
a \sym_A^- a''$ and $\theta_+ : a'' \sym_A^+ a'$ such that $\theta =
\theta_+ \circ \theta_-$.
lemme utilisé quelque part ?

For (a), this follows from $A_- \pperp A_+$, as then the
pullback of the cospan $A_- \hookrightarrow A \hookleftarrow A_+$ is

For (b), $A_- \in \T_A \subseteq \U_A$ and $A_+ \in
\T_A^{\pperp} \subseteq \U_A^{\perp}$, we also have $A_- \perp A_+$.
Hence, the pullback of the cospan $A_- \hookrightarrow A \hookleftarrow
A_+$ is a bipullback. But then any $\theta : a \sym_A a'$ forms a
reindexing problem, whose solution is exactly the seeked reindexing.
Uniqueness follows immediately from (a).

Thus, we get from the definition of thin groupoids some of the expected
properties of the polarized sub-groupoids: if a symmetry is both
positive and negative then it must be an identity, and any symmetry can
be obtained by first “reindexing Opponent moves”, then ”reindexing
Player moves”.

§.§.§ Further structure

Constructions on uniform groupoids extend to thin groupoids in the
expected way. The thin groupoid $1$ has $\T_1 =
\PreStrat(1)$. If $A$ and $B$ are thin groupoids, their tensor
is the uniform groupoid $A \tensor B$ extended with $\T_{A\tensor B} =
(\T_A \tensor \T_B)^{\pperp \pperp}$. The dual of $A$ has
$\T_{A^\perp} = \T_A^{\pperp}$. The par of $A$ and $B$ has
$\T_{A\parr B} = (\T_A^{\pperp} \tensor \T_B^{\pperp})^{\pperp}$, and
the linear arrow is $A \lin B = A^\perp \parr B$.

To establish the compositional properties of strategies, we rely on the
following analogue of <Ref>:

Consider $T \in \U_{A\lin B}$ for $A, B$ thin groupoids, along with a
class $\SU \subseteq \T_{A}$ such that $\SU^{\pperp \pperp} = \T_A$.

Then, $T \in \T_{A\lin B}$ iff $T@S \in \T_B$ for all $S \in \SU$.

This follows from diagram chasing lemmas on situations where the pullbacks are
discrete, see <Ref>. Interestingly, this is also
equivalent to $T^\star @S \in \T_A^{\pperp}$ for all $S \in \T_B^{\pperp}$.

It is a direct consequence of <Ref> that the identity span
on $A$ is in $\T_{A\lin A}$ for any thin groupoid $A$, and that if $S \in
\T_{A\lin B}$ and $T \in \T_{B \lin C}$ then $T \odot S \in \T_{A\lin C}$.
Together with <Ref>, we have thus identified a
compositional situation where the composition pullback of spans is a bipullback,
and where all arising reindexing problems have a unique solution if one
insists on this solution being positive.

§.§.§ Positive weak morphisms
Insisting on positive
solutions amounts to relating strategies not via arbitrary weak
morphisms, but with positive weak morphisms:

Consider $A$ a thin groupoid, $S, T \in \T_A$, and $(F, \phi)$ a weak morphism
from $S$ to $T$, i.e. $F : S \to T$ and $\phi : \display^S
\Rightarrow \display^T \circ F$.
Then, $(F, \phi)$ is positive if $\phi$ is positive, that
is, if $\forall s \in   S$, $\phi_s : \display^S s \sym_A^+ \display^T
F(s)$ is a positive symmetry.

Intuitively, comparing strategies with positive morphisms amounts to
relating them only via maps that do not reindex Opponent moves. This
has the effect of making everything stricter, and cutting the higher
dimension. More precisely:

Let $A$ be a thin groupoid. Consider $\PreThin(A)$ the sub-$2$-category of
$\Unif(A)$ with objects $\T_A$, and $\Thin(A)$
where additionally morphisms are positive.

Then, $\Thin(A)$ is locally discrete, i.e. all $2$-cells are
identities. Moreover, $\PreThin(A)$ and $\Thin(A)$ are biequivalent.

The first is a direct consequence of thinness: if $\mu : (F,
\phi) \Rightarrow (G, \psi) : S \to T$ for $\phi$ and $\psi$ positive,
then by definition of $2$-cells of $\Unif(A)$, for all $s \in S$,
$\mu_s \in T(Fs, Gs)$ is such that $\psi_s = \display^T \mu_s \circ
\phi_s$, i.e. $\display^T \mu_s = \psi_s \circ \phi_s^{-1}$
positive. Thus, $\mu_s$ is an identity morphism by thinness.

For the biequivalence, the crux is that if $(F, \phi) : S
\to T$ is a weak morphism, then there is a unique $(F_+, \phi_+) : S
\to T$ positive isomorphic to $(F, \phi)$, and a unique
$2$-cell $\mu$ between them. Uniqueness follows from thinness. For
existence, note that if $s \in S$ and $\theta : \display^S s \sym_A a$,
then there exist unique $\varphi : s \sym_S s'$ and $\theta_+ :
\display^S s \sym_A^+ a$ such that $\theta = \theta_+ \circ \display^S
\varphi$ – this exploits thinness, and the reindexing problem from the
fact that the pullback of the cospan $S \hookrightarrow A
\hookleftarrow A_+$ is a bipullback. We obtain $(F_+, \phi_+)$ by
applying this lemma pointwise.

This proposition illustrates the situation well: thanks to the thin
biorthogonality, the $2$-category $\PreThin(A)$ is represented up to
biequivalence as a mere category $\Thin(A)$. The higher dimensional
structure simply vanishes.

§.§.§ The bicategory $\Thin$

With this in place, we may finally define the components of our bicategory
$\Thin$. Its objects are thin groupoids. Its morphisms from $A$ to
$B$ are strategies from $A$ to $B$, i.e. elements of $\T_{A\lin B}$ –
recall that they are $(S, \display^S : S \to A \times B)$, in particular spans
from $A$ to $B$

\[
A \xot{\display^S_A} S \xto{\display^S_B} B\,.
\]

The identities are identity spans, and composition is via
the pullback (<ref>). If $S$ and $T$ are strategies from $A$
to $B$, the $2$-cells from $S$ to $T$ are the positive morphisms
$(F, \phi) : S \to T$. As $\phi : \display^S \Rightarrow
\display^T \circ F$ is a family of positive morphisms on $A^\perp \parr
B$ with underlying plain groupoid $A \times B$, it may be equivalently
presented as pair of $F^A : \display^S_A \Rightarrow \display^T_A
\circ F$ and $F^B : \display^S_B \Rightarrow \display^T_B \circ F$,
as in <Ref>.

For horizontal composition of positive morphisms, we first proceed as in
<Ref> and obtain a connected groupoid of (non necessarily
positive) horizontal compositions – which must all have the same image through
the biequivalence of <Ref>, providing our unique positive
horizontal composition. Altogether, we have:

Those components form $\Thin$, a bicategory.

See details in <Ref>.

Next, we develop the further structure of $\Thin$.

§ CARTESIAN CLOSED STRUCTURE

To construct a cartesian closed bicategory, we intend to follow
[20]. We first turn the construction $\BFam$ –
thereafter denoted by $\oc$ – into a pseudocomonad, and then
equip the Kleisli bicategory $\Thin_{\oc}$ with the cartesian closed

§.§ The Pseudocomonad

We first develop the action of $\oc$ on objects of $\Thin$.

§.§.§ The bang of thin groupoids
First, $\oc$ is defined
on uniform groupoids via $\U_{\oc A} = (\oc \U_A)^{\perp \perp}$, where
we have used

\[
\oc \U_A = \{(\oc S, \oc \display^S) \mid S \in \U_A\}
\]

using the functorial action $\oc \display^S : \oc S \to \oc A$. For thin
groupoids, the positive and negative symmetries of $\oc A$ were defined in
<Ref>. The thin structure is set as $\T_{\oc A} = (\oc
\T_A)^{\pperp \pperp}$ – it is a direct verification that this is a thin

§.§.§ The bang of strategies
If $S \in \T_{A\lin B}$,
we have $\display^S = \tuple{\display^S_A, \display^S_B}$
for $\display^S_A : S \to A$ and $\display^S_B : S \to B$ – its bang

\[
\oc A \xot{\oc \display^S_A} \oc S \xto{\oc \display^S_B} \oc B
\]

packaged as $(\oc S, \tuple{\oc \display^S_A, \oc \display^S_B})$.
That this is in $\T_{\oc A \lin \oc B}$ relies on:

Consider $A, B$ thin groupoids, and $T$ a prestrategy from $\oc A$ to
$B$. Then, the following two properties hold:

\[
\begin{array}{rl}
\text{\emph{(1)}} &
\text{$T \in \U_{\oc A \lin B}$ iff $(T, \display^T_{\oc A}) \in
\U_{\oc A}^{\perp}$ and}\\
&\text{for all $S \in \U_A$, $T@\oc S \in \U_B$,}\\
\text{\emph{(2)}} &
\text{$T \in \T_{\oc A \lin B}$ iff for all $S \in \T_A$, $T@\oc S \in
\T_B$.}
\end{array}
\]

This is an immediate application of <Ref>.
Since $\U_{\oc A} = (\oc \U_A)^{\perp \perp}$ and $\T_{\oc A} = (\oc
\T_A)^{\pperp \pperp}$. From this lemma, it is a rather direct verification that
for any $S \in \T_{A\lin B}$, we have $\oc S \in \T_{\oc A \lin \oc B}$ as

§.§.§ A pseudofunctor

Since $\oc$ is a functor, it preserves the identity span on the nose.
Since $\oc$ preserves pullbacks, for $S \in \T_{A\lin B}$ and $T \in
\T_{B \lin C}$, the universal property gives us

\[
m_{S, T} : \oc (T \odot S) \iso \oc T \odot \oc S
\]

a strong invertible $2$-cell in $\Thin$. As expected, this $2$is natural
in $S$ and $T$ (with respect to positive morphisms). Altogether, we obtain a
pseudofunctor $\oc : \Thin \to \Thin$. See <Ref> for

§.§.§ A pseudomonad on groupoids
In fact we first turn $\oc$
into a pseudomonad on $\Gpd$, from which its pseudocomonad structure on
$\Thin$ shall be derived.
We noted earlier that we have a functor $\BFam : \Gpd \to \Gpd$ – in
fact, it is extended to a $2$-endofunctor on the $2$-category of small
groupoids, noted

\[
\oc : \Gpd \to \Gpd\,,
\]

defined on a $2$-cell $\alpha : F \Rightarrow G : A \to B$ as the
natural transformation $\oc\alpha : \oc F \Rightarrow \oc G$ with
components all pairs

\[
(\oc \alpha)_{(A_i)_{i\in I}} = (\id_I, (\alpha_{A_i})_{i\in I}) \in
\oc B((F A_i)_{i\in I}, (G A_i)_{i\in I})\,.
\]

To turn this into a pseudomonad, we must adjoin a multiplication and a
unit. The components of the unit are the functors

\[
\begin{array}{rcrcl}
\eta_A &:& A &\to& \oc A\\
&& a &\mapsto& (a)_{\{0\}} = [0 \cdot a]
\end{array}
\]

with the obvious functorial action. The intuition is that the unit
transports a single resource usage from $A$ to $\oc A$, arriving at a
singleton family. In doing so, it must select a copy index. Any natural
number will do – the rest of the paper does not depend on this choice
– but for definiteness and compatibility with the traditional
convention from AJM games, we pick $0$.

For the multiplication $\mu_A : \oc \oc A \to \oc A$, we must flatten a
family of families into a family. For this purpose, we fix an injective
function $\pair{-, -} : \mathbb{N}^2 \to \mathbb{N}$ – again, the
results of this paper do not depend on that choice. Given
$I \subseteq_f \mathbb{N}$ and a family $(J_i)_{i\in I}$ where $J_i
\subseteq_f \mathbb{N}$ for all $i \in I$, let us write

\[
\Sigma_{i\in I} J_i = \{\pair{i,j} \mid i \in I,~j \in J_i\}\,,
\]

which is by definition still a finite subset of $\mathbb{N}$. Then we

\[
\begin{array}{rcrcl}
\mu_A &:& \oc \oc A & \to & \oc A\\
&&((a_{i, j})_{j \in J_i})_{i \in I} &\mapsto& (a_{i,j})_{\pair{i,j}
\in \Sigma_{i\in I} J_i}
\end{array}
\]

for any groupoid $A$, along with the obvious functorial action.

Altogether this yields $\eta : \Id_{\Gpd} \Rightarrow \oc$ and $\mu : \oc \oc
\Rightarrow \oc$, two (strict 2-) natural transformations. The monad laws, if
they were to hold on the nose, would mean that $\pair{0, i} = \pair{i, 0} = i$
and $\pair{\pair{i, j}, k} = \pair{i, \pair{j, k}}$ for all $i, j, k \in
\mathbb{N}$; and it is clear that no injection satisfying those laws exists.
Nevertheless, for every groupoid $A$ the coherence laws for a monad hold up to
natural isomorphisms: we have $\alpha_A$, $\beta_A$ and $\gamma_A$ as
indicated in <Ref>. For instance, for any $(a_j)_{j
\in J} \in \oc A$:

\[
(\alpha_A)_{(a_j)_{j\in J}} : (a_j)_{j\in J} \sym_{\oc A}
(a_j)_{\pair{0, j} \in \Sigma_{i \in \{0\}} J}
\]

reindexing along the bijection $J \bij \Sigma_{i \in \{0\}} J$. The
other components act similarly – note that they are all
negative symmetries. The associated families
$(\alpha_A)_{A \in \Gpd}$, $(\beta_A)_{A\in \Gpd}$ and
$(\gamma_A)_{A\in \Gpd}$ satisfy the conditions for
modifications, and the additional coherence laws for a

The $2$-functor $\oc : \Gpd \to \Gpd$ along with the components above
yield a pseudomonad on $\Gpd$.

\[
\begin{tikzcd}[cramped,row sep=20pt, column sep=50pt]
\oc \oc A
\ar[dr,"\mu_A"',myname=mul]&
\oc A	\ar[l,"\eta_{\oc A}"']
\ar[r, "\oc \eta_A"]
\ar[d, "\id_{\oc A}"{description},myname=id]
\phar[from=mul,"\stackrel{\alpha_A}{\Rightarrow}"]&
\oc \oc A
\ar[dl,"\mu_A",myname=mur]\\
&\oc A
\phar[from=mur,to=1-2,"\stackrel{\beta_A}{\Leftarrow}"]
\end{tikzcd}
\]

Unit natural isomorphisms

\[
\begin{tikzcd}[cramped,row sep=3pt]
& \oc \oc \oc A
\ar[dl,"\mu_{\oc A}"']
\ar[dr,"\oc \mu_A"]\\
\oc \oc A
\ar[dr,"\mu_A"']
\phar[rr,"\stackrel{\gamma_A}{\Rightarrow}"]&&
\oc \oc A
\ar[dl,"\mu_A"]\\
&\oc A
\end{tikzcd}
\]

Associativity natural isomorphism

§.§.§ Lifting functors to spans
We shall turn $\oc$ into a
pseudocomonad on $\Thin$ by lifting the components above to spans.
In general, if $F : B \to A$ is a functor, then there is a span $\check

\[
A \xot{F} B \xto{\id_B} B\,,
\]

called the lifting of $F$ – but we need sufficient conditions on
$F$ for this construction to yield morphisms in $\Thin$. For that
purpose, if $A$ and $B$ are thin groupoids, we say that a functor $F :
A \to B$ is a renaming iff the following conditions hold:

\[
\begin{array}{rl}
\text{\emph{(1)}} &
\text{for all $\theta: a \sym_A a'$, if $\theta$ is positive then so is
$F \theta$,}\\
\text{\emph{(2)}} &
\text{for all $(T,\display^T) \in \U_B^\perp$, $(T, F \circ \display^T)
\in \U_A^\perp$,}\\
\text{\emph{(3)}} &
\text{for all $(T, \display^T) \in \T_B^{\pperp}$, $(T, F \circ
\display^T) \in \T_A^{\pperp}$.}
\end{array}
\]

Clearly, renamings compose – we consider the $2$-category $\Ren$ whose objects
are thin groupoids, whose morphisms are renamings, and whose $2$-cells are
negative natural transformations. As expected, lifting renamings yields thin
spans (see <Ref>). Lifting can be extended to $2$-cells: if
$\alpha : F \Rightarrow G : A \to B$ is a negative natural transformation, then
$\check \alpha$ is the positive morphism described by the diagram:

\[
\begin{tikzcd}[cramped,row sep=10pt]
&B	\ar[dl,"F"']
\ar[dr,"\id_B"]
\ar[dd,"\id_B"{description},myname=id]\\
A	\phar[to=id,"\stackrel{\alpha}{\Rightarrow}"]&&B\\
&B	\ar[ul,"G"]
\ar[ur,"\id_B"']
\end{tikzcd}\,,
\]

noting that this is positive as negative $\alpha$ is in contravariant position.
Altogether, we get (see details in <Ref>):

There is a pseudofunctor $\check{-} : \Ren^{\op} \to \Thin$.

Here, $\Ren^{\op}$ is $\Ren$ with the morphisms reversed, but the
$2$-cells unchanged. It can be checked that for any thin groupoid $A$,
the functors $\eta_A : A \to \oc A$ and $\mu_A : \oc \oc A \to \oc A$
are renamings, in particular for every thin groupoid $A$ we get

\[
\check{\eta_A} \in \Thin(\oc A, A)
\qquad
\check{\mu_A} \in \Thin(\oc A, \oc \oc A)
\]

the main components to turn $\oc$ into a pseudocomonad. Unlike in
$\Gpd$, the families $\check{\eta}$ and $\check{\mu}$ are not strict
$2$-natural transformations but only pseudonatural transformations,
with $2$-cells

\[
\begin{array}{rcrcl}
\eta_S &:& \check{\eta}_B \odot \oc S &\To& S \odot \check{\eta}_A\\
\mu_S &:& \check{\mu}_B \odot \oc S &\To& \oc \oc S \odot \check{\mu}_A\,,
\end{array}
\]

positive isomorphisms obtained for $S \in \Thin(A, B)$ from the
universal property of pullbacks, via the observation that $\eta :
\Id_{\Gpd} \Rightarrow \oc$ and $\mu : \oc \oc \Rightarrow \oc$ are
cartesian natural transormations. It may be checked that
$\eta_S$ and $\mu_S$ are natural in $S$ and satisfy the coherence
conditions of pseudonatural transformations. Finally, the modifications
$\alpha, \beta, \gamma$ involved in the pseudomonad structure of $\oc$
on $\Gpd$ lift to the modifications required for the pseudocomonad
structure of $\oc$ on $\Thin$.

We have a pseudocomonad $\oc$ on $\Thin$.

See details in <Ref>.

We move on to studying the Kleisli bicategory $\Thin_{\oc}$ whose
horizontal composition, denoted $\sthcb$, is defined as expected.

§.§ Cartesian Closed Structure

§.§.§ Finite products
First, we show that $\Thin_{\oc}$ has
finite products, i.e. is a fp-bicategory in the sense of
Fiore and Saville [18] – unlike them, we
work with binary products.

Terminal object
Write $\top$ for the empty groupoid, made a thin groupoid with
$\U_\top = \T_\top = \{\id_\emptyset\}$. For any thin groupoid
$A$, $\Thin_{\oc}(A, \top)$ has exactly one element – the empty groupoid.
Thus, $\Thin_{\oc}$ has a (strict) terminal object.

Binary product
If $A$ and $B$ are thin groupoids, then the with $A \with B$
has underlying groupoid $A + B$ the disjoint union, with $(A + B)_- =
A_- + B_-$ and $(A + B)_+ = A_+ + B_+$. We adjoin $\U_{A\with B} =
(\U_A + \U_B)^{\perp \perp}$ and $\T_{A\with B} = (\T_A + \T_B)^{\pperp
\pperp}$, where as usual, $\U_A + \U_B$ comprises the set of all $(S +
T, \display^S + \display^T)$ for $(S, \display^S) \in \U_A$ and $(T,
\display^T) \in \U_B$, using the functorial action of $+$
(and likewise for $\T_A + \T_B$).

Pairing and projections The projections are simply set as
$\stbpl = \widecheck{(\eta_{A+B}\circ \cplprot)} \in \Thin_{\oc}(A\with B, A)$
and $\stbpr = \widecheck{(\eta_{A+B}\circ \cprprot)} \in \Thin_{\oc}(A \with B,
B)$ for $\cpl\co A \to A+B$ and $\cpr\co B \to A+B$ the obvious
coprojections/renamings. The pairing of $S \in \Thin_{\oc}(\Gamma, A)$
and $T \in \Thin_{\oc}(\Gamma, B)$ is

\[
(S + T, \display_{\oc \Gamma} : S + T \to \oc \Gamma,
\display_{A \with B} : S + T \to A + B)
\]

with $\display_{\oc \Gamma}$ the co-pairing
and $\display_{A\with B} = \display^S_A + \display^T_B$. We have:

For any thin groupoids $\Gamma, A$ and $B$, there is

\[
\begin{tikzcd}[cramped,row sep=0pt,csbo=7.5em]
\Thin_{\oc}(\Gamma,A \with B)
\ar[rr,bend left=15,"{(\stbpl \sthcb -, \stbpr\sthcb - )}"]
\bot
\Thin_{\oc}(\Gamma,A)
\times
\Thin_{\oc}(\Gamma,B)
\ar[ll,bend left=15,"\tuple{-, -}"]
\end{tikzcd}
\]

an adjoint equivalence.

If $S \in \Thin_{\oc}(\Gamma, A)$ and $T \in \Thin_{\oc}(\Gamma,
B)$ there are

\[
% \begin{array}{rcrcl}
%   \omega^A_{S, T} &:& \check{l} \odot \tuple{S, T} &\iso& S\\
%   \omega^B_{S, T} &:& \check{r} \odot \tuple{S, T} &\iso& T
% \end{array}
\omega^A_{S, T} : \stbpl \sthcb \tuple{S, T} \iso S
\qquad
\omega^B_{S, T} : \stbpr \sthcb \tuple{S, T} \iso T
\]

positive isos, and for $U \in \Thin_{\oc}(\Gamma, A \with B)$ there is

\[
\bar{\omega}_U : U \iso \tuple{\stbpl \sthcb U, \stbpr \sthcb T}
\]

a positive iso, defined in the obvious way.
Those are all natural in $S, T, U$, and satisfy the required triangle

See <Ref> for more details. Altogether,
this establishes that $\Thin_{\oc}$ is a fp-bicategory in the
sense of [18].

§.§.§ Cartesian closure
If $A$ and $B$ are thin groupoids,
then we set $A\tto B = \oc A \parr B$. Before we describe the
additional components, we must observe the Seely equivalence:

\[
\begin{tikzcd}
\oc A \tensor \oc B
\ar[rr, bend left=10, "s_{A, B}"]&&
\oc (A \with B)
\ar[ll, bend left=10, "\bar{s}_{A, B}"]
\end{tikzcd}
\]

where $s_{A, B}$ sends $(a_i)_{i\in I}, (b_j)_{j\in J}$ to $(c_k)_{k\in I\imix
J}$, with $I\imix J = \ibij(I \sqcup J)$ for some chosen bijection $\ibij =
\coprodfact{\ibij_l}{\ibij_r}$ between $\N\sqcup \N$ and $\N$, and where
$c_{\ibij_l(i)} = a_i$ and $c_{\ibij_r(j)} = b_j$; and $\bar{s}_{A, B}$ sends
$(c_k)_{k\in K}$ to $(a_i)_{i\in I}, (b_j)_{j\in J}$ where $I \subseteq K$ is
the subset of those $i\in K$ such that $c_i = a_i \in A$, and likewise for
$b_j$. Both functors are renamings, and the isomorphisms witnessing the
equivalence are negative.

Via the Seely equivalence, we first define the evaluation as
the span with basic groupoid $\oc A \times B$, with left leg the

\[
\scalebox{.89}{$
\oc A \times B \to (\oc A \times B) \times \oc A \to \oc (\oc A \times
B) \times \oc A \xto{s_{A, B}} \oc ((A \tto B) \with A)
\]

and right leg the projection $\oc A \times B \to B$. This yields a thin
span $\evm_{A, B} \in \Thin_{\oc}((A \tto B)\with A, B)$. Now, we need

\[
\Lambda(-) : \Thin_{\oc}(\Gamma \with A, B) \to \Thin_{\oc}(\Gamma, A
\tto B)
\]

the currying functor: given $S \in \Thin_{\oc}(\Gamma \with A,
B)$, its currying $\Lambda(S)$ is simply $S$, with display map post-composed with

\[
\oc (\Gamma + A) \times B \stackrel{\bar{s}_{\Gamma, A}}{\simeq} (\oc
\Gamma \times \oc A) \times B
\iso \oc \Gamma \times (\oc A \times B)\,.
\]

With this data in place, we may finally prove:

For any groupoids $\Gamma, A, B$, there is

\[
\begin{tikzcd}
\Thin_{\oc}(\Gamma, A\tto B)
\ar[rr, bend left=15, "\evm_{A, B} \odot_{\oc} (- \with A)"]&\bot&
\Thin_{\oc}(\Gamma \with A, B)
\ar[ll, bend left=15, "\Lambda(-)"]
\end{tikzcd}
\]

an adjoint equivalence.

One can first show the existence of adjoint equivalence between the currying
operation $\stcurry-$, and a symmetric uncurrying operation $\stuncurry-$. The
unit and counit of this adjunction can be derived from the ones of the Seely
(adjoint) equivalence. One can then prove that $\stuncurry-$ is in fact
isomorphic to $\evm_{A, B} \odot_{\oc} (- \with A)$ in order to get the wanted

See <Ref> for details. Altogether, we have:

We have $\Thin_{\oc}$, a cartesian closed bicategory.

This entails that we can interpret types of the simply-typed
$\lambda$-calculus as thin groupoids, morphisms as thin spans and
rewrites between terms as certain positive isomorphisms [19].

§ CONCLUSION

This paper focuses on the construction of $\Thin_{\oc}$, leaving for
later its application to semantics of $\lambda$-calculi and programming
languages. We believe this opens multiple perspectives for further
research: firstly, we may explore the obtained interpretation of the
$\lambda$-calculus, which syntactically should correspond to the
sequence typing system of Vial [38] and to the
non-uniform $\lambda$-calculus of Melliès
[15]. We should explore links with other
models of the literature, notably with the weighted relational model
recasting ideas from [37], and with
generalized species of structures and template games. Another related
direction consists in accommodating another feature of template games,
the mechanism to capture scheduling and synchronization
[34], into thin spans.

In more semantic directions, we believe that with respect to generalized
species of structures, the fact that operations on thin spans involve
no quotient may be helpful in two ways: (1) individuals may be
ordered concretely, and the model should support continuous reasoning
allowing one to deal easily with infinite computation; and
(2) adding “typed” weights coming from an SMCC as in
[24] should be a lot simpler, since those
weigths no longer have to themselves be saturated.

§ ACKNOWLEDGMENT

Work supported by the ANR projects DyVerSe (ANR-19-CE48-0010-01) and PPS
(ANR-19-CE48-0014); and by the Labex MiLyon (ANR-10-LABX-0070) of Université
de Lyon, within the program “Investissements d'Avenir” (ANR-11-IDEX-0007),
operated by the French National Research Agency (ANR).

[1]
J. Girard, “Linear logic,” Theor. Comput. Sci., vol. 50, pp. 1–102,
1987. [Online]. Available: <https://doi.org/10.1016/0304-3975(87)90045-4>

[2]
T. Ehrhard, “Finiteness spaces,” Math. Struct. Comput. Sci., vol. 15,
no. 4, pp. 615–646, 2005. [Online]. Available:

[3]
D. de Carvalho, M. Pagani, and L. T. de Falco, “A semantic measure of the
execution time in linear logic,” Theor. Comput. Sci., vol. 412,
no. 20, pp. 1884–1902, 2011. [Online]. Available:

[4]
V. Danos and T. Ehrhard, “Probabilistic coherence spaces as a model of
higher-order probabilistic computation,” Inf. Comput., vol. 209,
no. 6, pp. 966–991, 2011. [Online]. Available:

[5]
J. Laird, G. Manzonetto, G. McCusker, and M. Pagani, “Weighted relational
models of typed lambda-calculi,” in 28th Annual ACM/IEEE Symposium
on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28,
2013.1em plus 0.5em minus 0.4emIEEE Computer Society, 2013,
pp. 301–310. [Online]. Available: <https://doi.org/10.1109/LICS.2013.36>

[6]
M. Pagani, P. Selinger, and B. Valiron, “Applying quantitative semantics to
higher-order quantum computing,” in The 41st Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
'14, San Diego, CA, USA, January 20-21, 2014, S. Jagannathan and P. Sewell,
Eds.1em plus 0.5em minus 0.4emACM, 2014, pp. 647–658.
[Online]. Available: <https://doi.org/10.1145/2535838.2535879>

[7]
T. Ehrhard, M. Pagani, and C. Tasson, “Full abstraction for probabilistic
PCF,” J. ACM, vol. 65, no. 4, pp. 23:1–23:44, 2018. [Online].
Available: <https://doi.org/10.1145/3164540>

[8]
P. Clairambault and M. de Visme, “Full abstraction for the quantum
lambda-calculus,” Proc. ACM Program. Lang., vol. 4, no. POPL, pp.
63:1–63:28, 2020. [Online]. Available: <https://doi.org/10.1145/3371131>

[9]
D. de Carvalho, “Execution time of lambda-terms via denotational semantics and
intersection types,” CoRR, vol. abs/0905.4251, 2009. [Online].
Available: <http://arxiv.org/abs/0905.4251>

[10]
B. Accattoli, S. Graham-Lengrand, and D. Kesner, “Tight typings and split
bounds, fully developed,” J. Funct. Program., vol. 30, p. e14, 2020.
[Online]. Available: <https://doi.org/10.1017/S095679682000012X>

[11]
A. Bucciarelli, D. Kesner, and S. R. D. Rocca, “Inhabitation for
non-idempotent intersection types,” Log. Methods Comput. Sci.,
vol. 14, no. 3, 2018. [Online]. Available:

[12]
S. Abramsky, R. Jagadeesan, and P. Malacaria, “Full abstraction for PCF,”
Inf. Comput., vol. 163, no. 2, pp. 409–470, 2000.

[13]
J. M. E. Hyland and C. L. Ong, “On full abstraction for PCF: i, ii, and
III,” Inf. Comput., vol. 163, no. 2, pp. 285–408, 2000. [Online].
Available: <https://doi.org/10.1006/inco.2000.2917>

[14]
P. Baillot, V. Danos, T. Ehrhard, and L. Regnier, “Timeless games,” in
Computer Science Logic, 11th International Workshop, CSL '97, Annual
Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected
Papers, ser. Lecture Notes in Computer Science, M. Nielsen and W. Thomas,
Eds., vol. 1414.1em plus 0.5em minus 0.4emSpringer, 1997, pp.
56–77. [Online]. Available: <https://doi.org/10.1007/BFb0028007>

[15]
P. Melliès, “Asynchronous games 2: The true concurrency of innocence,”
Theor. Comput. Sci., vol. 358, no. 2-3, pp. 200–228, 2006.

[16]
P. Boudes, “Thick subtrees, games and experiments,” in Typed Lambda
Calculi and Applications, 9th International Conference, TLCA 2009,
Brasilia, Brazil, July 1-3, 2009. Proceedings, ser. Lecture Notes in
Computer Science, P. Curien, Ed., vol. 5608.1em plus 0.5em minus
0.4emSpringer, 2009, pp. 65–79. [Online]. Available:

[17]
T. Leinster, Higher operads, higher categories.1em plus 0.5em
minus 0.4emCambridge University Press, 2004, no. 298.

[18]
M. Fiore and P. Saville, “Coherence for bicategorical cartesian closed
structure,” Math. Struct. Comput. Sci., vol. 31, no. 7, pp. 822–849,
2021. [Online]. Available: <https://doi.org/10.1017/S0960129521000281>

[19]
——, “A type theory for cartesian closed bicategories (extended
abstract),” in 34th Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019.1em
plus 0.5em minus 0.4emIEEE, 2019, pp. 1–13. [Online]. Available:

[20]
M. Fiore, N. Gambino, M. Hyland, and G. Winskel, “The cartesian closed
bicategory of generalised species of structures,” Journal of the
London Mathematical Society, vol. 77, no. 1, pp. 203–220, 2008.

[21]
S. Castellan, P. Clairambault, and G. Winskel, “Thin games with symmetry and
concurrent hyland-ong games,” Log. Methods Comput. Sci., vol. 15,
no. 1, 2019.

[22]
H. Paquet, “Probabilistic concurrent game semantics,” Ph.D. dissertation,

[23]
P. Melliès, “Template games and differential linear logic,” in
LICS.1em plus 0.5em minus 0.4emIEEE, 2019, pp.

[24]
T. Tsukada, K. Asada, and C. L. Ong, “Species, profunctors and taylor
expansion weighted by SMCC: A unified framework for modelling
nondeterministic, probabilistic and quantum programs,” in
LICS.1em plus 0.5em minus 0.4emACM, 2018, pp.

[25]
Z. Galal, “A profunctorial scott semantics,” in 5th International
Conference on Formal Structures for Computation and Deduction, FSCD 2020,
June 29-July 6, 2020, Paris, France (Virtual Conference), ser. LIPIcs, Z. M.
Ariola, Ed., vol. 167.1em plus 0.5em minus 0.4emSchloss
Dagstuhl - Leibniz-Zentrum für Informatik, 2020, pp. 16:1–16:18.
[Online]. Available: <https://doi.org/10.4230/LIPIcs.FSCD.2020.16>

[26]
——, “A bicategorical model for finite nondeterminism,” in 6th
International Conference on Formal Structures for Computation and Deduction,
FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference),
ser. LIPIcs, N. Kobayashi, Ed., vol. 195.1em plus 0.5em minus
0.4emSchloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021,
pp. 10:1–10:17. [Online]. Available:

[27]
T. Tsukada, K. Asada, and C. L. Ong, “Generalised species of rigid resource
terms,” in 32nd Annual ACM/IEEE Symposium on Logic in Computer
Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017.1em plus
0.5em minus 0.4emIEEE Computer Society, 2017, pp. 1–12. [Online].
Available: <https://doi.org/10.1109/LICS.2017.8005093>

[28]
F. Olimpieri, “Intersection type distributors,” in LICS.1em
plus 0.5em minus 0.4emIEEE, 2021, pp. 1–15.

[29]
A. Kerinec, G. Manzonetto, and F. Olimpieri, “Why are proofs relevant in
proof-relevant models?” 2023, accepted in POPL 2023.

[30]
G. M. Kelly and M. L. Laplaza, “Coherence for compact closed categories,”
Journal of pure and applied algebra, vol. 19, pp. 193–213, 1980.

[31]
F. Lamarche, “Quantitative domains and infinitary algebras,” Theor.
Comput. Sci., vol. 94, no. 1, pp. 37–62, 1992. [Online]. Available:

[32]
M. Stay, “Compact closed bicategories,” arXiv preprint
arXiv:1301.1053, 2013.

[33]
A. E. Hoffnung, “Spans in 2-categories: A monoidal tricategory,” arXiv
preprint arXiv:1112.0560, 2011.

[34]
P. Melliès, “Categorical combinatorics of scheduling and synchronization
in game semantics,” Proc. ACM Program. Lang., vol. 3, no. POPL,
pp. 23:1–23:30, 2019.

[35]
P. Baillot, V. Danos, T. Ehrhard, and L. Regnier, “Believe it or not, ajm's
games model is a model of classical linear logic,” in LICS.1em plus 0.5em minus 0.4emIEEE Computer Society, 1997, pp. 68–75.

[36]
S. Castellan, P. Clairambault, and G. Winskel, “Symmetry in concurrent
games,” in CSL-LICS.1em plus 0.5em minus 0.4emACM,
2014, pp. 28:1–28:10.

[37]
P. Clairambault and H. Paquet, “The quantitative collapse of concurrent games
with symmetry,” CoRR, vol. abs/2107.03155, 2021.

[38]
P. Vial, “Infinitary intersection types as sequences: A new answer to klop's
problem,” in LICS.1em plus 0.5em minus 0.4emIEEE
Computer Society, 2017, pp. 1–12.

[39]
T. Ehrhard, “The scott model of linear logic is the extensional collapse of
its relational model,” Theor. Comput. Sci., vol. 424, pp. 20–45,

[40]
E. Cheng, M. Hyland, and J. Power, “Pseudo-distributive laws,”
Electronic Notes in Theoretical Computer Science, vol. 83, pp.
227–245, 2003.

In the following, we will type spans $A \xot{u} S \xto{v} B$ between groupoids
or thin groupoids $A$ and $B$ as $S \co A \stto B$.

§.§ Bipullbacks

In order to complete the equational definition of bipullbacks of
<Ref>, it is useful to consider the intensional definition
first: given a $2$$C$ with invertible $2$(a
$(2,1)$) and a cospan $S \xto{u} B \xot{v} T$ in $C$, a bipullback is a
pseudocone $(P,l,r,\mu)$ as in <Ref> such that, for every $X \in C$,
the precomposition of the pseudocone $(P,l,r,\mu)$ by morphisms $X \to P$
induces an equivalence of categories between $C(X,P)$ and the category of
pseudocones over the cospan $S \xto{u} B \xot{v} T$ and of vertex $X$ and
pseudocone morphisms. The essential surjectiveness of this precomposition
corresponds exactly to the condition <Ref> of
<Ref>. Its full faithfulness can be expressed as the following

*  given a $2$equality

\[
\begin{tikzcd}
\ar[d,"h"{description}]
\\
\ar[dl,"l"']
\ar[dr,"r"]
\\
\ar[dr,"u"']
\phar[rr,"\xTo{\mu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}
\qeq
\begin{tikzcd}
& X	\ar[ddl,bend right=30, "l \circ h"',myname=lp]
\ar[ddr,bend left=30, "r \circ h",myname=rp]
\ar[d,"h'"{description}]\\
& P     \ar[dl,"l"']
\ar[dr,"r"]
\phar[to=rp,"\xTo{\beta}"]
\phar[from=lp,"\xTo{\alpha}"]\\
S       \ar[dr,"u"']
\phar[rr,"\xTo{\mu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}
\]

for some $h,h' \co X \to P$ and $2$$\alpha \co l \circ h \To l \circ
h'$ and $\beta \co r \circ h' \To r \circ h$, there is a unique $\theta \co h
\To h'$ such that $\alpha = l \theta$ and $\beta = r \finv\theta$.

It is not too difficult to show that the latter property is equivalent to the
one asserting that, given two decompositions of a pseudocone $\nu$

\[
\adjustbox{scale=.8}{%
\begin{tikzcd}[csbo=3em]
& X     \ar[ddl,bend right=30, "l'"',myname=lp]
\ar[ddr,bend left=30, "r'",myname=rp]
\\\\
S       \ar[dr,"u"']
\phar[rr,"\xTo{\nu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}}
\qeq
\adjustbox{scale=.8}{%
\begin{tikzcd}[csbo=3em]
& X	\ar[ddl,bend right=30, "l'"',myname=lp]
\ar[ddr,bend left=30, "r'",myname=rp]
\ar[d,"h"{description}]
\\
& P     \ar[dl,"l"']
\ar[dr,"r"]
\phar[to=rp,"\xTo{\beta}"]
\phar[from=lp,"\xTo{\alpha}"]\\
S       \ar[dr,"u"']
\phar[rr,"\xTo{\mu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}}
\qeq
\adjustbox{scale=.8}{%
\begin{tikzcd}[csbo=3em]
& X	\ar[ddl,bend right=30, "l'"',myname=lp]
\ar[ddr,bend left=30, "r'",myname=rp]
\ar[d,"h'"{description}]
\\
& P     \ar[dl,"l"']
\ar[dr,"r"]
\phar[to=rp,"\xTo{\beta'}"]
\phar[from=lp,"\xTo{\alpha'}"]\\
S       \ar[dr,"u"']
\phar[rr,"\xTo{\mu}"]&&
T       \ar[dl,"v"]\\
\end{tikzcd}}
\]

there exists a unique $\theta \co h \To h'$ such that $l \theta = \alpha' \circ
\finv\alpha$ and $r \theta = \finv{\beta'} \circ \beta$, or equivalently
$\alpha' = (l\theta) \circ \alpha$ and $\beta' = \beta \circ (r \finv\theta)$,
which is the complete form of the condition <Ref>.

§.§ Pullbacks in $\Gpd$

It happens that pullbacks in $\Gpd$ are well-behaved w.r.t $2$:

A pullback of a cospan $S \xto{u} B \xot{v} T$ in $\Gpd$ is a strict $2$,
that is, also admits a universal factorization property w.r.t. morphisms of cones.

Let $I$ be the groupoid consisting of a walking isomorphism $u$ between two
objects $0$ and $1$. Given two functors $F$ and $G$ between two groupoids $C$
and $D$, a $2$
\[
\alpha \co F \To G \co C \to D \in \Gpd
\]

is then exactly the data of a functor $H \co I \times C \to D$ such that
$H(0,-) = F$ and $H(1,-) = G$. Using this correspondence, the property that a
pullback $(P,l,r)$ over the cospan is a $2$easily reduces to the one
that $(P,l,r)$ is a $1$.

Note that a pullback is a cone, which is in particular a pseudocone with
identity as inner $2$. One might then ask when a pullback is a bipullback,
in which case we have the following characterization:

Let $(P,l,r)$ be a pullback over a cospan $S \xto{u} B \xot{v} T$ in $\Gpd$.
Then the pseudocone induced by $(P,l,r)$ is a bipullback if and only if it
satisfies the condition <Ref> of

By <Ref>, $(P,l,r)$ is a $2$, so that it
satisfies a universal property w.r.t. cone morphisms. This condition is in
fact exactly <Ref> which is equivalent to
<Ref>. Thus, only <Ref>
is left to check for $(P,l,r)$ to be a bipullback.

We can then refine the previous proposition into a pointwise
characterization in the form of already stated <Ref> for
which we now provide a proof.

The implication is immediate, since the data of an isomorphism $\theta \co
f(s) \to g(t)$ is equivalent to the one of a pseudocone on S
[r,"f"] & B & T [l,"g"'] of vertex the terminal groupoid, whose
factorization in the form of the condition of
<Ref> is exactly the wanted property.

We now show the converse property. So let

\[
\begin{tikzcd}
\ar[ld,"h"',bend right=20]
\ar[rd,"k",bend left=20]
\\[1em]
\ar[rd,"f"']
\cphar[rr,"\xTo\theta"{yshift=1em}]
\ar[ld,"g"]
\\
\end{tikzcd}
\]

be a pseudocone. By hypothesis, for every $z\in Z$, there exist $s_z \in S$,
$\phi_z \co h(z) \to s_z$, $t_z \in T$, $\psi_z \co t_z \to k(z)$ such that
$f(s_z) = g(t_z)$ and $\theta_z = g(\psi_z) \circ f(\phi_z)$. The
collection of isomorphisms $(\phi_z)_{z \in Z}$ induces a functor $h'$ defined
by $h'(z) = s_z$ for $z \in Z$, and $h'(w) = \phi_{z'} \circ h(w) \circ
\finv \phi_z$ for $w \co z \to z' \in Z$. Similarly, we get a functor $k'$
defined by $h'(z) = t_z$ for $z \in Z$, and $k'(w) = \finv \psi_{z'} \circ
k(w) \circ \psi_z$ for $w \co z \to z' \in Z$. Given $w \co z \to z' \in Z$, we
check that $f \circ h'(w)$ and $g \circ k'(w)$ are equal. Since there
are only isomorphisms involved, it is enough to check that the equality holds
when in the context $g(\psi_{z'}) \circ (-) \circ f(\phi_z)$:

\begin{align*}
g(\psi_{z'}) \circ f (h'(w))\circ f(\phi_z)
g(\psi_{z'}) \circ f(h'(w) \circ \phi_z)
\\
g(\psi_{z'}) \circ f(\phi_{z'} \circ h(w))
\\
g(\psi_{z'}) \circ f(\phi_{z'}) \circ f(h(w))
\\
\theta_{z'} \circ f(h(w))
\\
g(k(w)) \circ \theta_{z}
\\
g(k(w)) \circ  g(\psi_{z}) \circ f(\phi_{z})
\\
g(\psi_{z'}) \circ  g(k'(w)) \circ f(\phi_{z})\zbox.
\end{align*}

Thus, $(Z,h',k')$ is a cone on S [r,"f"] & B & T [l,"g"'],
so there exists $m \co Z \to P$ which factors $h'$ and $k'$ through $\pl$ and
$\pr$. The collections $(\phi_z)_{z\in Z}$ and $(\psi_z)_{z\in Z}$ defines
natural isomorphisms $\phi \co h \To \pl \circ m$ and $\psi \co \pr \circ m
\To k$ which satisfy $(g \psi) \circ (f \phi) = \theta$. Hence, the condition
of <Ref> is satisfied and $(P,\pl,\pr)$ is a

We also have the following criterion for rectangles of bipullbacks:

Given a rectangle made of two squares which are pullbacks in $\Gpd$ as in

\[
\begin{tikzcd}
\ar[rd,phantom,very near start,"\drcorner"]
\ar[r,"\pi^L_M"]
\ar[d,"\pi^L_A"']
\ar[rd,phantom,very near start,"\drcorner"]
\ar[r,"\pi^M_R"]
\ar[d,"\pi^M_B"{description}]
\ar[d,"h"]
\\
\ar[r,"f"']
\ar[r,"g"']
\end{tikzcd}
\zbox,
\]

the following hold:

*  if the whole
rectangle is a bipullback, then the left square is too;

*  if the left and
right square are bipullback, then the whole rectangle is a bipullback.

We first prove <ref>. For this
purpose, we use <Ref>. So let $a \in A$, $m \in
M$ and $\theta \co f(a) \to \pi^M_B(m)$. We have that $g(\theta)$ is a
morphism from $g\circ f(a)$ to $g\circ \pi^M_B(m) = h\circ \pi^M_R(m)$. Since
the outer rectangle is assumed to be a bipullback, there exist $a' \in A$, $r'
\in R$, $u^A \co a \to a' \in A$, $v^R \co r' \to \pi^M_R(m)$ such that
$g(\theta) = h(v^R) \circ (g\circ f)(u^A)$. Thus, we have $g(\theta \circ
\finv{(f(u^A))}) = h(v^R)$. Since the right square is a pullback, there exists
a unique $w^M$ such that $\pi^M_B(w^M) = \theta \circ \finv{(f(u^A))}$ and
$\pi^M_R(w^M) = v^R$. Moreover, by the right pullback again, the target of
$w^M$ is $m$; its source is some $m'$ such that $\pi^M_B(m') = f(a')$. Then,
we have that $\theta = \pi^M_B(w^M) \circ f(u^A)$. We can conclude with
<Ref> that the left pullback is a bipullback.

We now prove <ref> using
<Ref> again. So let $a \in A$, $r \in R$ and
$\theta \co (g\circ f)(a) \to h(r)$. Since the right square is a bipullback,
there exist $b' \in B$, $r' \in R$, $u^B \co f(a) \to b'$ and $v^R \co r' \to
r$ such that $\theta = h(v^R) \circ g(u^B)$. Since $b'$ and $r'$ have the same
projection in $C$ through $g$ and $h$ respectively, there exists $m' \in M$
such that $\pi^M_B(m') = b'$ and $\pi^M_R(m') = r'$. Thus, we have $u^B \co
f(a) \to \pi^M_B(m')$. Since the left square is a bipullback, there exist $a''
\in A$, $m'' \in M$, $\tilde u^A \co a \to a''$, $\tilde v^M \co m'' \to m'$
such that $u^B = \pi^M_B(\tilde v^M) \circ f(\tilde u^A)$. We thus have

\begin{align*}
\theta
h(v^R) \circ g(u^B)
h(v^R) \circ g(\pi^M_B(\tilde v^M) \circ f(\tilde u^A))
\\
h(v^R) \circ g(\pi^M_B(\tilde v^M)) \circ g(f(\tilde u^A))
\\
h(v^R) \circ h(\pi^M_R(\tilde v^M)) \circ g(f(\tilde u^A))
\\
h(v^R \circ \pi^M_R(\tilde v^M)) \circ (g\circ f)(\tilde u^A)
\end{align*}

which is precisely the factorization required by
<Ref> to conclude that the whole rectangle is a

§.§ Uniformity and thinness

Several arguments concerning uniformity requires some sort of diagram chasing
relative to bipullbacks. An important lemma for this is the following:

Consider the diagram in $\Gpd$

\[
\begin{tikzcd}[rsbo=3em,csbo=4em]
\ar[ld,"\pl^{S}_{P}"']
\ar[rd,"\pr^{S}_{Q}"]
\phar[dd,"2"]
\cphar[dd,near start,"\dcorner"]
\\
\ar[ld,"\pl^{P}_{L}"']
\ar[rd,"\pr^{P}_{M}"{description}]
\phar[dd,"1"]
\cphar[dd,near start,"\dcorner"]
\ar[ld,"\pl^{Q}_{M}"{description}]
\ar[rd,"\pr^{Q}_{R}"]
\phar[dd,"3"]
\cphar[dd,near start,"\dcorner"]
\\
\ar[rd,"f^L_A"']
\ar[ld,"{f^M_A}"]
\ar[rd,"{f^M_B}"']
\ar[ld,"f^R_B"]
\\
\end{tikzcd}
\]

where the square $1$, $2$ and $3$ are pullbacks, and derive from it the
following diagram using the product structure:

\[
\begin{tikzcd}[column sep={5em,between origins}]
\ar[dl,"\pr^{P}_M \circ \pl^S_{P}"']
\ar[dr,"\gpdprodfactp {\pl^{P}_L \circ \pl^S_{P},\pr^{Q}_R \circ \pr^S_{Q}}"]
\phar[dd,"4"]
\\
\ar[dr,"\gpdprodfactp{f^M_A,f^M_B}"']
L \times R
\ar[dl,"f^L_A\times f^R_B"]
\\
A \times B
\end{tikzcd}
\]

Then $4$ is a pullback.
Moreover, the following hold:

*  if $1$ and the rectangle made of
$2$ and $3$ are bipullbacks, then $4$ is a bipullback;

*  if $3$ and the rectangle made of
$1$ and $2$ are bipullbacks, then $4$ is a bipullback;

*  if $4$ is a bipullback, then the
rectangle made of $1$ and $2$ ($2$ and $3$) is a bipullback.

The fact that 4 is a pullback is an easy consequence of the fact that 1,2,3
are pullbacks.

One can then use <Ref> without too much trouble on the
different bipullback hypotheses in order to deduce that the wanted pullbacks
are bipullbacks.

With the above tool, we can now prove <Ref>.
We first prove the first
implication, and start by showing <Ref>. So let
$(S,\display^S_A) \in \SU$. Given $(U,\display^U_B) \in \U_B^\perp$, we must
show that $T@S \perp U$. By hypothesis, we have that $T \perp S \times U$, the pullback of $\display^T_{A \times B}$ and $\display^S_A \times
\display^U_B$ is a bipullback. Thus, we conclude by
<Ref><ref> that the
pullback of $\display^{T@S}_B$ and $\display^U_B$ is a bipullback, $T@S \perp U$. Hence, $T@S \in \U_B$.

We now show <Ref>. Since $\id_B$ is an isofibration,
we have that the pullback of $\display^T_B$ and $\id_B$ is a bipullback. Thus,
given $U \in \U_A$, by <Ref>, we have that
$\display^T_A \perp \display^U_A$ if and only if $\display^T_{A\times B} \perp
\display^U_A \times \id_B$. But the latter holds, since $T \in \U_{A \lin B}$.
Hence, $\display^T_A \in \U_A^\perp$.

We now show the converse implication. So assume that $T$ satisfies
<Ref>. First note that, since
$(A,\id_A) \in \U_A$, we have that $\display^T_B \in \U_B^\perp$ by
<Ref>. Given $V \in \U_B$, we must show that, for every
$U \in \U_A$, we have $T \perp U \times V$. Since we have $\display^T_B \perp
\display^V_B$, by <Ref>, this is equivalent to have $U
\perp \dual T@V$ for every $U \in \U_A$. By hypothesis, it is equivalent to
only check the previous condition for $U \in S$. By
<Ref> again, it is equivalent to check that $T \perp U
\times V$ for every $U \in S$. Since $U \perp \display^T_A$, by
<Ref> again, it is equivalent to check that $T@U \perp
V$, but the latter holds by <ref>. Thus, $T \in \U_{A \lin

Using <Ref>, we can prove the compatibility of uniformity with

Given uniform groupoids $(A,\U_A)$ and $(B,\U_B)$ and prestrategies $S \in
\U_{A \lin B}$ and $T \in \U_{B \lin C}$, we have $T \sthc S \in \U_{A \lin C}$.

Recall that the composition of the two spans $S$ and $T$ is formed as in
<Ref>. We show the uniformity of $T \sthc S$ using
<Ref> with $\U_A$ taken as generating class of $\U_A$. The
fact that <Ref> is satisfied for $T \sthc S$ is immediate
from its validity for both $S$ and $T$. The fact that
<Ref> holds, that is, that $\display^S_A \circ \pl
\in \U_A^\perp$, is a consequence of the fact that $\display^T_B \in
\U_B^\perp$ by <Ref> on $T$, and the dual of
<Ref> for $S$, asserting in particular that $\dual S$ maps
elements of $\U_B^\perp$ to $\U_A^\perp$.

We handle thinness similarly, and start by proving <Ref>:

Assume that $T \in \T_{A \lin B}$ and let $S \in \SU$. By
<Ref>, we already have $T@S \in \U_{A \lin B}$. Next, we use
the fact that $\T_B = \T_B^{\pperp\pperp}$ to show that $T@S \in \T_B$. So let
$U \in \T_B^{\pperp}$. By <Ref>, we have $T@S \pperp
U$ iff $T \pperp S \times U$. But the latter holds since $T\in \T_{A \lin B}$
and $S \in \SU \subseteq \T_A$. Thus, $T@S \in \T_B$.

Conversely, assume that $T@S \in \T_B$ for every $S \in \SU$. First observe
that $\T_{A \lin B} = (\T_A \otimes \T_B^{\pperp})^{\pperp}$. So we must show
that, for every $S \in \T_A$ and $U \in \T_B^{\pperp}$, $T \pperp S\times U$. By
<Ref>, for a given $U$, the latter is equivalent to $S
\pperp \dual T@U$ for every $S \in \T_A$, $\dual T@U \in \T_A^{\pperp}$. But
since $\T_A^{\pperp} = \SU^{\pperp}$, for a given $U$, it is equivalent to $S
\pperp \dual T@U$ for every $S \in \SU$, itself equivalent to $T \pperp
S\times U$ for every $S \in \SU$, and finally equivalent to $T@S \pperp U$ for
every $S\in \SU$, which amounts to our initial assumption.

Using <Ref>, we can then prove the compatibility of thinness
with composition:

Given thin groupoids $A$ and $B$ and strategies $S \in \U_{A \lin B}$ and
$T \in \U_{B \lin C}$, we have $T \sthc S \in \T_{A \lin C}$.

The proof is similar to (in fact simpler than) the one of
<Ref> and follows from the criterion given
by <Ref>.

§.§ Details about the bicategory $\Thin$

We have the following convenient characterization of $0$of
$2$of $\Thin$:

Given thin groupoids $A,B,C$, strategies $\rho,\rho' \co A \stto B$,
$\sigma,\sigma' \co B \stto C$ and weak morphisms $F \co \rho \To \rho'$ and
$G \co \sigma \To \sigma'$ of $\Thin$, if there exist a functor $\stsupp H \co
\stsupp{\sigma\sthcomp\rho} \to \stsupp{\sigma'\sthcomp\rho'}$ and two natural
transformations $H^l$ and $H^r$ as in

\[
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pl"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^l}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"]
\\
\rho
\ar[r,"\stsupp F"']
\rho'
\end{tikzcd}
\qqand
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pr"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^r}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"]
\\
\sigma
\ar[r,"\stsupp G"']
\sigma'
\end{tikzcd}
\]

such that

\[
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pl"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^l}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"]
\\
\rho
\ar[r,"\stsupp F"{description}]
\ar[d,"\stdisp\rho_B"']
\cphar[rd,"\xTo{F^B}"]
\rho'
\ar[d,"\stdisp{\rho'}_B"]
\\
\ar[r,equals]
\end{tikzcd}
\qeq
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pr"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^r}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"]
\\
\sigma
\ar[r,"\stsupp G"{description}]
\ar[d,"\stdisp\sigma_B"']
\cphar[rd,"\xTo{G^B}"]
\sigma'
\ar[d,"\stdisp{\sigma'}_B"]
\\
\ar[r,equals]
\end{tikzcd}
\]

and such that the natural transformations

\[
\defeq
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pl"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^l}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"]
\\
\rho
\ar[r,"\stsupp F"{description}]
\ar[d,"\stdisp\rho_A"']
\cphar[rd,"\xTo{F^A}"]
\rho'
\ar[d,"\stdisp{\rho'}_A"]
\\
\ar[r,equals]
\end{tikzcd}
\defeq
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pr"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^r}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"]
\\
\sigma
\ar[r,"\stsupp G"{description}]
\ar[d,"\stdisp\sigma_C"']
\cphar[rd,"\xTo{G^C}"]
\sigma'
\ar[d,"\stdisp{\sigma'}_C"]
\\
\ar[r,equals]
\end{tikzcd}
\]

are positive over $A^\perp$ and $C$ respectively, we have that $H \defeq
(\stsupp H,H^A,H^C)$ is a positive morphism $\sigma\sthcomp\rho \To
\sigma'\sthcomp\rho'$ of $\Thin$ and that $H = G \sthc F$.

The fact that $H$ is a $2$$\sigma\sthcomp\rho \To \sigma'\sthcomp\rho'$
of $\Thin$ is immediate by the polarity assumption. The equality of $2$given by the hypothesis can be rewritten as

\[
\begin{tikzcd}[rsbo=large,csbo=large]
\stsupp{\sigma\sthc\rho}
\ar[dd,"\stsupp H"{description}]
\ar[ld,myname=leftcone]
\ar[rd,myname=rightcone]
\\
\stsupp\rho
\ar[dd,"\stsupp F"']
\ar[rd,phantom,"{\xTo{H^l}}"]
\stsupp\sigma
\ar[dd,"\stsupp G"]
\ar[ld,phantom,"{\xTo{\finv{(H^r)}}}"]
\\
\ar[dl]
\ar[dr]
\\
\stsupp {\rho'}
\ar[dr,"\stdisp{\rho'}_B"']
\stsupp{\sigma'}
\ar[dl,"\stdisp{\sigma'}_B"]
\\
\end{tikzcd}
\qeq
\begin{tikzcd}[rsbo=huge,csbo=4.4em]
\stsupp{\sigma\sthc\rho}
\ar[ld]
\ar[rd]
\\
\stsupp\rho
\ar[d,"\stsupp F"']
\ar[rdd,bend left,myname=midleft,"\stdisp\rho_{B}"{inner sep=0pt},pos=0.4]
\stsupp\sigma
\ar[d,"\stsupp G"]
\ar[ldd,bend right,myname=midright,"\stdisp\sigma_{B}"'{inner sep=0pt},pos=0.4]
\\
\ar[rd,"\stdisp{\rho'}_B"']
\ar[ld,"\stdisp{\sigma'}_B"]
\\
\ar[from=stsupprhop,to=midleft,phantom,"{\xTo{\finv{(F^B)}}}"]
\ar[from=midright,to=stsuppsigmap,phantom,"{\xTo{G^B}}"]
\end{tikzcd}
\]

so that $H^l$ and $H^r$ provide a factorization of the pseudocone on the
right, and define an object of the groupoid of compositions mentioned in
<Ref>. The actual horizontal composition in $\Thin$ is
then obtained by applying the biequivalence of <Ref>. But
since $\pair{H^A,H^C}$ is already a positive natural transformation on $\cA
\lin \cC$, this biequivalence does nothing on this object and $H = G \sthc F$.

Given thin groupoids $\cA,\cB,\cC$, we have a functor

\[
(-)\sthcomp (-) \co \Thin(\cB,\cC) \times \Thin(\cA,\cB) \to \Thin(\cA,\cC)\zbox.
\]

By the definition we took for the composition of the $2$of $\Thin$, we
already have that $(-)\sthcomp(-)$ respects the sources and targets of weak
morphisms, so that we are left to verify functoriality.

Given $\rho \in \Thin(\cA,\cB)$ and $\sigma \in\Thin(\cB,\cC)$, a solution
in $\stsupp H$, $H^l$ and $H^r$ for the equation

\[
\begin{tikzcd}
\stsupp{\sigma\sthc\rho}
\ar[r,"\stsupp H"]
\ar[d,"\pl"']
\cphar[rd,"\xTo{H^l}"]
\stsupp{\sigma\sthc\rho}
\ar[d,"\pl"]
\\
\stsupp{\rho}
\ar[r,myname=midarr,"\id_{\stsupp\rho}"{description}]
\ar[d,myname=rhodisp,"\stdisp\rho_B"']
\cphar[rd,"="]
\stsupp{\rho}
\ar[d,myname=rhopdisp,"\stdisp\rho_B"]
\\
\ar[r,equals]
\end{tikzcd}
\qeq
\begin{tikzcd}
\stsupp{\sigma\sthc\rho}
\ar[r,"\stsupp H"]
\ar[d,"\pr"']
\cphar[rd,"\xTo{H^r}"]
\stsupp{\sigma\sthc\rho}
\ar[d,"\pr"]
\\
\stsupp{\sigma}
\ar[r,myname=midarr,"\id_{\stsupp\sigma}"{description}]
\ar[d,myname=rhodisp,"\stdisp\sigma_B"']
\cphar[rd,"="]
\stsupp{\sigma}
\ar[d,myname=rhopdisp,"\stdisp\sigma_B"]
\\
\ar[r,equals]
\end{tikzcd}
\]

is given by $\stsupp H = \id_{\rho\sthcomp\sigma}$, $H^l = \id_{\pl}$ and $H^r
= \id_{\pr}$. Thus, since identities are member of $A^-$ and $C^+$, the
polarity condition of <Ref> is satisfied so that

\[
\id_\sigma \sthc \id_\rho
\qeq
(\id_{\stsupp{\sigma\sthcomp\rho}},\id_{\stdisp\rho_A \circ \pl},\id_{\stdisp\sigma_C\circ\pr})
\qeq
\id_{\sigma\sthcomp\rho}
\zbox.
\]

Now, given four positive morphisms organized as

\[
\begin{array}{l}
\rho \xto{F} \rho' \xto{F'} \rho'' \in \Thin(\cA,\cB)\,,\\
\sigma \xto{G} \sigma' \xto{G'} \sigma'' \in \Thin(\cB,\cC)\,,
\end{array}
\]

the procedure to compute $F \sthcomp G$ gives us $\stsupp H,H^l$
and $H^r$ s.t.

\[
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pl"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^l}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"]
\\
\rho
\ar[r,"\stsupp F"{description}]
\ar[d,"\stdisp\rho_B"']
\cphar[rd,"\xTo{F^B}"]
\rho'
\ar[d,"\stdisp{\rho'}_B"]
\\
\ar[r,equals]
\end{tikzcd}
\qeq
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pr"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^r}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"]
\\
\sigma
\ar[r,"\stsupp G"{description}]
\ar[d,"\stdisp\sigma_B"']
\cphar[rd,"\xTo{G^B}"]
\sigma'
\ar[d,"\stdisp{\sigma'}_B"]
\\
\ar[r,equals]
\end{tikzcd}
\]

and with $\stdisp{\rho'}_A H^l$ and $\stdisp{\sigma'}_C H^r$ respectively
negative on $\cA$ and positive on $\cC$; similarly, the procedure to compute
$F' \sthcomp G'$ gives us $\stsupp{H'},H'^l$ and $H'^r$ such that

\[
\begin{tikzcd}
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"']
\ar[r,"\stsupp {H'}",myname=F]
\cphar[rd,"\xTo{H'^l}"]
\stsupp{\sigma''\sthcomp\rho''}
\ar[d,"\pl"]
\\
\rho'
\ar[d,"\stdisp{\rho'}_B"']
\ar[r,"\stsupp {F'}"{description}]
\cphar[rd,"\xTo{F'^B}"]
\rho''
\ar[d,"\stdisp{\rho''}_B"]
\\
\ar[r,equals]
\end{tikzcd}
\qeq
\begin{tikzcd}
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"']
\ar[r,"\stsupp {H'}",myname=F]
\cphar[rd,"\xTo{H'^r}"]
\stsupp{\sigma''\sthcomp\rho''}
\ar[d,"\pr"]
\\
\sigma'
\ar[d,"\stdisp{\sigma'}_B"']
\ar[r,"\stsupp {G'}"{description}]
\cphar[rd,"\xTo{G'^B}"]
\sigma''
\ar[d,"\stdisp{\sigma''}_B"]
\\
\ar[r,equals]
\end{tikzcd}
\]

and with $\stdisp{\rho''}_A H'^l$ and $\stdisp{\sigma''}_C H'^r$ respectively
negative on $\cA$ and positive on $\cC$. On the one hand, we thus have that
$(G' \sthc F') \circ (G \sthc F)$ is the span morphism $K = (\stsupp
K,K^l,K^r)$ with $\stsupp K = \stsupp {H'} \stsupp H$ and

\begin{gather*}
\begin{tikzcd}[ampersand replacement=\&]
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pl"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^l}"]
\&
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"{description}]
\ar[r,"\stsupp {H'}",myname=F]
\cphar[rd,"\xTo{H'^l}"]
\&
\stsupp{\sigma''\sthcomp\rho''}
\ar[d,"\pl"]
\\
\rho
\ar[r,"\stsupp F"{description}]
\ar[d,"\stdisp\rho_A"']
\cphar[rd,"\xTo{F^A}"]
\&
\rho'
\ar[d,"\stdisp{\rho'}_A"{description}]
\ar[r,"\stsupp {F'}"{description}]
\cphar[rd,"\xTo{F'^A}"]
\&
\rho''
\ar[d,"\stdisp{\rho''}_A"]
\\
\ar[r,equals]
\&
\ar[r,equals]
\&
\end{tikzcd}
\\
\begin{tikzcd}[ampersand replacement=\&]
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pr"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^r}"]
\&
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"{description}]
\ar[r,"\stsupp {H'}",myname=F]
\cphar[rd,"\xTo{H'^r}"]
\&
\stsupp{\sigma''\sthcomp\rho''}
\ar[d,"\pr"]
\\
\sigma
\ar[r,"\stsupp G"{description}]
\ar[d,"\stdisp\sigma_C"']
\cphar[rd,"\xTo{G^C}"]
\&
\sigma'
\ar[d,"\stdisp{\sigma'}_C"{description}]
\ar[r,"\stsupp {G'}"{description}]
\cphar[rd,"\xTo{G'^C}"]
\&
\sigma''
\ar[d,"\stdisp{\sigma''}_C"]
\\
\ar[r,equals]
\&
\ar[r,equals]
\&
\end{tikzcd}
\zbox.
\end{gather*}

On the other hand, we have

\[
\begin{array}{rc}
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pl"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^l}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pl"{description}]
\ar[r,"\stsupp {H'}",myname=F]
\cphar[rd,"\xTo{H'^l}"]
\stsupp{\sigma''\sthcomp\rho''}
\ar[d,"\pl"]
\\
\rho
\ar[r,"\stsupp F"{description}]
\ar[d,"\stdisp\rho_B"']
\cphar[rd,"\xTo{F^B}"]
\rho'
\ar[d,"\stdisp{\rho'}_B"{description}]
\ar[r,"\stsupp {F'}"{description}]
\cphar[rd,"\xTo{F'^B}"]
\rho''
\ar[d,"\stdisp{\rho''}_B"]
\\
\ar[r,equals]
\ar[r,equals]
\end{tikzcd}
\\
\begin{tikzcd}
\stsupp{\sigma\sthcomp\rho}
\ar[d,"\pr"']
\ar[r,"\stsupp H",myname=F]
\cphar[rd,"\xTo{H^r}"]
\stsupp{\sigma'\sthcomp\rho'}
\ar[d,"\pr"{description}]
\ar[r,"\stsupp {H'}",myname=F]
\cphar[rd,"\xTo{H'^r}"]
\stsupp{\sigma''\sthcomp\rho''}
\ar[d,"\pr"]
\\
\sigma
\ar[r,"\stsupp G"{description}]
\ar[d,"\stdisp\sigma_B"']
\cphar[rd,"\xTo{G^B}"]
\sigma'
\ar[d,"\stdisp{\sigma'}_B"{description}]
\ar[r,"\stsupp {G'}"{description}]
\cphar[rd,"\xTo{G'^B}"]
\sigma''
\ar[d,"\stdisp{\sigma''}_B"]
\\
\ar[r,equals]
\ar[r,equals]
\end{tikzcd}
\zbox.
\end{array}
\]

Moreover, the two natural transformations obtained as the horizontal pasting
of $H^l$ and $H'^l$ along $\pl$ and the horizontal pasting of $H^r$ and $H'^r$
along $\pr$ satisfy the polarity condition of the .

Hence, by considering again the diagrammatic definition of $K$, the tells
us that $K$ is also $(G' \circ G) \sthc (F' \circ F)$, which concludes functoriality.

We now show the unitality of the horizontal composition. Given a thin
groupoid $A$, we write $\stid A$ for the identity span $A \xot{\id_A} A
\xto{\id_A}$. We have

Given a thin groupoid $\cA$, we have $\stid\cA \in \T_{\cA \lin \cA}$.

This is an easy consequence of <Ref> and

We also write $\stid\cA$ for the corresponding functor $\termcat \to
\Thin(\cA,\cA)$. Given an additional thin groupoid $\cB$, there is a
transformation $\stru$ between the functors

\begin{gather*}
\Thin(\cA,\cB)
\xto{\sim}
\Thin(\cA,\cB) \times \termcat
\to \cdots
\\
\xto{\unit{} \times \stid\cA}
\Thin(\cA,\cB) \times \Thin(\cA,\cA)
\xto{(-)\sthcomp(-)}
\Thin(\cA,\cB)
\end{gather*}

\[
\Thin(\cA,\cB)
\xto{\unit{}}
\Thin(\cA,\cB)
\]

whose component at $\sigma \in \Thin(\cA,\cB)$ is defined as
follows. Recall that the span $\sigma \sthcomp \stid\cA$ is defined by the

\[
\begin{tikzcd}[cs={5em,between origins}]
\stsupp {\sigma \sthcomp \stid\cA}
\ar[dl,"\pl"']
\ar[dr,"\pr"]
\ar[dd,phantom,very near start,"\dcorner"]
\\
\ar[dr,"\unit A"{description}]
\ar[dl,"\unit A"{description}]
\stsupp \sigma
\ar[dl,"{\stdisp[A]\sigma}"'{description}]
\ar[dr,"{\stdisp[B]\sigma}"{description}]
\\
\end{tikzcd}
\zbox.
\]

Then, $\stsupp{\stru_\sigma} \defeq \pr$ is an isomorphism (as the pullback of
an isomorphism) which moreover induces a strong isomorphism of strategies
$\stru_\sigma \co \sigma \sthcomp \stid\cA \To \sigma \in \Thin$.

$\stru \defeq (\stru_\sigma)_{\sigma \in \Thin}$ is a natural isomorphism.

Let $\cA,\cB$, $\sigma,\sigma'\co \cA \stto \cB$ and $F \co \sigma \to
\sigma'$ in $\Thin(\cA,\cB)$. We first picture the two compositions $\tau \defeq \stid\cA
\sthcomp \sigma$ and $\tau' \defeq \stid\cA \sthcomp \sigma'$ on the diagram

\[
\begin{tikzcd}[rsbo=large,csbo=large]
\stsupp\tau
\ar[dd,phantom,very near start,"\dcorner"]
\ar[ld,dashed,"\pl^\tau"']
\ar[rd,dashed,"\pr^\tau"]
\\
\ar[ld,"\unit A"{description}]
\ar[rd,"\unit A"{description}]
\stsupp\sigma
\ar[ld,"\stdisp{\sigma}_A"{description}]
\ar[rd,"\stdisp{\sigma}_B"{description}]
\\
\\
\ar[lu,"\unit A"{description}]
\ar[ru,"\unit A"{description}]
\stsupp{\sigma'}
\ar[lu,"\stdisp{\sigma'}_A"{description}]
\ar[ru,"\stdisp{\sigma'}_B"{description}]
\\
\stsupp{\tau'}
\ar[uu,phantom,very near start,"\ucorner"]
\ar[lu,dashed,"\pl^{\tau'}"]
\ar[ru,dashed,"\pr^{\tau'}"']
\end{tikzcd}
\zbox.
\]

We now compute the composition $F \sthcomp \unit{\stid\cA}$.
By the , it is the morphism $\tilde F \co \sigma \sthc \stid\cA \To
\sigma' \sthc \stid\cA$ defined by

\[
\stsupp{\tilde F}
\qeq
\stsupp{\tau}
\xto{\pr^\tau}
\stsupp\sigma
\xto{\stsupp F}
\stsupp{\sigma'}
\xto{\finv{(\pr^{\tau'})}}
\stsupp{\tau'}
\]

\begin{gather*}
\tilde F^A
\begin{tikzcd}[ampersand replacement=\&]
\stsupp{\tau}
\ar[d,"\pl^\tau"']
\ar[r,"\pr^\tau"]
\cphar[rd,"="]
\&
\stsupp\sigma
\ar[d,"\stdisp\sigma_A"{description}]
\ar[r,"\stsupp F"]
\cphar[rd,"\xTo{F^A}"]
\&
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_A"{description}]
\ar[r,"\finv{(\pr^{\tau'})}"]
\cphar[rd,"="]
\&
\stsupp{\tau'}
\ar[d,"\pl^{\tau'}"]
\\
\ar[d,"\unit A"']
\ar[r,equals]
\cphar[rd,"="]
\&
\ar[d,"\unit A"{description}]
\ar[r,equals]
\cphar[rd,"="]
\&
\ar[d,"\unit A"{description}]
\ar[r,equals]
\cphar[rd,"="]
\&
\ar[d,"\unit A"]
\\
\ar[r,equals]
\&
\ar[r,equals]
\&
\ar[r,equals]
\&
\end{tikzcd}
\\
\tilde F^B
\begin{tikzcd}[ampersand replacement=\&]
\stsupp{\tau}
\ar[d,"\pr^\tau"']
\ar[r,"\pr^\tau"]
% \cphar[rd,"="]
\cphar[rrrd,"="]
\&
\stsupp\sigma
% \ar[d,"\stdisp\sigma_A"{description}]
\ar[r,"\stsupp F"]
% \cphar[rd,"\xTo{F^A}"]
\&
\stsupp{\sigma'}
% \ar[d,"\stdisp{\sigma'}_A"{description}]
\ar[r,"\finv{(\pr^{\tau'})}"]
% \cphar[rd,"="]
\&
\stsupp{\tau'}
\ar[d,"\pr^{\tau'}"]
\\
\stsupp\sigma
\ar[d,"\stdisp\sigma_B"']
\ar[rrr,"\stsupp F"{description}]
\cphar[rrrd,"\xTo{F^B}"]
\&
\&
\&
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_B"]
\\
\ar[rrr,equals]
\&
\&
\&
\end{tikzcd}
\zbox.
\end{gather*}

The naturality of $\stru$ is then expressed by the equation

\[
\stru_{\sigma'} \circ (F \sthc \unit{\stid\cA}) = F \circ \stru_\sigma
\]

that we now check. We first have

\[
\stsupp{\stru_{\sigma'} \circ (F \sthc \unit{\stid\cA})}
\qeq
\stsupp{\tau}
\xto{\pr^\tau}
\stsupp\sigma
\xto{\stsupp F}
\stsupp{\sigma'}
\qeq
\stsupp{F \circ \stru_\sigma}
\zbox.
\]

\[
\begin{array}{ccc}
(\stru_{\sigma'} \circ (F \sthc \unit{\stid\cA}))^A
\begin{tikzcd}
\stsupp{\tau}
\ar[d,"\pl^\tau"']
\ar[r,"\pr^\tau"]
\cphar[rd,"="]
\stsupp\sigma
\ar[d,"\stdisp\sigma_A"{description}]
\ar[r,"\stsupp F"]
\cphar[rd,"\xTo{F^A}"]
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_A"]
\\
\ar[d,"\unit A"']
\ar[r,equals]
\cphar[rd,"="]
\ar[d,"\unit A"{description}]
\ar[r,equals]
\cphar[rd,"="]
\ar[d,"\unit A"]
\\
\ar[r,equals]
\ar[r,equals]
\end{tikzcd}
\\[5em]
(F \circ \stru_\sigma)^A
\end{array}
\]

\[
\begin{array}{ccc}
(\stru_{\sigma'} \circ (F \sthc \unit{\stid\cA}))^B
\begin{tikzcd}
\stsupp{\tau}
\ar[d,"\pr^\tau"']
\ar[r,"\pr^\tau"]
% \cphar[rd,"="]
\cphar[rrd,"="]
\stsupp\sigma
% \ar[d,"\stdisp\sigma_A"{description}]
\ar[r,"\stsupp F"]
% \cphar[rd,"\xTo{F^A}"]
\stsupp{\sigma'}
\ar[d,equals]
\\
\stsupp\sigma
\ar[d,"\stdisp\sigma_B"']
\ar[rr,"\stsupp F"{description}]
\cphar[rrd,"\xTo{F^B}"]
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_B"]
\\
\ar[rr,equals]
\end{tikzcd}
\\[5em]
(F \circ \stru_\sigma)^B
\zbox.
\end{array}
\]

Which concludes the proof that $\stru$ defines a natural iso.

Similarly, there is a transformation $\stlu$ between

\begin{gather*}
\Thin(\cA,\cB)
\xto{\sim}
\termcat \times \Thin(\cA,\cB)
\to\cdots
\\
\xto{\stid\cB \times \unit{}}
\Thin(\cB,\cB) \times \Thin(\cA,\cB)
\xto{(-)\sthcomp(-)}
\Thin(\cA,\cB)
\end{gather*}

\[
\Thin(\cA,\cB)
\xto{\unit{}}
\Thin(\cA,\cB)
\]

whose component at a strategy $\sigma \in \Thin(\cA,\cB)$ is defined as
follows. Recall that the span $\stid\cB \sthcomp \sigma$ is defined by the

\[
\begin{tikzcd}[cs={5em,between origins}]
\stsupp {\stid\cB \sthcomp \sigma}
\ar[dl,"\pl"']
\ar[dr,"\pr"]
\ar[dd,phantom,very near start,"\dcorner"]
\\
\stsupp\sigma
\ar[dr,"\stdisp\sigma_B"{description}]
\ar[dl,"\stdisp\sigma_A"{description}]
\ar[dl,"{\unit B}"'{description}]
\ar[dr,"{\unit B}"{description}]
\\
\end{tikzcd}
\zbox.
\]

Then, $\stsupp{\stlu_\sigma} \defeq \pl$ is an isomorphism (as the pullback of
an isomorphism) which moreover induces a strong isomorphism of thin spans
$\stlu_\sigma \co \stid\cB \sthcomp \sigma \To \sigma \in \Thin$. As before, we have

$\stlu \defeq (\stlu_\sigma)_{\sigma \in \Thin}$ is a natural isomorphism.

Given thin groupoids $\cA,\cB,\cC,\cD$, there is a transformation

\begin{gather*}
\stass \co ((-)\sthcomp(-))\sthcomp(-) \To (-)\sthcomp((-)\sthcomp(-))
\\
\co \Thin(\cC,\cD) \times \Thin(\cB,\cC) \times \Thin(\cA,\cB)
\\
\to \Thin(\cA,\cD)
\end{gather*}

whose component at $\sigma \in \Thin(\cA,\cB)$, $\tau\in \Thin(\cB,\cC)$ and
$\upsilon\in \Thin(\cC,\cD)$ is given by a strong morphism

\[
\stass_{\sigma , \tau , \ups} \co (\ups \sthcomp \tau) \sthcomp \sigma \to \upsilon \sthcomp (\tau
\sthcomp \sigma)
\]

defined as expected between the two compositions using the different pullbacks
involved, as in

\[
\begin{tikzcd}[csbo=3em,rsbo=2em]
\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}
\phar[dd,very near start,"\dcorner"]
\ar[rd,"\pr^{(\ups\sthcomp\tau)\sthcomp\sigma}"]
\ar[lldd,"\pl^{(\ups\sthcomp\tau)\sthcomp\sigma}"']
\ar[dddddd,"\stsupp{\stass_{\sigma,\tau,\ups}}"'{description},bend left=80,looseness=2.5]
\\
\stsupp{\ups\sthcomp\tau}
\phar[dd,very near start,"\dcorner"]
\ar[ld,"\pl^{\ups\sthcomp\tau}"']
\ar[rd,"\pr^{\ups\sthcomp\tau}"]
\\
\stsupp\sigma
\ar[ld]
\ar[rd]
\stsupp\tau
\ar[ld]
\ar[rd]
\stsupp\ups
\ar[ld]
\ar[rd]
\\
\\
\stsupp\sigma
\ar[lu]
\ar[ru]
\stsupp\tau
\ar[lu]
\ar[ru]
\stsupp\ups
\ar[lu]
\ar[ru]
\\
\stsupp{\tau\sthcomp\sigma}
\phar[uu,very near start,"\ucorner"]
\ar[lu,"\pl^{\tau\sthcomp\sigma}"]
\ar[ru,"\pr^{\tau\sthcomp\sigma}"']
\\
\stsupp{\ups\sthcomp(\tau\sthcomp\sigma)}
\phar[uu,very near start,"\ucorner"]
\ar[lu,"\pl^{\ups\sthcomp(\tau\sthcomp\sigma)}"]
\ar[rruu,"\pr^{\ups\sthcomp(\tau\sthcomp\sigma)}"']
\end{tikzcd}
\zbox.
\]

An inverse for $\stass_{\sigma,\tau,\ups}$ is defined symmetrically, so that $\stass$ is
an isomorphic transformation.

The transformation $\stass$ is a natural isomorphism.

Let $F \co \sigma \To \sigma' \co \cA \stto \cB$, $G \co \tau \To \tau' \co
\cB \stto \cC$ and $H \co \ups \To \ups' \co \cC \stto \cD$ be weak morphisms
in $\Thin$. We compute $(\ups \sthcomp \tau) \sthcomp \sigma$ as usual but
moreover factor the projection $\pl^{(\ups \sthcomp \tau) \sthcomp \sigma}$
canonically through $\stsupp{\tau \sthcomp \sigma}$ by a unique morphism
$\tilde\pl^{(\ups \sthcomp \tau) \sthcomp \sigma}$ so that we get a diagram

\[
\begin{tikzcd}[csbo=3.5em,rsbo=2em]
\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}
\phar[dd,very near start,"\dcorner"]
\ar[ld,"\tilde\pl^{(\ups \sthcomp \tau) \sthcomp \sigma}"']
\ar[rd]
\\
\stsupp{\tau\sthcomp\sigma}
\phar[dd,very near start,"\dcorner"]
\ar[ld]
\ar[rd]
\stsupp{\ups\sthcomp\tau}
\phar[dd,very near start,"\dcorner"]
\ar[ld]
\ar[rd]
\\
\stsupp\sigma
\ar[ld]
\ar[rd]
\stsupp\tau
\ar[ld]
\ar[rd]
\stsupp\ups
\ar[ld]
\ar[rd]
\\
\end{tikzcd}
\]

and we get a similar diagram for $\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}$.
Symmetrically, the projection $\pr^{\ups \sthcomp (\tau \sthcomp \sigma)}$ can
be factored canonically through $\stsupp{\ups\sthc\tau}$ by a morphism $\tilde
\pr^{\ups \sthcomp (\tau \sthcomp \sigma)}$, and the projection $\pr^{\ups'
\sthcomp (\tau' \sthcomp \sigma')}$ through $\stsupp{\ups'\sthc\tau'}$ by a
morphism $\tilde \pr^{\ups' \sthcomp (\tau' \sthcomp \sigma')}$. Note that
$\pl^{\ups\sthc(\tau\sthc\sigma)} \circ \stsupp{\stass_{\sigma,\tau,\ups}} =
\tilde\pl^{(\ups\sthc\tau)\sthc\sigma}$ and other similar equalities hold. By
computing $K \defeq G \sthcomp F$, we get natural transformations $\tilde K^A$
and $\tilde K^C$ such that

\begin{gather*}
\begin{tikzcd}[column sep=small,ampersand replacement=\&]
\stsupp{\tau \sthcomp \sigma}
\ar[r,"\stsupp K",myname=Garr]
\ar[d,"\pl^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde K^A}"]
\&
\stsupp{\tau' \sthcomp \sigma'}
\ar[d,"\pl^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\sigma
\ar[d,"\stdisp\sigma_A"{description}]
\ar[r,"\stsupp F"{description},myname=mididA]
\cphar[rd,"\xTo{F^A}"]
\&
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_A"{description}]
\\
\ar[r,equals]
\&
\end{tikzcd}
\shortintertext{and}
\begin{tikzcd}[column sep=small,ampersand replacement=\&]
\stsupp{\tau \sthcomp \sigma}
\ar[r,"\stsupp K",myname=Garr]
\ar[d,"\pr^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde K^C}"]
\&
\stsupp{\tau' \sthcomp \sigma'}
\ar[d,"\pr^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\tau
\ar[d,"\stdisp\tau_C"{description}]
\ar[r,"\stsupp G"{description},myname=mididA]
\cphar[rd,"\xTo{G^C}"]
\&
\stsupp{\tau'}
\ar[d,"\stdisp{\tau'}_C"{description}]
\\
\ar[r,equals]
\&
\end{tikzcd}
\end{gather*}

\[
\]

which satisfy moreover that

\[
\begin{tikzcd}[column sep=small]
\stsupp{\tau \sthcomp \sigma}
\ar[r,"\stsupp K",myname=Garr]
\ar[d,"\pl^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde K^A}"]
\stsupp{\tau' \sthcomp \sigma'}
\ar[d,"\pl^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\sigma
\ar[d,"\stdisp\sigma_B"{description}]
\ar[r,"\stsupp F"{description},myname=mididA]
\cphar[rd,"\xTo{F^B}"]
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_B"{description}]
\\
\ar[r,equals]
\end{tikzcd}
\begin{tikzcd}[column sep=small]
\stsupp{\tau \sthcomp \sigma}
\ar[r,"\stsupp K",myname=Garr]
\ar[d,"\pr^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde K^C}"]
\stsupp{\tau' \sthcomp \sigma'}
\ar[d,"\pr^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\tau
\ar[d,"\stdisp\tau_B"{description}]
\ar[r,"\stsupp G"{description},myname=mididA]
\cphar[rd,"\xTo{G^B}"]
\stsupp{\tau'}
\ar[d,"\stdisp{\tau'}_B"{description}]
\\
\ar[r,equals]
\end{tikzcd}
\zbox.
\]

Similarly, by computing $L \defeq H \sthcomp G$, we get natural
transformations $\tilde L^B$ and $\tilde L^D$ such that

\begin{gather*}
\begin{tikzcd}[column sep=small,ampersand replacement=\&]
\stsupp{\ups \sthcomp \tau}
\ar[r,"\stsupp L",myname=Garr]
\ar[d,"\pl^{\ups\sthcomp\tau}"']
\cphar[rd,"\xTo{\tilde L^B}"]
\&
\stsupp{\ups' \sthcomp \tau'}
\ar[d,"\pl^{\ups'\sthcomp\tau'}"]
\\
\stsupp\tau
\ar[d,"\stdisp\tau_B"{description}]
\ar[r,"\stsupp G"{description},myname=mididB]
\cphar[rd,"\xTo{G^B}"]
\&
\stsupp{\tau'}
\ar[d,"\stdisp{\tau'}_B"{description}]
\\
\ar[r,equals]
\&
\end{tikzcd}
\shortintertext{and}
\begin{tikzcd}[column sep=small,ampersand replacement=\&]
\stsupp{\ups \sthcomp \tau}
\ar[r,"\stsupp L",myname=Garr]
\ar[d,"\pr^{\ups\sthcomp\tau}"']
\cphar[rd,"\xTo{\tilde L^D}"]
\&
\stsupp{\ups' \sthcomp \tau'}
\ar[d,"\pr^{\ups'\sthcomp\tau'}"]
\\
\stsupp\ups
\ar[d,"\stdisp\ups_D"{description}]
\ar[r,"H"{description},myname=mididB]
\cphar[rd,"\xTo{H^D}"]
\&
\stsupp{\ups'}
\ar[d,"\stdisp{\ups'}_D"{description}]
\\
\ar[r,equals]
\&
\end{tikzcd}
\end{gather*}

which satisfy moreover that

\[
\begin{tikzcd}[column sep=small]
\stsupp{\ups \sthcomp \tau}
\ar[r,"\stsupp L",myname=Garr]
\ar[d,"\pl^{\ups\sthcomp\tau}"']
\cphar[rd,"\xTo{\tilde L^B}"]
\stsupp{\ups' \sthcomp \tau'}
\ar[d,"\pl^{\ups'\sthcomp\tau'}"]
\\
\stsupp\tau
\ar[d,"\stdisp\tau_C"{description}]
\ar[r,"\stsupp G"{description},myname=mididB]
\cphar[rd,"\xTo{G^C}"]
\stsupp{\tau'}
\ar[d,"\stdisp{\tau'}_C"{description}]
\\
\ar[r,equals]
\end{tikzcd}
\begin{tikzcd}[column sep=small]
\stsupp{\ups \sthcomp \tau}
\ar[r,"\stsupp L",myname=Garr]
\ar[d,"\pr^{\ups\sthcomp\tau}"']
\cphar[rd,"\xTo{\tilde L^D}"]
\stsupp{\ups' \sthcomp \tau'}
\ar[d,"\pr^{\ups'\sthcomp\tau'}"]
\\
\stsupp\ups
\ar[d,"\stdisp\ups_C"{description}]
\ar[r,"\stsupp H"{description},myname=mididB]
\cphar[rd,"\xTo{H^C}"]
\stsupp{\ups'}
\ar[d,"\stdisp{\ups'}_C"{description}]
\\
\ar[r,equals]
\end{tikzcd}
\zbox.
\]

\[
\begin{tikzcd}[column sep={4em,between origins},row sep={3em,between origins}]
\stsupp{(\ups'\sthcomp\tau')\sthcomp\sigma'}
\phar[dd,very near start,"\dcorner"]
\ar[rd,"\pr^{(\ups' \sthcomp \tau') \sthcomp \sigma'}"]
\ar[ld,"\tilde\pl^{(\ups' \sthcomp \tau') \sthcomp \sigma'}"']
\\
\stsupp{\tau'\sthcomp\sigma'}
\ar[rd,"\pr^{\tau'\sthcomp\sigma'}"']
\stsupp{\ups'\sthc\tau'}
\ar[ld,"\pl^{\ups'\sthc\tau'}"]
\\
\stsupp{\tau'}
\end{tikzcd}
\]

is a bipullback by <Ref>, and that the
natural transformations $\tilde K^C$ and $\tilde L^B$ define a pseudocone of
vertex $\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}$ on the associated cospan,
we get $\stsupp M$, $\tilde M^A$ and $\tilde M^D$ such that

\[
\begin{array}{cc}
\begin{tikzcd}[column sep=small]
\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}
\ar[r,"\stsupp M"]
\ar[d,"\tilde\pl^{(\ups \sthcomp \tau) \sthcomp \sigma}"']
\cphar[rd,"\xTo{\tilde M^A}"]
\stsupp{(\ups'\sthcomp\tau')\sthcomp\sigma'}
\ar[d,"\tilde\pl^{(\ups' \sthcomp \tau') \sthcomp \sigma'}"]
\\
\stsupp{\tau \sthcomp \sigma}
\ar[r,"\stsupp K"{description},myname=Garr]
\ar[d,"\pr^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde K^C}"]
\stsupp{\tau' \sthcomp \sigma'}
\ar[d,"\pr^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\tau
\ar[r,"\stsupp G"{description},myname=mididA]
\stsupp{\tau'}
\end{tikzcd}
\\
\begin{tikzcd}[column sep=small]
\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}
\ar[r,"\stsupp M"]
\ar[d,"\pr^{(\ups \sthcomp \tau) \sthcomp \sigma}"']
\cphar[rd,"\xTo{\tilde M^D}"]
\stsupp{(\ups'\sthcomp\tau')\sthcomp\sigma'}
\ar[d,"\pr^{(\ups' \sthcomp \tau') \sthcomp \sigma'}"]
\\
\stsupp{\ups\sthcomp\tau}
\ar[r,"\stsupp L"{description},myname=Garr]
\ar[d,"\pr^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde L^B}"]
\stsupp{\ups'\sthcomp\tau'}
\ar[d,"\pr^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\tau
\ar[r,"\stsupp G"{description},myname=mididA]
\stsupp{\tau'}
\end{tikzcd}
\zbox.
\end{array}
\]

We thus get a weak morphism $M = (\stsupp M,M^A,M^D)$ between
$(\ups\sthcomp\tau)\sthcomp\sigma$ and $(\ups'\sthcomp\tau')\sthcomp\sigma'$
in $\Span$, where

\begin{gather*}
\begin{tikzcd}[column sep=small,ampersand replacement=\&]
\stsupp{(\ups\sthcomp\tau)\sthcomp\sigma}
\ar[r,"\stsupp M"]
\ar[d,"\tilde\pl^{(\ups \sthcomp \tau) \sthcomp \sigma}"']
\cphar[rd,"\xTo{\tilde M^A}"]
\&
\stsupp{(\ups'\sthcomp\tau')\sthcomp\sigma'}
\ar[d,"\tilde\pl^{(\ups' \sthcomp \tau') \sthcomp \sigma'}"]
\\
\stsupp{\tau \sthcomp \sigma}
\ar[r,"\stsupp K"{description},myname=Garr]
\ar[d,"\pl^{\tau\sthcomp\sigma}"']
\cphar[rd,"\xTo{\tilde K^A}"]
\&
\stsupp{\tau' \sthcomp \sigma'}
\ar[d,"\pl^{\tau'\sthcomp\sigma'}"]
\\
\stsupp\sigma
\ar[d,"\stdisp\sigma_A"{description}]
\ar[r,"\stsupp F"{description},myname=mididA]
\cphar[rd,"\xTo{F^A}"]
\&
\stsupp{\sigma'}
\ar[d,"\stdisp{\sigma'}_A"{description}]
\\
\ar[r,equals]
\&
\end{tikzcd}
\shortintertext{and}
\begin{tikzcd}[column sep=small,ampersand replacement=\&]