# On strict extensional reflexivity
in compact closed categories

Peter Hines

###### Abstract

This article has two related aims. The first is to study the categorical
setting of Abramsky, Haghverdi, & Scott’s untyped linear combinatory algebras
[6], and the second is to relate this to the much more recent work by Abramsky
& Heunen on Frobenius algebras in the infinitary setting [7]. The key to this
is (extensional) reflexivity (i.e. the property of an object being isomorphic
to its own internal hom $R\cong[R\rightarrow R]$). We first characterise
extensionally reflexive objects in compact closed categories, then consider
when & how this property may be ‘strictified’ – how we may give a monoidally
equivalent category where the isomorphisms exhibiting reflexivity are in fact
identity arrows. This results in small two-object compact closed categories
consisting of a unit object and a single (non-unit) strictly reflexive object.
We then move on to studying the endomorphism monoids of such objects from an
algebraic rather than logical or categorical viewpoint. We demonstrate that
these necessarily contain an interesting inverse monoid that may be thought of
as Richard Thompson’s iconic group $\mathcal{F}$ together with the equally
iconic bicyclic monoid $\mathcal{B}$ of semigroup theory, with non-trivial
interactions between the two derived from the Frobenius algebra identity – and
claim this as a particularly significant example of the (unitless) Frobenius
algebras of [7].
We first develop the theory from a purely theoretical point of view, then move
on to develop concrete examples, based on the algebra and category theory
behind [21, 22, 6]. The concrete examples we give are based on the traced
monoidal category of partial injections, and reflexive objects in the compact
closed category that results from applying the ${\bf Int}$ or ${\bf GoI}$
construction. We then give compact closed categories, monoidally equivalent to
compact closed subcategories of $\bf Int(pInj)$, where this reflexivity is
exhibited by identity arrows, and show how the above algebraic structures
(Thompson’s $\mathcal{F}$, the bicyclic monoid, and Frobenius algebras) arise
in a fundamental manner.

This work is of course !( ) dedicated to Samson Abramsky.

##  1 Historical background

The starting point for this chapter is Girard’s Geometry of Interaction
program – in particular the first two parts. It is by now well-established
that compact closed categories model key aspects of this (see [6, 25] for a
good account), and this observation motivated the name of Abramsky’s
categorical $\bf GoI$ construction [1] (see Section 7).

However, this immediately poses an interesting puzzle. In [21], Girard makes
the rather cryptic comment that his system ‘forgets types’, even though the
stated aim was to produce a model of the polymorphically typed System
$\mathcal{F}$, rather than a purely untyped system. The explanation seems to
be that the GoI system moves from a rigidly typed system to an entirely
untyped system, in order to build a more flexible (polymorphic) type system on
top of this111This is commonly studied via has become known as Hyland-Ong
types [36]. E. Haghverdi & P. Scott also presented a Geometry of Interaction
system that is decidedly typed in [25]; however, this current chapter
concentrates on the purely untyped aspects of the Geometry of Interaction
program, and (re-)introducing types would be a non-trivial subsequent step..
The claim that there is an untyped logical system at the core of Girard’s GOI
was borne out in Abramsky, Haghverdi, and Scott’s paper [6] that gave an
untyped combinatory logic (precisely, linear-exponential combinatory logic)
based on the primitives from Girard’s first two Geometry of Interaction papers
[21, 22].

It is natural to wish to study this type-freeness via the ‘objects as types’
paradigm of categorical logic [44]. In the classical / Cartesian world, Lambek
& Scott introduced, as models of untyped lambda calculus, the $C$-monoids of
[44], which may reasonably be viewed as monoids satisfying all of the axioms
for Cartesian closure apart from the existence of a terminal object222The
complete situation is slightly more subtle than this description suggests.
There is a good case that C-monoids do indeed account for units, but these are
implicit – a passage to the Karoubi envelope then makes them explicit. This is
beyond the scope of this paper, but covered in [44]..

Based on similar ideas, analogues of compact closure within monoids were
studied in [26, 27] (again motivated by J.-Y. Girard’s first three Geometry of
Interaction papers [21, 22, 23]) and the claim was made that certain monoids
derived from the GOI program satisfy, ‘unitless analogues of compact closure’.
This work was carried out independently of [6]; however, the underlying
algebraic structures – based on Girard’s original system – are identical.

There are significant subtleties associated with this claim333To complicate
matters, the axiomatisation in [27] work was intended & stated to be
equivalent to that of [26]. Unfortunately, as recently pointed out by C.
Heunen, several severe typo.s made their way into the final published version
– this axiomatisation, at least, unambiguously does not capture compact
closure!. With Cartesian closure, we are left with the essential concepts even
without the terminal object. The same – at least for the usual axiomatisation
– does not apply to compact closure.

##  2 Compact closure

In [41], the abstract 2-categorical definition of a compact closed category is
shown to have a concrete characterisation in terms of the existence of a
duality and distinguished arrows. It is by now standard to take this as
fundamental.

######  Definition 1.

A symmetric monoidal category $({\mathcal{C}},\otimes,\sigma_{\\_,\\_},I)$ is
compact closed when it is equipped with :

  * •

a dual – a contravariant monoidal functor
$(\\_)^{*}:{\mathcal{C}}^{op}\rightarrow{\mathcal{C}}$ satisfying
$\left((\\_)^{*}\right)^{*}=Id_{\mathcal{C}}$

  * •

for all objects $A\in Ob(\mathcal{C})$, distinguished unit & co-unit arrows
$\eta_{A}:I\rightarrow A\otimes A^{*}$ and $\epsilon_{A}:A^{*}\otimes
A\rightarrow I$ that satisfy the yanking axiom

$(1_{A}\otimes\epsilon)(\eta\otimes 1_{A})\ =\ 1_{A}\ =\
(\epsilon_{A^{*}}\otimes 1_{A})(1_{A}\otimes\eta_{A^{*}})$

Using the usual diagrammatic conventions from [38, 39], the unit / co-unit
arrows are drawn as ‘cups’ and ‘caps’

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A^{*}}$
$\textstyle{A^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A}$

giving the yanking axiom as

$\textstyle{A}$$\textstyle{A}$$\textstyle{A}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
= =
$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

######  Remark 2 (Interpretations and Examples).

The neat diagrammatic representation of the unit and co-unit arrows, and
yanking, readily lead to numerous distinct interpretations. One of the
earliest and most natural was for the unit and co-unit arrows to be
interpreted as the Axiom and Cut rules of various forms of linear logic

Axiom : $\frac{}{A\ \ \ A^{\perp}}$ |  Cut : $\frac{A^{\perp}\ \ \ A}{}$
---|---

This is the basis for the close connection between compact closure and the
Geometry of Interaction discussed throughout, and the interpretation of
yanking as cut-elimination is intuitively natural. The concrete examples we
develop in Section 11 onwards are based on Girard’s GoI system, and derived
from the Int or GoI construction described in Section 7.

An alternative interpretation was found in [28, 29], where algebraic models of
dynamics of Turing machines were observed to be compact closed; the unit and
co-unit model the changes of direction of the read-write head of a Turing
machine as it moves over the tape, and the dual corresponds to interchanging
the role of ‘left’ and ‘right’ in the definition of the dynamics.

A further interpretation may be found in the Categorical Quantum Mechanics
program of Abramsky & Coeke [5], where the unit and co-unit respectively
correspond to the production of a maximally entangled state, and a (post-
selected) measurement that results in the observation of this maximally
entangled state.

Numerous other interpretations have been given – in particular, the pregroups
of J. Lambek [43] arise from dropping the requirement of symmetry (implicitly,
considering non-commutative multiplicative linear logic) to give linguistic
models with a distinctly logical flavour. See [12, 13, 43] for the original
motivation from linear logic and the identification as ‘non-symmetric compact
closure’.

###  2.1 On the definition(s) of compact closed monoids

It is not immediate how a compact closed monoid should be defined, apart from
in the highly degenerate case where the unique object is the unit object. In
this setting, we recall the folklore that the subcategory of any monoidal
category generated by its unit object is compact closed, with MacLane’s
distinguished unit arrows & their inverses trivially satisfying the axioms for
the unit / co-unit of compact closure.

With Cartesian closure, we are generally happy to accept that the existence of
a terminal object is a relatively minor part of the definition (and indeed may
even be hidden in the structure of C-monoids – see Footnote 2), and consider
that a Cartesian closed monoid is one satisfying all the other parts of the
definition. By contrast, erasing the unit object from the definition of
compact closure leaves us with nothing – not even the duality (some authors,
notably [40], define the duality in terms of the unit / co-unit arrows).

The approach taken in [26, 27] was to give an axiomatisation of compact
closure for semi-monoidal categories (i.e. categories satisfying all MacLane’s
axioms except for those relating to the unit object – see Definition 17) that

  1. 1.

does not mention the unit, and

  2. 2.

is equivalent to to the usual definition in the presence of a unit.

Regardless of whether the logical interpretation of working without a unit is
desirable, a fundamental question needs to be asked :

> How do we know this definition of unitless compact closure is the ‘correct’
> definition? Is it sufficient for it to reduce to the standard definition in
> the presence of a unit?

Expanding on this question, we may ask what the implications would be of two
such axiomatisations of unitless compact closure that both reduce to the usual
definition in the presence of a unit, but are provably inequivalent? How
should we decide between them?

Such an pair of provably distinct axiomatisations has recently been
established in joint (currently unpublished) work by the author and C. Heunen.
The concrete examples of [26, 27] satisfy both sets of axioms, and the
defining arrows of these axiomatisations correspond in each case to distinct
interesting logical, computational, or categorical features that we would be
unhappy to exclude in the general case; there is simply no reason to prefer
one axiomatisation over the other, and every reason to consider structures
satisfying both axiomatisations.

The existence of concrete examples implies these are compatible, so may follow
from a single set of axioms. However, this illustrates that reduction to the
usual axioms in the presence of a unit is therefore not sufficient. What is
also needed is some notion of completeness – that any other compatible axiom
scheme that is equivalent to compact closure in the presence of a unit is a
consequence of it.

The axioms given in [26] do not have such a ‘completeness’ property and, at
best, cannot be the whole story. The project described above remains ongoing.

##  3 From closed monoids to reflexive objects

Nothing in the above discussion precludes compact closed categories where all
non-unit objects are isomorphic (concrete examples given in part 4. of
Proposition 86), or even (in a small category) identical – giving two-object
compact closed categories, with a single non-unit object: see Corollary 16 and
the concrete examples of Definition 88. However, it is also worthwhile to take
a step back and again ask the obvious question,

> “What was the purpose of Lambek & Scott introducing Cartesian Closed
> Monoids?”

The immediate answer of course is, ‘to model untyped lambda calculus’. Looking
slightly deeper [44] observes that Cartesian closure, combined with the fact
that there is only one object, means that the unique object $c$ is necessarily
isomorphic to its own function space $c^{c}$ (i.e. is a reflexive object), and
this is the key [56] to the unrestricted application & abstraction.

######  Remark 3 (Untyped systems – a change of emphasis).

From a categorical logic ‘objects as types’ perspective, it seems natural that
an ‘untyped version of $\mathcal{X}$’ should be modeled by an
“$\mathcal{X}$–monoid”, provided this can be defined in a satisfactory manner.
When the intention is to model the unrestricted application / abstraction of
an untyped lambda calculus, from precisely the same perspective the notion of
reflexivity is the desirable property. These two concepts – although closely
related – are not identical.

We therefore take as fundamental the notion of objects that are ‘isomorphic to
their own internal hom’. The most general setting in which reflexivity may be
defined is that of the ‘non-monoidal closed categories’ of M. Laplaza [45]
(see Remark 12 for the justification for such a general setting). These are
defined simply as categories with an internal hom functor (i.e. without
explicit reference to any monoidal tensor or adjunction between hom and
tensor) that satisfies some fairly intricate coherence conditions. Laplaza’s
definition, of course, includes the more familiar monoidal closed categories
as a special case.

The following is taken from [56] (see also [35]), although we make some
necessary (see Remark 5) changes in terminology.

######  Definition 4.

Let $({\mathcal{C}},[\\_\rightarrow\\_])$ be a closed category, in the sense
of [45] (this includes monoidal closed categories as a special case).

An (extensionally) reflexive object, or simply reflexive object $R\in
Ob(\mathcal{C})$ is one that is isomorphic to its own internal hom, so
$R\cong[R\rightarrow R]$.

Explicitly, reflexive objects are equipped with mutually inverse isomorphisms
:

  * •

The app isomorphism $\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
6.00006pt}:R\rightarrow[R\rightarrow R]$

  * •

The lam isomorphism $\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
3.99994pt}:[R\rightarrow R]\rightarrow R$

satisfying $\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
3.99994pt}\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip 6.00006pt}=1_{R}$
and $\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
6.00006pt}\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
3.99994pt}=1_{[R\rightarrow R]}$.

We say that $R$ is weakly or intensionally reflexive when $[R\rightarrow R]$
is a retract of $R$, so $\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
6.00006pt}\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
3.99994pt}=1_{[R\rightarrow R]}$, but
$\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
3.99994pt}\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
6.00006pt}=e^{2}=e$ is an idempotent of ${\mathcal{C}}(R,R)$. Note that this
breaks with convention somewhat, by allowing for extensional reflexivity to be
a very special case of weak reflexivity.

Finally, we say a reflexive object is strictly reflexive when
$\vartriangleleft$ $|$ and  $\vartriangleright$ $|$ are identity arrows.
Strictly reflexive objects are of course extensional.

######  Remark 5.

[A conflict of terminology] It is more common (e.g. [35, 56]) to refer to
(extensional) reflexivity as “strict reflexivity”, and to what we call “weak
reflexivity” simply as “reflexivity”. This immediately sets us up for a strong
and probably unavoidable conflict of notation; we are interested in
‘strictifying’ reflexivity in the sense of strictification within categorical
coherence – i.e. giving a suitable equivalence of categories under which the
isomorphisms exhibiting (extensional) reflexivity become identity arrows.

The usage of the term “strict” is very well-established in both fields, so
this conflict of notation is unavoidable – all we can do is point out the
conventions we use!

######  Remark 6 (Weak, strong, & strict reflexivity in models of combinatory
logic).

A key aim of this chapter is to study the categorical / algebraic setting for
the untyped combinatory logic of Abramsky, Haghverdi & Scott, which we claim
is that of strict reflexivity. In some sense, compact closed monoids would be
too extravagant a setting. By contrast to the logical interpretation of [21,
22], the system of [6] has no connectives (& hence no need for tensors), and
no negation (& hence no non-degenerate duality is required)444However, units
do play a rôle in [6], so reflexivity within a setting including these is
essential.; in a $\lambda$ calculus, the key notions are those of application
& abstraction. From that viewpoint, it is appropriate to concentrate on
reflexivity.

However, combinatory logics are ‘lower-level’ systems than $\lambda$ calculii.
The notion of abstraction itself is derived from more primitive operations –
an operation that acts like lambda-abstraction is built up using combinators.
Our claim is that in models of untyped combinatory logic, we will not only
observe reflexivity, but reflexivity that is strict — the isomorphisms that
exhibit reflexivity are identities.

Finally, although reflexivity already features heavily in [6], it is
intensional, or weak, reflexivity. Girard’s original system (implicitly)
considered both – we are therefore ‘plugging a gap’. It is also difficult to
see how reflexivity that is not exhibited by isomorphisms may be strictified,
unless we pass to the Karoubi envelope (i.e. idempotent splitting). This will
then provide reflexive objects that are extensionally reflexive — the setting
we consider.

###  3.1 Reflexive objects of compact closed categories

Reflexive objects of compact closed categories have a particularly simple
characterisation.

######  Definition 7.

Let $(\mathcal{C},\\_\otimes\\_,I)$ be a monoidal category. An object $N\in
Ob({\mathcal{C}})$ is called self-similar or pseudo-idempotent when it
satisfies $N\cong N\otimes N$. The isomorphisms exhibiting this self-
similarity are unique up to unique isomorphism [31], and commonly referred to
as the code and decode arrows
$\mbox{\scalebox{1.2}{$\vartriangleleft$}}\in{\mathcal{C}}(N\otimes N,N)$ and
$\mbox{\scalebox{1.2}{$\vartriangleright$}}\in\mathcal{C}(N,N\otimes N)$
respectively.

Similarly, let $(\mathcal{D},(\\_)^{*})$ be a category with a dual. An object
$S\in Ob({\mathcal{D}})$ is called self-dual when it satisfies $S\cong S^{*}$;
there is no standard notation or terminology for arrows exhibiting self-
duality.

Examples of self-similar objects are given in Section 14, and self-similar
objects of compact closed categories in Lemma 84, Proposition 86, and
Definition 88. A characterisation of self-dual objects in a large class of
compact closed categories is given in Corollary 39, with the example of Lemma
84 being particularly relevant.

######  Remark 8.

The notions ‘pseudo-idempotency’ and ‘self-similarity’ are precisely
equivalent; the different terminology simply arises from different fields.
Some authors (e.g. [20]) use the term ‘idempotent’ for what we call ‘pseudo-
idempotent’, although [37] defines an idempotent to satisfy the much stricter
condition $\mbox{\scalebox{1.2}{$\vartriangleleft$}}\otimes I_{N}\ =\
1_{N}\otimes\mbox{\scalebox{1.2}{$\vartriangleleft$}}$. For consistency, we
use the term self-similar object rather than pseudo-idempotent, unless usage
is very well-established.

Self-duality and self-similarity together are enough to characterise reflexive
objects of compact closed categories.

######  Lemma 9.

Let $({\mathcal{C}},\\_\otimes\\_,\sigma_{\\_,\\_},I,(\ )^{*})$ be a compact
closed category. The reflexive objects of $\mathcal{C}$ are precisely the
self-dual self-similar objects.

###### Proof.

Both parts of this proof are based on the very special form the internal hom
takes in a compact closed category, as $[A\rightarrow
B]\stackrel{{\scriptstyle def.}}{{=}}A^{*}\otimes B$.
$(\Rightarrow)$ Let $R\in Ob(\mathcal{C})$ be a reflexive object, so there
exist mutually inverse arrows
$\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
6.00006pt}\in{\mathcal{C}}(R,[R\rightarrow R])$ and
$\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
3.99994pt}\in{\mathcal{C}}([R\rightarrow R],R)$. As the dual is a
contravariant monoidal functor, the following diagram commutes :

$\textstyle{R^{*}}$$\textstyle{[R\rightarrow
R]^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{[R\rightarrow
R]^{*}}}$$\scriptstyle{\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
4.20004pt}^{*}}$$\textstyle{R^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{R}^{*}}$$\scriptstyle{\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
2.79996pt}^{*}}$$\textstyle{[R\rightarrow R]^{*}}$

Appealing to the identity $[R\rightarrow R]=R^{*}\otimes R$, we then derive
isomorphisms exhibiting the self-duality of $R$.

$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$
$\vartriangleright$ $|$ $\textstyle{R^{*}\otimes
R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{R^{*},R}}$$\textstyle{R\otimes
R^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
4.20004pt}^{*}}$$\textstyle{R^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{R^{*}}}$$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{R}}$$\textstyle{R^{*}\otimes
R\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$ $\vartriangleleft$ $|$
$\textstyle{R\otimes
R^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\sigma_{R,R^{*}}}$$\textstyle{R^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip
2.79996pt}^{*}}$

Once we have established that $R\cong R^{*}$ is self-dual, self-similarity or
pseudo-idempotency of R follows as $R\cong[R\rightarrow R]=R^{*}\otimes R\cong
R\otimes R$. Thus reflexive objects are self-dual and self-similar.
$(\Leftarrow)$ This direction is even simpler. Let $R$ be both self-dual and
self-similar. Then $R\ \cong\ R\otimes R\ \cong\ R^{*}\otimes R=[R\rightarrow
R]$ and so $R$ is reflexive. ∎

######  Remark 10 (Examples of self-similar and reflexive objects).

It is not difficult to give examples of either self-similar or reflexive
objects. From a general viewpoint, self-similarity dates back at least as far
as Hilbert’s parable of the Grand Hotel and Cantor’s work on foundations of
set theory (see [60] for a good overview), and is significantly prefigured by
Galileo’s ‘infinity paradox’. As observed in [26] it is also a key feature of
Girard’s Geometry of Interaction program, and the term ‘self-similar’ is used
in a wide range of algebraic fields (e.g. [19]) motivated by a connection with
fractal structures.

Relevant concrete examples, along with Hilbert-hotel style bijections based on
the natural numbers, are given in Lemma 14 and Definitions 72.

For any self-similar object $X$ of a compact closed category, its tensor with
its dual, $X\otimes X^{*}$ is not only self-similar, but self-dual. Thus,
provided a compact closed category does indeed contain self-similar objects,
we have instant access to reflexive objects555It is perhaps easier to point
out compact closed categories that do not have reflexive objects. The compact
closed category $({\bf Hilb_{fd}},\otimes)$ of finite-dimensional Hilbert
spaces with tensor product, as studied in the categorical quantum mechanics
program, is a notable example. We refer to [4] for the obstacles to defining
compact closure in the infinite-dimensional (& hence reflexive) case. It is
tempting, although highly speculative, to relate this to the problems early
pioneers of quantum computing had in attempting to define a ‘fully quantum’
universal computer [18, 53]..

Concrete examples of reflexive objects are given in Corollary 85. However, at
this point we cannot simply declare that we are done, and have established a
suitable categorical setting for the type-freeness evident in [21, 22, 6]. It
is notable that all the action takes place within a single algebraic
structure. Instead, we treat reflexivity like many other categorical
properties and consider how reflexivity may be ‘strictified’ so that the
isomorphisms exhibiting it become, under a suitable equivalence of categories,
identity arrows.

##  4 Strictification of reflexivity

What we now need is a notion of ‘strictifying’ reflexivity; moving – via a
categorical equivalence – from a setting in which an object is reflexive is up
to some pair of isomorphisms, to a setting in which reflexivity may be
exhibited by identity arrows.

######  Definition 11.

Given a reflexive object $R$ of a closed category $({\mathcal{C}},[\
\rightarrow\ ])$, we define a strictification of the reflexivity of $R$ to be
:

  * •

a small closed category $\mathcal{S}$ and a faithful functor of closed
categories $\Gamma:\mathcal{S}\rightarrow{\mathcal{C}}$,

  * •

a reflexive object $N\in Ob(\mathcal{S})$ where $\Gamma(N)=R$,

  * •

a closed category $\mathcal{D}$, equivalent to $\mathcal{S}$, in which this
reflexivity is exhibited by identity arrows.

The above slightly convoluted description is required to avoid violating the
principle of equivalence; in practice, we will simply refer to ‘a small closed
subcategory of ${\mathcal{C}}$ that contains $R$’, along with an equivalent
closed subcategory where reflexivity is exhibited by identities.

When $R$ is a reflexive object of a monoidal closed category
$({\mathcal{C}},\otimes,[\\_\rightarrow\\_],I)$we say that such a
strictification is a monoidal strictification when the relevant equivalence of
categories is a monoidal equivalence, and the faithful functor
$\Gamma:S\rightarrow{\mathcal{C}}$ is a monoidal functor.

######  Remark 12.

[Closure, and monoidal closure] Closure within the ‘non-monoidal closed
categories’ found in the somewhat obscure paper [45] of M. Laplaza is
undoubtedly the most ‘pure’ form of closure available. Additional categorical
features associated with closure (such as the Cartesian product used in [44])
often correspond to additional logical or computational structures (in [44],
the product re-appears in logcial form, as ‘surjective pairing’), and a notion
of closure defined without reference to any other operations beyond an
internal hom. does not impose any additional notions on a logical or lambda-
calculus interpretation.

Despite this, we consider (monoidal) strictification of reflexivity within
compact closed categories. Thus, we require an equivalence of categories
preserves the unit object, elements of objects and names of arrows, and indeed
the notion of monoidal well-pointedness.

This is partly for theoretical reasons; we are studying the setting of [6, 21,
22], rather than some more abstract notion of combinatory logic or lambda
model. It is also partly for practical reasons; [45] requires what have been
referred to as ‘monstrous’ coherence conditions, which would make any such
strictification a decidedly non-trivial task – we refer to [34] for what is
possibly the closest approach.

We are therefore considering what is possibly the easiest case : monoidal
strictification for a class of reflexive objects in compact closed categories,
including those used in [21, 22, 6].

##  5 Strict duality, and strict self-similarity

As the notion of reflexivity in compact closed categories simply splits into
the notions of self-duality and self-similarity, we first consider what it
means to have strict versions of both of these.

###  5.1 Strict self-duality

The notion of self-duality in the strict setting is well-studied :

######  Definition 13.

A dagger on a (monoidal) category ${\mathcal{C}}$ is defined in [57] to be a
contravariant (monoidal) functor $(\
)^{\dagger}:{\mathcal{C}}^{op}\rightarrow{\mathcal{C}}$ that is the identity
on objects and satisfies $\left((\
)^{\dagger}\right)^{\dagger}=Id_{\mathcal{C}}$. Thus, a dagger can be thought
of as a strict version of self-duality. Simply as notation, we extend this
definition slightly, and say that a dual $(\
)^{*}:{\mathcal{C}}^{op}\rightarrow{\mathcal{C}}$ is a dagger at an object
$X\in Ob({\mathcal{C}})$ when $X$ is strictly self-dual. This is precisely
equivalent to stating that the monoidal subcategory generated by $X$ is a
dagger category.

######  Remark 14.

The best-known examples of daggers on compact closed categories are
undoubtedly those found in the ‘categorical quantum mechanics’ program [5],
where the dual in the compact closed category of finite-dimensional Hilbert
spaces is a dagger. However, we are not able to use this setting to provide
reflexive objects (see footnote 5).

The notion of a dagger has occasionally been criticised as an ‘evil’ concept
(i.e. breaking the principle of equivalence by relying on a notion of equality
between objects). Leaving aside the possibility of the purist leveling the
same criticism at the identity functor, we take an alternative viewpoint :
self-duality is simply a categorical property for which we may consider – in
the appropriate setting – a strict form.

The following is then a simple corollary of Lemma 9 above :

######  Corollary 15.

Let $N$ be a reflexive strictly self-dual object of a compact closed category
$({\mathcal{C}},\otimes,(\ )^{*})$, so $(\ )^{*}$ is a dagger at $N$. Then
$N\in Ob({\mathcal{C}})$ is self-similar, and the $lam$ and $app$ arrows
exhibiting reflexivity

$\mbox{\scalebox{1.1}{$\vartriangleleft$}$|$\hskip 3.99994pt}:[N\rightarrow
N]\rightarrow N\ \mbox{ and }\
\mbox{\scalebox{1.1}{$\vartriangleright$}$|$\hskip
6.00006pt}:N\rightarrow[N\rightarrow N]$

are also code / decode arrows exhibiting self-similarity

$\mbox{\scalebox{1.2}{$\vartriangleleft$}}:N\otimes N\rightarrow N\ \mbox{ and
}\ \mbox{\scalebox{1.2}{$\vartriangleright$}}:N\otimes N\rightarrow N$

###### Proof.

The internal hom in a compact closed category is given by $[N\rightarrow N]\
=\ N^{*}\otimes N$. As the dual is a dagger at $N$, we derive $[N\rightarrow
N]=N\otimes N$. The $lam$ and $app$ isomorphisms are then mutually inverse
bijections exhibiting $N\cong N\otimes N$. However, these are unique up to
unique isomorphism [31], so our result follows. ∎

######  Corollary 16.

Let $N$ be a reflexive strictly self-dual object of a compact closed category.
Then

  1. 1.

The monoidal subcategory generated by $N$ is compact closed,

  2. 2.

All non-unit objects of this subcategory are isomorphic,

  3. 3.

When $N$ is strictly reflexive, this subcategory has precisely two objects,
one of which is the unit object.

(Concrete examples of 1. and 2. are given in Part 4. of Proposition 86, and of
Part 3. in Definition 88).

This convergence of the elements of reflexivity is particularly relevant for
compact closed categories arising from the $\bf Int$ or $\bf GoI$
construction, where all self-dual objects are by construction isomorphic to
some strictly self-dual object.

###  5.2 Strict self-similarity

It is now inevitable that we consider how self-similarity may be strictified.
We are fortunate to be able to rely on a pre-existing coherence theorem and
strictification procedure [31]. However, somewhat inconveniently for our aim
of finding a monoidal strictification of reflexivity, this firmly and
unavoidably lives within the theory of semi-monoidal categories.

###  5.3 Monoidal and semi-monoidal categories

A semi-monoidal category is simply one that satisfies all MacLane’s axioms for
a monoidal category, except for those concerning the unit object. The
following definitions may be found in [42].

######  Definition 17.

A semi-monoidal category is a category ${\mathcal{C}}$ with a functor
$\\_\otimes\\_:{\mathcal{C}}\times{\mathcal{C}}\rightarrow{\mathcal{C}}$ that
is associative up to an object-indexed family of natural isomorphisms
$\tau_{X,Y,Z}:X\otimes(Y\otimes Z)\rightarrow(X\otimes Y)\otimes Z$ satisfying
MacLane’s pentagon condition

$(\ \tau_{W,X,Y}\otimes 1_{Z})\ \tau_{W,X\otimes Y,Z}\ (1_{W}\otimes\
\tau_{X,Y,Z})\ =\ \ \tau_{W\otimes X,Y,Z}\ \tau_{W,X,Y\otimes Z}$

A functor between semi-monoidal categories that (strictly) preserves the
tensor is a (strict) semi-monoidal functor. We assume the obvious definition
of semi-monoidal equivalence of categories.

A semi-monoidal monoid is simply a small semi-monoidal category with precisely
one object. These lie on the border of algebra and category theory, and
interesting algebraic structures frequently arise from core categorical ones
in this setting (e.g. Section 5.4).

What is lost in the passage from monoidal to semi-monoidal categories is the
following notions:

######  Definition 18.

Let $({\mathcal{C}},\otimes,I)$ be a monoidal category. The elements of $X$
are members of the homset ${\mathcal{C}}(I,X)$, and the elements of the unit
object ${\mathcal{C}}(I,I)$ are known as abstract scalars [2], by analogy with
the case of vector spaces and linear maps.

When the abelian monoid of abstract scalars is the singleton, we say that $I$
is a trivial unit, or that $({\mathcal{C}},\otimes,I)$ has trivial scalars.

When ${\mathcal{C}}$ is a monoidal closed category, the elements of
$[X\rightarrow Y]$ are known as names and are in 1:1 correspondence with the
members of the homset ${\mathcal{C}}(X,Y)$. Finally, when
$({\mathcal{C}},\otimes,I)$ is compact closed, there is also a 1:1
correspondence between ${\mathcal{C}}(X,Y)$ and the elements
${\mathcal{C}}([X\rightarrow Y],I)$; these are known as co-names.

We treat monoidal categories as a special class of semi-monoidal categories.
When discussing potential unit objects in semi-monoidal categories, it is
common to rely on A. Saavedra’s characterisation666It is notable that Saavedra
never explicitly stated that this precisely characterised units in the sense
of MacLane-Kelly. This observation was made by J. Kock who also laid out the
basics of the theory of semi-monoidal categories [42]. He later extended this
to a more general theory of ‘weak units’ in collaboration with A. Joyal [37].
of units [55], as laid out in [42, 37]. Thus ‘being a unit’ is a property that
an object may have, rather than a part of the definition.

######  Definition 19.

A (Saavedra) unit in a semi-monoidal category $({\mathcal{C}},\otimes,\tau)$
is an object $U\in Ob(\mathcal{C})$ that is both pseudo-idempotent and
cancellable i.e. it is self-similar, and the functors
$(U\otimes\\_),(\\_\otimes U):{\mathcal{C}}\rightarrow{\mathcal{C}}$ are fully
faithful.

The theory of Saavedra units is particularly relevant for semi-monoidal
monoids, where it allows us to characterise those semi-monoidal monoids whose
unique object is a unit object. The following is taken from [31].

######  Proposition 20.

Let $(M,\star,\alpha)$ be a semi-monoidal monoid. Then $\star$ is strictly
associative (i.e. $\alpha=1_{M}$) iff the unique object of $M$ is a unit
object.

###  5.4 An algebraic interlude

Proposition 20 raises an obvious question : the canonical associativity
isomorphisms for a (non-degenerate) semi-monoidal monoid form a non-trivial
group — is it the same in every case, and if so, which group this is?

One of the most familiar and well-studied objects in group theory is Richard
Thompson’s group $\mathcal{F}$. This was originally defined in terms of a
representation, as the group of homeomorphisms of the unit interval that are
piece-wise linear and order-preserving, non-differentiable only at a finite
number of dyadic rationals, and have slope of the form $2^{k}$,
$k\in\mathbb{N}$ on differentiable sections.

We use the definition as a group presentation :

######  Definition 21.

Thompson’s group $\mathcal{F}$ is defined by

$\mathcal{F}=\langle x_{0},x_{1},x_{2},\ldots\ :\
x_{i}^{-1}x_{j}x_{i}=x_{j+1}\ \forall\ i<j\rangle$

Note that this is not a minimal presentation; it is well-established that
$\\{x_{0},x_{1}\\}$ generates the whole of $\mathcal{F}$. However, the
required relators are significantly less intuitive.

It is by now folklore that group of canonical associativity isomorphisms in a
(non-unit) semi-monoidal monoid is precisely Thompson’s $\mathcal{F}$. This –
or at least statements equivalent to this claim – have been presented and
rediscovered many times, and the following list is not exhaustive!

######  Remark 22.

[Connections between $\mathcal{F}$ and coherence for associativity] As early
as 1973, R. Thompson and J. McKenzie noted [52] a connection with
‘associativity laws’. In [49], M. Lawson considered a class of semi-monoidal
monoids in the special case where the tensor $\\_\star\\_$ admits projection /
injection arrows (as studied in [26, 48, 27]), and demonstrated that the group
of canonical isomorphisms777A curious feature of [49] is that the link between
the given representation of $\mathcal{F}$ and associativity isomorphisms is
not made explicit by the author, despite having (along with other authors)
described and used the same operations as associativity isomorphisms in
previous work [48, 26]. is precisely $\mathcal{F}$. In [17], P. Dehornoy
considered $\mathcal{F}$ abstractly, and noted that, ‘The only [non-trivial]
relations in this presentation of $\mathcal{F}$ correspond to the well-known
MacLane-Stasheff pentagon’. In [20], M. Fiore & T. Leinster considered the
strict monoidal category freely generated by a generic (pseudo-)idempotent and
proved that its symmetry group is precisely $\mathcal{F}$. In [10], M. Brin
talks about, ‘the resemblance of the usual coherence theorems with Thompson’s
group $\mathcal{F}$’, and this observation was used in [31] to note that – at
least in the ‘free’ case, canonical associativity isomorphisms for a semi-
monoidal monoid are precisely a copy of $\mathcal{F}$. M. Lawson recently
updated his paper [49] in [47], and gave a construction of $\mathcal{F}$ based
on (finite) maximal binary prefix codes; any categorically-minded reader will
identify this construction as functorial, and the relevant prefix codes as a
representation of MacLane’s monogenic category $W$ (excluding the unit
object).

The following theorem and outline proof is presented with no claim to
originality; it is given simply because the monoidal category theory is often
implicit, rather than explicit, in several of the references of Remark 22
above. We also wish to connect the generators of the presentation given in
Definition 21 above with the category theory.

######  Theorem 23.

Let $(M,\\_\star\\_)$ be a (non-unit) semi-monoidal monoid. The canonical
associativity isomorphisms for $\\_\star\\_$ form a copy of Thompson’s group
$\mathcal{F}$.

###### Proof.

[OUTLINE]
Let us denote the canonical associator for $\\_\star\\_$ by $\alpha\in M$, and
define $\\{x_{j}\\}_{j\in\mathbb{N}}$ inductively by $x_{0}=\alpha$, and
$x_{i+1}=1\star x_{i}$. Functoriality of $\\_\star\\_$ and MacLane’s pentagon
then immediately give the defining relations of Thompson’s $\mathcal{F}$, as
$x_{i}^{-1}x_{j}x_{i}=x_{j+1}\ \forall\ i<j$. Thus the group of canonical
associativity isomorphisms contains a homomorphic image of $\mathcal{F}$.
However, a standard fact (e.g. [9]) about $\mathcal{F}$ is that it has no non-
abelian quotients, and so this is precisely a copy of $\mathcal{F}$. Finally,
we may appeal to MacLane’s pentagon to demonstrate that all canonical
associativity isomorphisms for $\\_\star\\_$ are generated by the set
$\\{x_{j}\\}_{j\in\mathbb{N}}$. ∎

######  Remark 24.

Thompson’s group $\mathcal{F}$ is itself, of course, a semi-monoidal monoid.
This observation was made – in non-categorical terms – by K. Brown in [11]
where he describes a group homomorphism
$\mu:\mathcal{F}\times\mathcal{F}\rightarrow\mathcal{F}$ that is “associative
up to conjugation by the generator $x_{0}$”. It is also remarkable that –
despite [11] being phrased in entirely non-categorical terms – K. Brown also
proves that $\mu(1,\\_)$ and $\mu(\\_,1)$ are injective, but cannot be
surjective. In our terms, he is establishing precisely that J. Kock’s
conditions for a Saavedra unit are not satisfied by the unique object of
$\mathcal{F}$.

###  5.5 Functors between monoidal & semi-monoidal categories

We return to category theory, and define several functors between the (large)
categories of monoidal and semi-monoidal categories.

######  Definition 25.

We denote the (large) categories of monoidal categories and semi-monoidal
categories by $\bf MonCat$ and $\bf SemiMonCat$ respectively. There is an
obvious faithful functor $\iota:{\bf MonCat}\rightarrow{\bf SemiMonCat}$
corresponding to the triviality that every monoidal category is also semi-
monoidal.

Given a semi-monoidal category $({\mathcal{C}},\otimes)$, we may adjoint a
strict unit object simply by taking the categorical coproduct with the
terminal monoidal category, and extending the tensor by strictness. This
process is functorial; we denote this functor by $(\\_)_{+I}:{\bf
SemiMonCat}\rightarrow{\bf MonCat}$. Note that by construction,
$({\mathcal{C}},\otimes)_{+I}$ has trivial scalars, and no non-trivial
elements.

Going in the other direction, given a monoidal category
$(\mathcal{M},\\_\otimes\\_,I)$, let us denote by
$(\mathcal{M},\\_\otimes\\_)_{-I}$ the full subcategory consisting of all non-
unit objects. This ‘forgetting the unit’ process is also functorial; we denote
this by $(\\_)_{-I}:{\bf MonCat}\rightarrow{\bf SemiMonCat}$. The composite
$\left((\ )_{+I}\right)_{-I}=Id_{\bf SemiMonCat}$. This is, of course, a one-
sided inverse; $\left((\ )_{-I}\right)_{+I}:{\bf MonCat}\rightarrow{\bf
MonCat}$ is certainly not the identity functor. Rather, it has the effect of
deleting elements (and therefore, when appropriate, names and co-names). This
endofunctor on $\bf MonCat$ will prove important; we refer to it as the de-
element functor, and denote it by $\left(\
\right)_{-{\tiny\begin{array}[]{cc}{\mathcal{E}}&\\!\\!{\mathcal{A}}\\\\[-1.5pt]
{\mathcal{F}}&\\!\\!{\mathcal{W}}\end{array}}}=\left(\left(\
\right)_{-I}\right)_{+I}:\ {\bf MonCat}\rightarrow{\bf MonCat}$.

######  Remark 26.

Given a compact closed category $(\mathcal{C},\otimes)$, the de-element
functor certainly does not result in a compact closed category;
$(\mathcal{C},\otimes)_{-{\tiny\begin{array}[]{cc}{\mathcal{E}}&\\!\\!{\mathcal{A}}\\\\[-1.5pt]
{\mathcal{F}}&\\!\\!{\mathcal{W}}\end{array}}}$ has lost elements, including
abstract scalars, names, co-names, & the distinguished unit / co-unit maps.
However, it may still be closed in the sense of [45].

######  Remark 27.

A natural question is whether, given some abelian monoid $U$, we may ‘extend’
a monoidal category with trivial scalars to one where the abstract scalars are
taken from this abelian monoid? This is a surprisingly non-trivial task; a
procedure for doing so in the case of traced and compact closed categories is
given in [2]. We discuss this further in Section 17

##  6 A coherence theorem for self-similarity

We now describe the relevant points of the coherence theorem for self-
similarity [31], which lives firmly within the category $\bf SemiMon$.

The theory of semi-monoidal monoids is essentially interchangeable with the
theory of self-similarity in semi-monoidal categories. Let $(M,\star)$ be a
monoid with a semi-monoidal tensor; the unique object $m\in Ob(M)$ of this
monoid is clearly self-similar, as $m\star m=m$. Similarly, the endomorphism
monoid of any strictly self-similar object is clearly a semi-monoidal
monoid888A special case of this is strictly reflexive objects in compact
closed categories. However, this is due to the special form that the internal
hom takes in a compact closed category; the same need not be true in arbitrary
monoidal closed categories, and is certainly not the case for non-monoidal
closed categories.. Thus semi-monoidal monoids may be considered to be a
‘strict’ form of self-similar objects. This observation was formalised in the
coherence theorem and strictification procedure of [31], where the following
useful results may be found :

######  Theorem 28.

Let $N\in Ob({\mathcal{C}})$ be a self-similar object of a semi-monoidal
category $(\mathcal{C},\otimes)$, and let
$\mbox{\scalebox{1.2}{$\vartriangleleft$}}\in{\mathcal{C}}(N\otimes N,N)$ and
$\mbox{\scalebox{1.2}{$\vartriangleright$}}\in{\mathcal{C}}(N,N\otimes N)$ be
the unique (up to unique isomorphism) code and decode bijections exhibiting
this self-similarity. Then

  1. 1.

The operation defined on the endomorphism monoid of $N$ by

$f\star g=\mbox{\scalebox{1.2}{$\vartriangleleft$}}(f\otimes
g)\mbox{\scalebox{1.2}{$\vartriangleright$}}\ \ \forall
f,g\in{\mathcal{C}}(N,N)$

is a semi-monoidal tensor on ${\mathcal{C}}(N,N)$.

  2. 2.

There is a semi-monoidal equivalence of categories between

    1. (a)

the semi-monoidal subcategory of $(\mathcal{C},\otimes)$ generated by $N$,

    2. (b)

the semi-monoidal monoid $(\mathcal{C}(N,N),\\_\star\\_)$.

  3. 3.

As a consequence of Proposition 20, the equivalence of categories of Point 2
maps strict to non-strict associativity in the case where $\\_\otimes\\_$ is
strict but $N$ is not a unit object.

###### Proof.

We refer to [31] for proofs of the above. These proofs are based on giving
necessary and sufficient conditions for the commutativity of diagrams over a
certain class of primitives (the tensor $\otimes$ and its canonical
isomorphisms, the tensor $\star$ and its canonical isomorphisms, and the code
/ decode arrows). ∎

######  Remark 29 (On the choice of code / decode arrows).

It is natural to wonder whether the choice of code / decode arrows is
significant – in particular, if we are intending to strictify reflexivity,
should we not ensure that the distinguished  $\vartriangleright$ $|$ and
$\vartriangleleft$ $|$ of Corollary 15 are chosen, as opposed to some other
isomorphisms with the same source / target?

The answer to this lies in the observation of [31] that code / decode arrows
are unique up to unique isomorphism. Thus, all strictifications of some self-
similar object are semi-monoidally equivalent (algebraically, they are
isomorphic semi-monoidal monoids), regardless of the choice of code / decode
arrows. Changing the code / decode isomorphisms may be seen as moving to an
isomorphic representation of the same structure – this is studied in more
detail in [32], where an analogy between this and changes of basis in matrix
representations is formalised.

######  Corollary 30.

The endomorphism monoid of every self-similar object in a semi-monoidal
category contains a copy of Thompson’s $\mathcal{F}$. (Note that this result
holds even if the semi-monoidal category in question is strictly associative).

The ‘adjoining a strict unit’ functor $(\ )_{+I}:{\bf
SemiMonCat}\rightarrow{\bf MonCat}$ of Definition 25 does not give us, for
free, a monoidal, rather than semi-monoidal, equivalence. Rather, we have the
following simple corollary:

######  Corollary 31.

Let $({\mathcal{C}},\otimes,I)$ be a monoidal category, and denote by
$(N^{\otimes},\otimes,I)$ the full monogenic monoidal subcategory generated by
some self-similar object $N\cong N\otimes N$. Then there exists a monoidal
equivalence of categories between $({\mathcal{C}},\star)_{+I}$ and
$(N^{\otimes},\otimes,I)_{-{\tiny\begin{array}[]{cc}{\mathcal{E}}&\\!\\!{\mathcal{A}}\\\\[-1.5pt]
{\mathcal{F}}&\\!\\!{\mathcal{W}}\end{array}}}$.

######  Remark 32.

As Corollary 31 emphasises, the strictification process for self-similarity of
[31] naturally lives within $\bf SemiMonCat$ rather than $\bf MonCat$;
Applying it in the monoidal setting gives an equivalence of ‘de-elemented’
categories. Some work is needed in order to use it to strictify reflexivity in
a compact closed category, even given a self-similar object with a dagger.

The key to doing this is the canonical construction of compact closed
categories from symmetric traced monoidal categories, given by either the Int
construction of [40], or the GoI construction of [1]. Notably, this
construction equips the compact closed category with a suitable range of
elements (& hence names and co-names), even when the underlying traced
category has none.

##  7 From traced categories to compact closure

It is well known that the two constructions of compact closed categories from
symmetric traced monoidal categories (the Int construction of [40] and the GoI
construction of [1]) are equivalent in the symmetric case, although [40] also
considered the more general braided / tortile monoidal categories. Despite
this, they used significantly different conventions, and the equivalence
between the two was given by E. Haghverdi in [24] (see also Footnote 8.).

Somewhat perversely for a volume dedicated to the work of S. Abramsky, we will
work with the conventions of [40] instead999Although this has become
convention, we do not simply act out of peer pressure. Rather, we consider the
conventions of [40] and [1] to give two different, but isomorphic compositions
(along with tensors, duals, etc.) on the same underlying structure. Our claim
is that interesting category theory and algebra may arise out of taking a
2-category or bi-category approach, and considering the interaction of the
two. This was (implicitly) the approach taken in the identification in [26] of
the cut / cut-elimination procedure in Girard’s Geometry of Interaction as
compact closure. This was written when the author was unaware of the work of
[1] and based on an early draft of [40]. This referred to a second,
isomorphic, ‘vertical’ composition on hom-sets of $\bf Int(\mathcal{C})$,
introduced in order to transform the ‘horizontal’ composition of [40] into
something that directly matched the resolution formula and cut-elimination
procedure within Girard’s Geometry of Interaction system. In retrospect, the
(isomorphic) ‘horizontal’ and ‘vertical’ compositions are those derived from
the respective $\bf Int$ and $\bf GoI$ constructions of [40] and [1]. See
Remark 71 for more details on this..

###  7.1 Categorical traces

We start with the definition of a traced symmetric monoidal category, as a
special case of the more general braided monoidal categories of [40].

######  Definition 33.

A trace on a symmetric monoidal category
$(\mathcal{C},\\_\otimes\\_,\sigma_{\\_,\\_},I)$ is an object-indexed family
of mappings of homsets $Tr^{U}_{X,Y}:\mathcal{C}(X\otimes U,Y\otimes
U)\rightarrow\mathcal{C}(X,Y)$ that is natural in $X$ and $Y$, dinatural in
$U$, and satisfies the following axioms:

  * •

(Vanishing I) $Tr^{I}_{X,Y}(\ )=Id_{{\mathcal{C}}(X,Y)}$, for all $X,Y\in
Ob({\mathcal{C}})$.

  * •

(Vanishing II) $Tr^{U\otimes V}_{X,Y}=Tr^{U}_{X,Y}\left(Tr^{V}_{X\otimes
U,Y\otimes U}(f)\right)$ for all $f:X\otimes U\otimes V\rightarrow Y\otimes
U\otimes V$.

  * •

(Yanking) $Tr^{U}_{U,U}(\sigma_{U,U})=1_{U}$.

  * •

(Superposing) $Tr^{U}_{X,Y}(f)\otimes g=Tr^{U}_{X\otimes A,Y\otimes
B}\left((1_{Y}\otimes\sigma_{B,U})(f\otimes
g)(1_{X}\otimes\sigma_{A,U})\right)$ for all $f:X\otimes U\rightarrow Y\otimes
U$, $g:A\rightarrow B$.

######  Remark 34.

A consequence of the Vanishing I axiom is that when
$({\mathcal{C}},\otimes,I)$ has trivial scalars, traces are uniquely
determined by their action on non-unit objects. The Vanishing II axiom is also
sometimes known as the ‘confluence axiom’, for obvious reasons.

The diagrammatic calculus for traced & compact closed categories is well-
established in [38, 39, 40], where traces appear as feedback loops :

$\textstyle{f:X\otimes U\rightarrow Y\otimes
U}$$\textstyle{Tr^{U}(f):X\rightarrow
Y}$$\textstyle{Y}$$\textstyle{U}$$\textstyle{Y}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{F}$
is mapped to
$\textstyle{F}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

##  8 From traces to compact closure

We now give an exposition of the construction of compact closed categories
from traced symmetric monoidal categories

######  Definition 35.

Let $(\mathcal{C},\otimes,\sigma,I,Tr_{\\_,\\_}^{\\_}(\ ))$ be a traced
symmetric monoidal category. The compact closed category $({\bf
Int\mathcal{C}},\\_\Box\\_,(\ )^{*},\epsilon_{\\_},\eta_{\\_})$ is defined as
follows:

  1. 1.

(Objects) An object $(X,U)$ of $\bf Int{\mathcal{C}}$ is a pair of objects of
$\mathcal{C}$.

  2. 2.

(Arrows) The homset ${\bf Int{\mathcal{C}}}((X,U),(Y,V))$ is precisely
${\mathcal{C}}(X\otimes V,Y\otimes U)$.

  3. 3.

(Composition) Given arrows $f:(X,U)\rightarrow(Y,V)$ and
$g:(Y,V)\rightarrow(Z,W)$, their composite $g\circ f\in{\bf
Int{\mathcal{C}}}((X,U),(Z,W))$ is defined using the trace, symmetry, &
composition of the underlying category ${\mathcal{C}}$ (which we denote by
concatenation), as follows :

$\textstyle{Z}$$\textstyle{U}$$\textstyle{Z}$$\textstyle{V}$$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{g\in{\bf
Int{\mathcal{C}}}((Y,V),(Z,W))}$$\textstyle{g}$$\textstyle{g}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{g\circ
f\in{\bf
Int{\mathcal{C}}}((X,U),(Z,W))}$$\textstyle{Y}$$\textstyle{U}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{f\in{\bf
Int{\mathcal{C}}}((X,U),(Y,V))}$$\textstyle{f}$$\textstyle{f}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

  4. 4.

(Identities) The identity at an object $1_{(X,U)}\in{\bf
Int{\mathcal{C}}}((X,U),(X,U))$ is simply $(1_{X}\otimes
1_{U})\in{\mathcal{C}}(X\otimes U,X\otimes U)$.

  5. 5.

The Tensor $\bf Int{\mathcal{C}}$ has a symmetric monoidal tensor,
$\\_\Box\\_$, given by:

     * •

(Objects) $(X_{1},U_{1})\Box(X_{2},U_{2})\ =\ (X_{1}\otimes X_{2},U_{2}\otimes
U_{1})$ for all $(X_{1},U_{1}),(X_{2},U_{2})\in Ob({\bf Int{\mathcal{C}}})$.

     * •

(Arrows) Given arrows $f:(X_{1},U_{1})\rightarrow(Y_{1},V_{1})$ and
$g:(X_{2},U_{2})\rightarrow(Y_{2},V_{2})$, their tensor $f\Box
g:(X_{1},U_{1})\Box(X_{2},U_{2})\rightarrow(Y_{1},V_{1})\Box(Y_{2},V_{2})$ is
given diagrammatically, as

$\textstyle{Y_{1}}$$\textstyle{Y_{2}}$$\textstyle{U_{2}}$$\textstyle{U_{1}}$$\textstyle{Y_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{U_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{f}$$\textstyle{g}$$\textstyle{X_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{V_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

  6. 6.

(The unit object) The unit object is simply $(I,I)$, where $I$ is the unit
object of ${\mathcal{C}}$.

  7. 7.

(The dual on objects) This is defined by $(X,U)^{*}=(U,X)$.

  8. 8.

(The dual on arrows) This is defined in terms of the symmetry isomorphism of
${\mathcal{C}}$; given an arrow $f\in{\mathcal{C}}((X,U),(Y,V))$, then
$\left(f\right)^{*}=\left(\sigma_{Y,U}f\sigma_{X,V}\right)\in{\bf
Int{\mathcal{C}}}((U,X),(Y,V))$.

  9. 9.

(The unit and co-unit) The distinguished unit and co-unit arrows
$\eta:(I,I)\rightarrow(X,U)\Box(U,X)$ and
$\epsilon:(U,X)\Box(X,U)\rightarrow(I,I)$ are specified by symmetry arrows in
the underlying traced monoidal category $\mathcal{C}$, so

$\eta_{(X,U)}=\left(\sigma_{I,X\otimes U}\right)\in{\bf
Int{\mathcal{C}}}((I,I),(X,U)\Box(U,X))$

and

$\epsilon_{(U,X)}=\left(\sigma_{U\otimes X,I}\right)\in{\bf
Int{\mathcal{C}}}((U,X)\Box(X,U),(I,I))$

Although Joyal, Street, and Verity assumed strict associativity of the
underlying traced monoidal category (and hence of the resulting compact closed
category), and often left canonical isomorphisms implicit, it is nevertheless
straightforward to write down the construction in the case where these
canonical isomorphisms are made explicit. This rather thankless task was
carried out in [26] where the following may be found:

######  Lemma 36.

Let $({\mathcal{C}},\otimes\sigma_{\\_,\\_},\tau_{\\_,\\_,\\_},I,Tr(\ ))$ be a
traced symmetric monoidal category. Then the associativity and symmetry
isomorphisms of the resulting compact closed category $({\bf
Int{\mathcal{C}}},\\_\Box\\_)$ are given by

Symmetry

For all $(X,U),(X^{\prime},U^{\prime})\in Ob({\bf Int{\mathcal{C}}})$,

$S_{(X,U),(X^{\prime},U^{\prime})}=\sigma_{X,X^{\prime}}\otimes\sigma_{U,U^{\prime}}$

Associativity

For all $(X,U),(Y,V),(Z,W)\in Ob({\bf Int{\mathcal{C}}})$,

$T_{(X,U),(Y,V),(Z,W)}=\alpha_{X,Y,Z}\otimes\alpha^{-1}_{W,V,U}$

###### Proof.

We refer to [26] for the details. The key point is to demonstrate that the
sources and targets are correct.

Symmetry

${\mathcal{C}}((X\otimes X^{\prime})\otimes(U\otimes
U^{\prime}),(X^{\prime}\otimes X)\otimes(U^{\prime}\otimes U))={\bf
Int{\mathcal{C}}}((X,U)\Box(X^{\prime},U^{\prime}),(X^{\prime},U^{\prime})\Box(X,U))$

Associativity

$\begin{array}[]{rl}&{\mathcal{C}}(\left(X\otimes(Y\otimes
Z)\right)\otimes\left((W\otimes V)\otimes U\right),\left((X\otimes Y)\otimes
Z)\right)\otimes\left(W\otimes(V\otimes U)\right)\\\ =&{\bf
Int{\mathcal{C}}}((X,U)\Box((Y,V)\Box(Z,W)),((X,U)\Box(Y,V))\Box(Z,W))\\\
\end{array}$

∎

A common intuition is that $\bf Int\mathcal{C}$ is a ‘dualised’ version of
$\mathcal{C}$ that contains both $\mathcal{C}$ and $\mathcal{C}^{op}$. This is
apparent in the following, taken from [40].

######  Proposition 37.

There exist faithful traced monoidal functors
$L_{I},R_{I}:{\mathcal{C}}\rightarrow{\bf Int{\mathcal{C}}}$ that are
covariant and contravariant respectively. These are given by, for all $X,Y\in
Ob(\mathcal{C})$, and $f\in\mathcal{C}(X,Y)$,

Covariant

$L_{I}(X)=(X,I)$ and $L_{I}(f)=(f\otimes 1_{I})\in{\bf
Int{\mathcal{C}}}((X,I),(Y,I))$

Contravariant

$R_{I}(X)=(I,X)$ and $R_{I}(f)=(1_{I}\otimes f)\in{\bf
Int{\mathcal{C}}}((I,X),(I,Y))$

Should we be prepared to consider semi-monoidal rather than monoidal functors,
the above proposition generalises to arbitrary non-unit objects. In this
setting, we have no single distinguished covariant and contravariant faithful
semi-monoidal functors from $(\mathcal{C},\otimes)$ to $({\bf
Int{\mathcal{C}}},\Box)$; rather, we have such functors indexed by the objects
of $\mathcal{C}$.

######  Proposition 38.

Given an arbitrary object $U\in Ob(\mathcal{C})$ of some traced symmetric
monoidal category, we may define both covariant and contravariant faithful
semi-monoidal functors from $(\mathcal{C},\otimes)$ to $(\bf
Int\mathcal{C},\Box)$ by, for all $X,Y\in Ob(\mathcal{C})$, and
$f\in\mathcal{C}(X,Y)$,

Covariant

$L_{U}(X)=(X,U)$ and $L_{U}(f)=(f\otimes
1_{U})\in{\bf{\mathcal{C}}}((X,U),(Y,U))$

Contravariant

$R_{U}(X)=(U,X)$ and $R_{U}(f)=(1_{U}\otimes f)\in{\bf
Int{\mathcal{C}}}((U,X),(U,Y))$

###### Proof.

This follows in precisely the same way as the standard proofs of Proposition
37; we are simply not insisting that our functors preserve a unit object. ∎

######  Corollary 39.

As a well-established corollary, objects of the form$(N,N)\in Ob({\bf
Int{\mathcal{C}}})$ are self-dual, for arbitrary $N\in Ob(\mathcal{C})$, and
all self-dual objects are isomorphic to some object of this form.

######  Corollary 40.

A self-dual object $(N,N)\in Ob({\bf Int{\mathcal{C}}})$ is self-similar iff
$N\in Ob({\mathcal{C}})$ is self-similar.

###### Proof.

$(\Leftarrow)$ This is immediate, and well-established (e.g. [26]). Given code
/ decode arrows
$\mbox{\scalebox{1.2}{$\vartriangleleft$}}\in\mathcal{C}(N\otimes N,N)$ and
$\mbox{\scalebox{1.2}{$\vartriangleright$}}\in\mathcal{C}(N,N\otimes N)$, the
self-similarity of $(N,N)\in Ob({\bf Int\mathcal{C}})$ is exhibited by

$(\mbox{\scalebox{1.2}{$\vartriangleleft$}}\otimes\mbox{\scalebox{1.2}{$\vartriangleright$}})\in{\bf
Int{\mathcal{C}}}((N,N)\Box(N,N),(N,N))\ \ \mbox{ and }\ \
(\mbox{\scalebox{1.2}{$\vartriangleright$}}\otimes\mbox{\scalebox{1.2}{$\vartriangleleft$}})\in{\bf
Int{\mathcal{C}}}((N,N),(N,N)\Box(N,N))$

$(\Rightarrow)$ Consider some $(N,N)\cong(N,N)\Box(N,N)$. then

$(N,N)\ \cong\ (N,I)\Box(I,N)\ \cong\
\left((N,I)\Box(I,N)\right)\Box\left((N,I)\Box(I,N)\right)$

As the tensor of $\bf Int{\mathcal{C}}$ is symmetric, this implies

$(N,I)\Box(I,N)\ \cong\
\left((N,I)\Box(N,I)\right)\Box\left((I,N)\Box(I,N)\right)\ \cong\ (N\otimes
N,I)\Box(I,N\otimes N)$

and our result follows as the functors
$L_{I},R_{I}:{\mathcal{C}}\rightarrow{\bf Int{\mathcal{C}}}$ are faithful. ∎

As a corollary of the above two results, we observe that is is
straightforward, at least in principle, to exhibit strictly reflexive objects
of compact closed categories derived from the $\bf Int$ construction.

######  Corollary 41.

Let $N\in Ob({\mathcal{C}})$ be a strictly self-similar object of a symmetric
traced monoidal category. Then $(N,N)\in Ob({\bf Int{\mathcal{C}}})$ is both
strictly self-dual and strictly self-similar, and hence strictly reflexive.

###### Proof.

Strict self-duality is immediate. The self-similarity of $(N,N)$ is, by
Corollary 40, exhibited by

$(\mbox{\scalebox{1.2}{$\vartriangleleft$}}\otimes\mbox{\scalebox{1.2}{$\vartriangleright$}})\in{\bf
Int{\mathcal{C}}}((N,N)\Box(N,N),(N,N))\ \ \mbox{ and }\ \
(\mbox{\scalebox{1.2}{$\vartriangleright$}}\otimes\mbox{\scalebox{1.2}{$\vartriangleleft$}})\in{\bf
Int{\mathcal{C}}}((N,N),(NN)\Box(N,N))$

However, when $\mbox{\scalebox{1.2}{$\vartriangleleft$}}=1_{N}=1_{N\otimes
N}=\mbox{\scalebox{1.2}{$\vartriangleright$}}$ these are both identity maps,
so $(N,N)$ is strictly self-similar. ∎

The above result is not as helpful as it first appears; it is not immediate
how to find strictly self-similar objects of traced monoidal categories; we do
not have a consistent method of strictifying self-similarity in monoidal
(rather than semi-monoidal) setting, so some work remains before we can
achieve our goal of strictifying reflexivity in compact closed categories.

###  8.1 A naming of parts

A useful aspect of the $\bf Int$ construction is that it simply creates names
(& indeed elements generally) ex nihilo. Less dramatically, we observe that
even when the underlying traced monoidal category $({\mathcal{C}},\otimes)$
has no elements, the category $\bf Int{\mathcal{C}}$ is, by construction,
fully equipped with names for all its arrows (& hence a wide range of
elements).

######  Lemma 42.

Let $(\mathcal{C},\otimes,\sigma,I,Tr_{\\_,\\_}^{\\_})$ be a traced symmetric
monoidal category. Then :

  1. 1.

For arbitrary $(U,V)\in Ob({\bf Int{\mathcal{C}}})$, the elements of $(U,V)$
are in 1:1 correspondence with the homset ${\mathcal{C}}(V,U)$.

  2. 2.

For arbitrary $X\in Ob({\mathcal{C}})$ , the following are in 1:1
correspondence:

     * •

elements of $X\in Ob({\mathcal{C}})$,

     * •

elements of $L_{I}(X)\in Ob({\bf Int{\mathcal{C}}})$,

     * •

elements of $R_{I}(X)\in Ob({\bf Int{\mathcal{C}}})$.

  3. 3.

For an arbitrary self-dual object $(N,N)\in Ob({\bf Int{\mathcal{C}}})$, the
elements of $(N,N)$ are in 1:1 correspondence with the endomorphism monoid
${\mathcal{C}}(N,N)$.

###### Proof.

  1. 1.

From the definition of homsets, ${\bf
Int{\mathcal{C}}}((I,I),(U,V))\stackrel{{\scriptstyle
def.}}{{=}}{\mathcal{C}}(I\otimes V,U\otimes I)\cong{\mathcal{C}}(V,U)$.

  2. 2.

As a special case of 1., ${\bf
Int{\mathcal{C}}}((I,I),L_{I}(X))\stackrel{{\scriptstyle
def.}}{{=}}{\mathcal{C}}(I\otimes I,X\otimes I)\cong{\mathcal{C}}(I,X)$ and
${\bf Int{\mathcal{C}}}((I,I),R_{I}(X))\stackrel{{\scriptstyle
def.}}{{=}}{\mathcal{C}}(I\otimes I,I\otimes X)\cong{\mathcal{C}}(I,X)$.

  3. 3.

This is again a special case of 1.

∎

##  9 Strictifying reflexivity in a compact closed category

The observations of Lemma 42, although straightforward, provide a route to the
monoidal equivalences of compact closed categories we need in order to give a
monoidal strictification of reflexivity. The following preliminary results are
needed:

######  Proposition 43.

Let $({\mathcal{C}},\otimes)$ be a symmetric traced monoidal category with
trivial scalars. Then

  1. 1.

The de-elemented version
$({\mathcal{C}},\otimes)_{-{\tiny\begin{array}[]{cc}{\mathcal{E}}&\\!\\!{\mathcal{A}}\\\\[-1.5pt]
{\mathcal{F}}&\\!\\!{\mathcal{W}}\end{array}}}$ is also traced.

  2. 2.

For arbitrary non-unit $N\cong N\otimes N\in Ob({\mathcal{C}})$ there is a
$\dagger$ \- isomorphism101010The terminology ‘isomorphic’ rather than
‘equivalent’ is deliberate; these are both small categories, and there is a
bijection of sets of objects as well as homsets. of $\dagger$-compact closed
categories between

    1. (a)

The monoidal subcategory of $\bf Int{\mathcal{C}}$ generated by $(N,N)$.

    2. (b)

The monoidal subcategory of $\bf
Int\left({\mathcal{C}}_{-{\tiny\begin{array}[]{cc}{\mathcal{E}}&\\!\\!{\mathcal{A}}\\\\[-1.5pt]
{\mathcal{F}}&\\!\\!{\mathcal{W}}\end{array}}}\right)$ generated by $(N,N)$.

  3. 3.

When $N$ is self-similar, the monoidal subcategory of ${\bf
Int}(({\mathcal{C}}(N,N),\star)_{+I})$ generated by $(N,N)$ is $\dagger$
monoidal equivalent to a. and b. above.

###### Proof.

  1. 1.

This is a straightforward consequence of the Vanishing 1 axiom; as observed in
Remark 34, tracing out the unit object is the identity on homsets. Conversely,
as there is only one abstract scalar of
$({\mathcal{C}},\otimes)_{-{\tiny\begin{array}[]{cc}{\mathcal{E}}&\\!\\!{\mathcal{A}}\\\\[-1.5pt]
{\mathcal{F}}&\\!\\!{\mathcal{W}}\end{array}}}$, traces of the form
$Tr_{I,I}^{U}(\ )$ are also uniquely determined.

  2. 2.

Parts a. and b. follows from Part 3. of Lemma 42 above; the only homsets of
either of these compact closed categories determined by elements of the
underlying traced category are the abstract scalars, which are trivial in both
cases. It makes no difference whether or not we start with the ‘de-elemented’
version.

  3. 3.

This follows from the monoidal equivalence of categories noted in Corollary 31
(and indeed the fact that the $\bf Int$ construction is not ‘evil’; given
monoidally equivalent traced monoidal categories ${\mathcal{C}}$ and
$\mathcal{D}$, there exists a monoidal equivalence of categories between $\bf
Int({\mathcal{C}})$ and $\bf Int(\mathcal{D})$).

We may also exhibit the trace on $({\mathcal{C}}(N,N),\star)_{+I}$ explicitly;
in [26] it is observed that for a self-similar object $N$ of a symmetric
traced monoidal category, there exists an operation $trace$ on
$({\mathcal{C}}(N,N),\star)$ given by

$trace(f)\ =\
Tr_{N,N}^{N}(\mbox{\scalebox{1.2}{$\vartriangleright$}}f\mbox{\scalebox{1.2}{$\vartriangleleft$}})\
\ \forall f\in{\mathcal{C}}(N,N)$

that ‘satisfies all of the axioms of [40] apart from Vanishing I’. As
${\mathcal{C}}$ has trivial scalars, this extends uniquely (as described in
Remark 34) to a categorical trace on the symmetric monoidal category
$({\mathcal{C}}(N,N),\star)_{+I}$, and coincides, up to monoidal equivalence,
with the trace on the subcategory of ${\mathcal{C}}$ monoidally generated by
$N$.

∎

This now gives the desired monoidal strictification of extensional
reflexivity.

######  Theorem 44.

Let $\left({\mathcal{C}},\otimes,\sigma,I,Tr(\ )\right)$ be a symmetric traced
monoidal category with trivial scalars, and let $X\in Ob({\bf
Int{\mathcal{C}}})$ be a reflexive object. Then there exists a monoidal
strictification of the reflexivity of $X$.

###### Proof.

By Lemma 9, $X$ is self-dual, and from Corollary 39 it is therefore isomorphic
to $(N,N)\in Ob(\bf Int{\mathcal{C}})$ for some $N\in Ob({\mathcal{C}})$.
Without loss of generality, we therefore work with the strictly self-dual
reflexive object $(N,N)\in Ob({\bf Int{\mathcal{C}}})$. As $X$ is self-
similar, $N$ is therefore a self-similar object of $({\mathcal{C}},\otimes)$,
by Corollary 40.

By Proposition 43 above, the monoidal subcategory of ${\bf
Int}(({\mathcal{C}}(N,N),\star)_{+I})$ generated by $(N,N)$ then gives a
monoidal strictification of this reflexivity, as axiomatised in Definition 11.
∎

###  9.1 Discussion

We have exhibited a process that will strictify the reflexivity of a large
class – although not all – reflexive objects in compact closed categories.
There are several notable points.

  1. 1.

The two restrictions on this process are :

    1. (a)

The compact closed category itself needs to arise from applying the $\bf Int$
or $\bf GoI$ construction, to a traced monoidal category.

    2. (b)

The underlying traced monoidal category (and hence the compact closed category
itself) must have trivial scalars.

The first condition rules out compact closed categories such as finite-
dimensional Hilbert spaces with tensor product (which does not, in any case,
have reflexive objects), or relations with Cartesian product (which certainly
does have reflexive objects). However, it is satisfied by the categories on
which the original Geometry of Interaction system was based.

The second condition is also satisfied by the setting of the original Geometry
of Interaction system that we will analyse in Section 11 onwards. It is harder
to think of ‘natural’ examples that are ruled out by this restriction,
although we may certainly construct examples by using the techniques of [2] to
‘adjoin’ a non-trivial involutive monoid of abstract scalars. This is
discussed further in Section 17.

  2. 2.

The object $(N,N)$ of the compact closed category ${\bf
Int}\left(({\mathcal{C}}(N,N),\star)_{+I}\right)$ is strictly self-similar,
and therefore its endomorphism monoid is a semi-monoidal monoid. At this
point, it is tempting to axiomatise away all the problems of Section 2.1, and
simply define a ‘compact closed monoid’ to be the result of such a process.
This would be inaccurate, and on a par with simply defining a compact closed
category to be some subcategory of one that arises from (a restricted version
of) the $\bf Int$ or $\bf GoI$ construction.

  3. 3.

A curiosity of this setting is that the endomorphism monoid of $N$ in the
traced monoidal category $({\mathcal{C}}(N,N),\star)_{+I}$ has the same
underlying set as the endomorphism monoid of $(N,N)$ in the compact closed
category ${\bf Int}\left({\mathcal{C}}(N,N),\star)_{+I}\right)$, since $N$ is
strictly self-similar. This is a very useful property when we come to study
such endomorphism monoids from a more algebraic setting.

######  Conjecture.

The restrictions of Point 1. above are not essential, and reflexivity may be
strictified for arbitrary reflexive objects in compact closed categories.

##  10 Properties of strictly reflexive objects

We now move on from demonstrating that – at least in certain cases –
reflexivity may be strictified, and consider the structure of strictly
reflexive objects in compact closed categories more generally. Our setting
includes, but is not restricted to, objects derived from the strictification
of reflexivity given in Theorem 44.

###  10.1 Notation & an algebraic perspective

As observed in Point 3 of Section 9.1, for a strictly self-similar object $N$
of a traced symmetric monoidal category ${\mathcal{C}}$, the endomorphism
monoids ${\mathcal{C}}(N,N)$ and ${\bf Int{\mathcal{C}}}((N,N),(N,N))$have the
same underlying set. The $\bf Int$ construction provides a new composition,
tensor, etc. on this set. With suitable notational discipline, we may treat
the ‘old’ and ‘new’ compositions & tensors as operations on the same set, and
even consider their interaction.

This is not done simply in order to horrify categorically-minded readers
(although it will undoubtedly have that effect), but neither is it just a
notational trick.

The historical precedent and motivation for this was not originally phrased
categorically. In Girard’s system, it is notable that the dynamics (i.e. cut
and cut-elimination) is modeled by the composition of an endomorphism monoid
of a compact closed category, whereas the model of conjunction is the tensor
$\\_\star\\_$ of the underlying traced category. The models of the
exponentials are different again, and the bang $!(\ )$ is best seen as a right
fixed-point semi-monoidal endofunctor $f\star!(f)=!(f)$ for the tensor
modeling the conjunction – but is derived from yet another monoidal tensor
that distributes over the tensor modeling conjunction.

The system as a whole relies on treating all these as operations on the same
underlying set, and indeed considering their interaction. Outside of models of
untyped systems, it is hard to account for all this; within the untyped (or
strictly reflexive) setting it is more algebraically natural, but still
category-theoretically disturbing.

Such notational abuse allows us to write down the following

######  Proposition 45.

Let $({\mathcal{C}},\otimes,s_{\\_,\\_},a_{\\_,\\_,\\_},Tr_{\\_,\\_}^{-})$ be
a symmetric traced monoidal category, and let $N=N\otimes N\in
Ob({\mathcal{C}})$ be a (non-unit) strictly self-similar object.
$({\mathcal{C}}(N,N),\otimes)$ is then a semi-monoidal monoid; for simplicity,
let us denote its underlying set by $M$, its composition by $\cdot$, its
tensor by $\otimes$, and its canonical associativity isomorphism & inverse by

$\tau=a_{N,N,N}\in{\mathcal{C}}(N\otimes(N\otimes N),(N\otimes N)\otimes
N)={\mathcal{C}}(N,N)$

and

$\tau^{\prime}=a^{-1}_{N,N,N}\in{\mathcal{C}}((N\otimes N)\otimes
N,N\otimes(N\otimes N))={\mathcal{C}}(N,N)$

and its canonical symmetry isomorphism by

$\sigma=s_{N,N}\in{\mathcal{C}}(N\otimes N,N\otimes N)={\mathcal{C}}(N,N)$

In the compact closed category $({\bf Int{\mathcal{C}}},\Box)$, the object
$(N,N)$ is strictly reflexive, and its endomorphism monoid is a semi-monoidal
monoid with underlying set $M$. Let us denote its composition by $\circ$, its
tensor by $\Box$, its canonical associativity isomorphism & inverse by
$T,T^{\prime}\in M$ and its symmetry isomorphism by $S\in M$.

The following are then immediate :

  1. 1.

$(M,\circ)$ and $(M,\cdot)$ share the same identity element, $1_{M}$.

  2. 2.

$T=\tau\otimes\tau^{-1}$

  3. 3.

$S=\sigma\otimes\sigma$

  4. 4.

The functions $(1\otimes\\_),(\\_\otimes 1):(M,\cdot)\rightarrow(M,\cdot)$ are
homomorphic self-embeddings of the monoid $(M,\cdot)$.

  5. 5.

The functions $(1\Box\\_),(\\_\Box 1):(M,\circ)\rightarrow(M,\circ)$ are
homomorphic self-embeddings of the monoid $(M,\circ)$.

  6. 6.

The functions $(1\otimes\\_),(\\_\otimes 1):(M,\cdot)\rightarrow(M,\circ)$ are
homomorphic and anti-homomorphic monoid embeddings respectively.

  7. 7.

The subset $\\{\tau,\tau^{\prime}\\}\subseteq M$ generates, by closure under
the composition $\cdot$ and the tensor $\otimes$, a subgroup of $(M,\cdot)$
isomorphic to Thompson’s group $\mathcal{F}$.

  8. 8.

The subset
$\\{T,T^{\prime}\\}=\\{\tau\otimes\tau^{\prime},\tau^{\prime}\otimes\tau\\}\subseteq
M$ generates, by closure under the composition $\circ$ and the tensor $\Box$,
a subgroup of $(M,\circ)$ isomorphic to Thompson’s group $\mathcal{F}$.

###### Proof.

Part 1. is immediate from the definition of the $\bf Int$ construction, and
parts 2. - 3. are similarly immediate from Lemma 36. Parts 4. and 5. are
general results on semi-monoidal monoids found in [31]. Part 6. is derived
from Proposition 38. Finally, parts 7. and 8. are immediate from Theorem 23. ∎

We now move on to horrify further the categorically-minded reader, and
consider some interactions between the canonical isomorphisms for $\star$, and
the tensor $\Box$ and composition $\circ$. Doing so leads us to the (rather
categorically respectable) theory of Frobenius algebras, as well as monoids
derived from Frobenius algebras that have close connections with classic
structures from both group and semigroup theory.

######  Remark 46.

As indicated in Footnote 9., we may consider the composition, tensor, dual,
etc. derived from Abramsky’s GoI construction, rather than Joyal, Street, &
Verity’s $\bf Int$ construction, as yet another collection of operations on
the same underlying set – together with a non-trivial bijection of the
underlying set that will map between the two.

In the following sections, we consider the interactions between the
composition, tensor, and canonical isomorphisms of the underlying traced
monoidal category with those of the derived from the $\bf Int$ construction.
We could of course do the same with the operations derived from the $\bf GoI$
construction instead, and derive an entirely distinct (& similarly
interesting) set of non-trivial interactions.

This brings us to another reason for using the conventions of [40] instead of
those of [1] – we derive a more direct route to an interesting class of
Frobenius algebras & monoids introduced by Abramsky & Heunen in [7].

###  10.2 Reflexivity and (unitless) Frobenius algebras & monoids

As well as the fundamental rôle of compact closure in Abramsky & Coecke’s
categorical quantum mechanics program [5], another key building block is the
(closely connected – see Proposition 50) notion of a Frobenius algebra. Beyond
their well-known applications in quantum field theory [37], in quantum
information they model fan-out operations [61] in quantum circuits, and play
the rôle of orthonormal bases in purely categorical formulations [14, 15] of
quantum foundations.

In stark contrast to compact closure itself, the notion of a ‘unitless
Frobenius algebra’ is well-established, both in terms of theory and examples.
These were defined and studied by S. Abramsky and C. Heunen in [7], from where
the following definition (but not terminology) is taken :

######  Definition 47.

Let $(\mathcal{C},\otimes,\alpha_{\\_,\\_,\\_})$ be a semi-monoidal category.
An Abramsky-Heunen or A-H Frobenius algebra $\mathcal{F}=(S,\Delta,\nabla)$ in
$\mathcal{C}$ consists of an object $S\in Ob({\mathcal{C}})$, equipped with an
associative split arrow $\Delta:S\rightarrow S\otimes S$ and a co-associative
merge arrow $\nabla:S\otimes S\rightarrow S$. These are required to satisfy
the Frobenius condition

$(1_{S}\otimes\nabla)\alpha_{S,S,S}^{-1}(\Delta\otimes
1_{S})=\Delta\nabla=(\nabla\otimes 1_{S})\alpha_{S,S,S}(1_{S}\otimes\Delta)$

Explicitly, associativity and co-associativity are the requirements that

  * •

$\nabla(1_{S}\otimes\nabla)=\nabla(\nabla\otimes 1_{S})\alpha_{S,S,S}$

  * •

$(1_{S}\otimes\Delta)\Delta=\alpha_{S,S,S}((\Delta\otimes 1_{S})\Delta)$.

Every Frobenius algebra is – by definition – an A-H Frobenius algebra, but the
converse is not true. In particular, as the above definition does not mention
the unit object, there are therefore no obstacles to considering A-H Frobenius
algebras whose distinguished object is the unique (non-unit) object of a semi-
monoidal monoid.

######  Definition 48.

Let $(M,\star,\alpha)$ be a semi-monoidal monoid, and let $\Delta$ and
$\nabla$ be the split and merge arrows of an A-H Frobenius algebra at the
unique object of this monoid. We define its A-H Frobenius or A-H F monoid to
be the semi-monoidal submonoid of $(M,\star)$ generated by the closure of
$\\{\alpha,\alpha^{-1},\Delta,\nabla\\}$ under composition and tensor.

######  Remark 49 (Another variation of terminology).

It is more standard to refer to the ‘split’ and ‘merge’ arrows of a Frobenius
algebra as the co-monoid and monoid arrows respectively. We do not do this, in
order to avoid the potentially fatal confusion of terminology that would
result.

An interesting class of examples of Frobenius algebras is given by the
following well-known result :

######  Theorem 50.

For every object $X$ of a compact closed category
$({\mathcal{C}},\\_\otimes\\_,\sigma_{\\_,\\_},I,\epsilon\\_,\eta\\_)$, the
object $X^{*}\otimes X$ is self-dual and there is a Frobenius algebra (the
canonical Frobenius algebra) at $X\otimes X^{*}$ with distinguished arrows
$\Delta$ and $\nabla$ given by the following composites:

$\textstyle{X^{*}\otimes
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\textstyle{X^{*}\otimes
I\otimes
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{X}^{*}\otimes\eta_{X}\otimes
1_{X}}$$\textstyle{X\otimes X^{*}\otimes X^{*}\otimes X}$

and

$\textstyle{X^{*}\otimes X\otimes X^{*}\otimes
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{X^{*}}\otimes\epsilon_{X}\otimes
1_{X}}$$\textstyle{X^{*}\otimes I\otimes
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\cong}$$\textstyle{X^{*}\otimes
X}$

###### Proof.

We refer to, for example, [58] for a direct proof of this, but note that it
follows abstractly from a more general result of [46], where it is proved for
any object with an ambidextrous adjunction – with the self-dual compact closed
case following as a special case. ∎

######  Corollary 51.

In Theorem 50 above, $\nabla\Delta\cong 1_{X^{*}\otimes X}\otimes\mu$ for some
abstract scalar $\mu\in{\mathcal{C}}(I,I)$, and hence when
$({\mathcal{C}},\otimes,I)$ has trivial scalars $\nabla\Delta=1_{X^{*}\otimes
X}$. However, this is a one-sided, rather than two-sided inverse.

###### Proof.

The composite $\nabla\Delta\cong 1_{X^{*}\otimes X}$ differs from the identity
on $X^{*}\otimes X$ by the composite of a unit and a co-unit (i.e. a closed
loop) in a compact closed category. Therefore, by [2], it is the identity up
to an abstract scalar, and is precisely the identity when the monoid of
scalars is trivial. To see why it is not a two-sided inverse, note that were
this to be the case, every self-dual object of any compact closed category
would be self-similar & hence reflexive. ∎

######  Definition 52.

Let $N\cong X\otimes X^{*}$ be a self-dual object of a compact closed category
${\mathcal{C}}$ . We refer to the A-H Frobenius algebra at $N$ given by
Theorem 50 above as the standard A-H Frobenius algebra at $N$.

In the case where $N$ is a strictly reflexive object of ${\mathcal{C}}$, we
observe that the endomorphism monoid of $N$ is a semi-monoidal monoid, and
therefore (following Definition 48) contains an A-H Frobenius monoid. We refer
to this as the standard A-H F. monoid at $N$. When ${\mathcal{C}}$ also has
trivial scalars, we refer to this as the simple A-H F monoid.

######  Conjecture.

We conjecture that “non-degenerate standard A-H Frobenius monoids differ only
by their scalars”. More precisely, but less generally, all (non-abelian)
simple A-H F. monoids are isomorphic.

The simple A-H F monoid is worth studying as much for its algebra as its
category theory. The following places it in the mainstream of semigroup theory
and group theory, as we demonstrate in Section 10.3.

######  Lemma 53.

Let $N$ be a strictly reflexive object of a compact closed category
$({\mathcal{C}},\otimes,t_{\\_,\\_,\\_})$ with trivial units. Then the split &
merge maps $\Delta,\nabla\in{\mathcal{C}}(N,N)$ of the simple A-H F monoid
satisfy:

  1. 1.

$\nabla\Delta=1_{N}$

  2. 2.

$\Delta\nabla=1_{N}$ iff $N$ is the unit object.

###### Proof.

Part 1. is immediate from Corollary 51 above. For part 2., let denote
$t_{N,N,N}\in{\mathcal{C}}(N,N)$ by $\alpha$, and assume that the inverse of
part 1. is a two-sided inverse. In this case, the associativity axiom,
$\nabla(1\otimes\nabla)=\nabla(\nabla\otimes 1)\alpha$ implies
$(1\otimes\nabla)=(\nabla\otimes 1)\alpha$, giving
$\alpha=\Delta\otimes\nabla$. Similarly, the co-associativity axiom implies
$\alpha=\nabla\otimes\Delta$ and so $\alpha=\alpha^{-1}$. Therefore,
associativity at this semi-monoidal monoid is strict. By Proposition 20 this
is the case iff $N$ is the unit object. ∎

In certain cases (including those arising from the strictification of
reflexivity procedure described in Theorem 44), we are able to give an
explicit description of the standard A-H F monoid at a strictly reflexive
object. The key to this is that in the case where the compact closed category
of Theorem 50 above arises from the $\bf Int$ construction, the split and
merge arrows have a particularly neat form :

######  Proposition 54.

Let $(C,\otimes,\alpha_{\\_,\\_,\\_},\sigma_{\\_,\\_})$ be a traced symmetric
monoidal category. Then the defining split and merge arrows of the standard
Frobenius algebra at a self-dual object $(N,N)\cong(N,I)\Box(I,N)\in Ob({\bf
Int{\mathcal{C}}})$,

$\Delta\in{\bf Int{\mathcal{C}}}((N,N),(N,N)\Box(N,N))\ =\
{\mathcal{C}}(N\otimes(N\otimes N),(N\otimes N)\otimes N)$

and

$\nabla\in{\bf Int{\mathcal{C}}}((N,N)\Box(N,N),(N,N))\ =\ C((N\otimes
N)\otimes N,N\otimes(N\otimes N))$

are given by the symmetry and associativity isomorphisms of the underlying
traced category, as

  * •

$\Delta\ =\ \alpha_{N,N,N}(1\otimes\sigma_{N,N})$

  * •

$\nabla\ =\ (1\otimes\sigma_{N,N})\alpha_{N,N,N}^{-1}$

respectively.

###### Proof.

This is immediate, and simply follows from substituting in the definitions of
the unit / co-unit maps of $\bf Int{\mathcal{C}}$ into the definitions of
Theorem 50. ∎

######  Remark 55.

The above observation, although simple, breaks the connection between the
standard Frobenius algebra at a self-dual object of $\bf Int{\mathcal{C}}$ and
the distinguished unit / co-unit maps – and hence, the unit object. Instead,
the standard Frobenius algebra is simply derived from the canonical
isomorphisms of the underlying traced symmetric monoidal category
${\mathcal{C}}$. This will of course be key to writing down the generators of
the standard A-H F monoid(s) of Definition 52.

######  Theorem 56.

Let $({\mathcal{C}},\otimes,s_{\\_,\\_},a_{\\_,\\_,\\_},Tr_{\\_,\\_}^{-})$ be
a symmetric traced monoidal category, and let $N=N\otimes N\in
Ob({\mathcal{C}})$ be a (non-unit) strictly self-similar object. We follow the
conventions & notation of Proposition 45, and denote the underlying set of
${\mathcal{C}}(N,N)={\bf Int{\mathcal{C}}}((N,N),(N,N))$ by $M$, along with
the two semi-monoidal monoid structures on it given by

  * •

(From the underlying traced category) $(M,\cdot,\otimes,\tau,\sigma)$

  * •

(From the compact closed category) $(M,\circ,\Box,T,S)$.

Let us denote the inverse of $\tau\in(M,\cdot)$ by
$\tau^{\prime}\in(M,\cdot)$.Then the standard A-H Frobenius monoid is the
monoid generated by the closure of the set

$\\{\tau\cdot(1\otimes\sigma)\ ,\ (1\otimes\sigma)\cdot\tau^{\prime}\ ,\
\tau\otimes\tau^{\prime}\ ,\ \tau^{\prime}\otimes\tau\\}$

under the composition $\circ$ and tensor $\Box$.

###### Proof.

From Proposition 54, the split and merge arrows are given by
$\Delta=\tau\cdot(1\otimes\sigma)$ and
$\nabla=(1\otimes\sigma)\cdot\tau^{\prime}$ respectively. The associator for
$\\_\Box\\_$ and its inverse are given by $T=\tau\otimes\tau^{\prime}$ and
$T^{\prime}=\tau^{\prime}\otimes\tau$ respectively. These primitives then, by
definition, generate the standard A-H Frobenius monoid, and satisfy the
Frobenius condition

$(1\Box\nabla)\circ T^{\prime}\circ(\Delta\Box 1)\ =\ \Delta\circ\nabla\ =\
(\nabla\Box 1)\circ T(1\Box\Delta)$

along with associativity and co-associativity

  * •

$\nabla\circ(1\Box\nabla)=\nabla\circ(\nabla\Box 1)\circ T$

  * •

$(1\Box\Delta)\circ\Delta=((\Delta\Box 1)\circ\Delta)\circ T$.

∎

###  10.3 Algebraic aspects

The standard A-H F monoid at a strictly reflexive object contains, by
construction, all canonical associativity isomorphisms of the semi-monoidal
endomorphism monoid; it therefore (by Theorem 23) contains a copy of
Thompson’s iconic group $\mathcal{F}$. We now demonstrate that the simple case
also contains a copy of one of the most iconic structures from semigroup
theory – the bicyclic monoid. Further, there is a very natural way in which
the simple A-H F monoid may be thought of as, “interacting copies of the
bicyclic monoid, and Thompson’s $\mathcal{F}$”.

The following was first published in [50], but appears previously to have been
known by Clifford, Preston, & Rees (see [33] for a historical overview).

######  Definition 57.

The bicyclic monoid $\bf B$ is the monoid with two generators, and a single
relation

${\mathcal{B}}\ =\ \langle s,r\ :\ rs=1\rangle$

(Note that this is a one-sided inverse, and certainly does not imply that
$sr=1$)!

It is remarkably well-studied, and appears in a wide range of algebraic and
computational settings. Its theory is very well-established; the following
results may be found in, for example, [48].

######  Theorem 58.

  1. 1.

$\mathcal{B}$ is an inverse monoid, and is isomorphic to the inverse monoid of
partial injections on the natural numbers generated by the successor function
and its (partially defined) inverse.

  2. 2.

Given an arbitrary monoid $M$, and a pair of elements $r,s\in M$ satisfying
$rs=1\neq sr$, then the submonoid generated by $\\{r,s\\}$ is isomorphic to
$\mathcal{B}$.

  3. 3.

The elements of $\mathcal{B}$ may be given a normal form as pairs of natural
numbers, with composition given by, for all
$(d,c),(b,a)\in\mathbb{N}\times\mathbb{N}$

$(d,c)(b,a)\ =\
\left(d+[b\stackrel{{\scriptstyle\bullet}}{{-}}c],[c\stackrel{{\scriptstyle\bullet}}{{-}}b]+a\right)$

where the monus operation $\stackrel{{\scriptstyle\bullet}}{{-}}$ is defined
by
$y\stackrel{{\scriptstyle\bullet}}{{-}}x=\left\\{\begin{array}[]{lr}y-x&x\leq
y\\\ 0,&\mbox{otherwise.}\end{array}\right.$

######  Remark 59.

It is hard to avoid seeing the bicyclic monoid itself as a categorical
structure. It is well-known that the natural numbers with the usual ordering
forms a (posetal) category, and addition is a (strictly symmetric &
associative) monoidal tensor on this category, with the unit object simply
being $0\in\mathbb{N}$. Further, it is straightforward that $\mathbb{N}$ is a
closed monoidal category, with the internal hom given by the above monus
operation,
$y\stackrel{{\scriptstyle\bullet}}{{-}}x=\left\\{\begin{array}[]{lr}y-x&x\leq
y\\\ 0,&\mbox{otherwise.}\end{array}\right.$

The bicyclic monoid then has all the appearance of being the result of a
‘dualising’ construction on this monoidal closed category. It may also be
relevant that $(\mathbb{N},+,0)$ is traced, with the trace given on objects by
subtraction.

######  Theorem 60.

Let $N$ be a (non-unit) strictly reflexive object of a compact closed category
$({\mathcal{C}},\otimes,t_{\\_,\\_,\\_},s_{\\_,\\_},I)$ with trivial scalars.
Then ${\mathcal{C}}(N,N)$ is a semi-monoidal monoid containing a copy of the
simple A-H F monoid, which we denote $\mathbb{A}\subseteq{\mathcal{C}}(N,N)$.
Then

  1. 1.

$\mathbb{A}$ is generated by the closure under composition and tensor of :

     * •

The associator $\alpha=t_{N,N,N}$ and its inverse $\alpha^{-1}$.

     * •

The split map $\Delta$ and its generalised inverse $\nabla$.

  2. 2.

The associator and its inverse generate (by closure under composition &
tensor), a copy of Thompson’s $\mathcal{F}$ within $\mathbb{A}$.

  3. 3.

The split element $\Delta$ and its generalised inverse $\nabla$ generate (by
closure under composition) a copy of the bicyclic monoid $\mathcal{B}$ within
$\mathbb{A}$.

###### Proof.

Part 1. is simply the definition of the simple A-H F monoid at $N$. Part 2.
follows directly from Theorem 23. From Corollary 51, the split and merge
arrows of the simple A-H F monoid satisfy $\nabla\Delta=1$ and
$\Delta\nabla\neq 1$, and from Part 2. of Theorem 58, they therefore generate
a copy of the bicyclic monoid. ∎

##  11 Concrete examples

We now move on from the abstract theory of strict extensional reflexivity to
concrete examples. These have been separated out from the theoretical
constructions, in order to emphasise that the theory is generally applicable,
and not tied to any specific example.

The concrete setting we now consider it that of Girard’s original two Geometry
of Interaction papers [21, 22] (and indeed Abramsky, Haghverdi, & Scott’s
linear combinatory logic [6]). The starting point for this is the (inverse)
traced monoidal category of partial injections, considered as a traced
monoidal subcategory of an illustrative example of Joyal, Street, and Verity.

###  11.1 The category of relations, its matrix calculus, and its trace

In [40], Joyal, Street, and Verity used the monoidal category of relations
with disjoint union as a canonical example of a traced, but not compact
closed, category. Their treatment was based on writing relations in matrix
form.

######  Definition 61.

The category ${\bf Rel}$ of relations on sets has as objects all sets. An
arrow $R\in{\bf Rel}(X,Y)$ is a subset $R\subseteq Y\times X$. Given an arrow
$S\in{\bf Rel}(Y,Z)$, composition is given by the usual formula for relational
composition,

$(z,x)\in SR\ \ \mbox{ iff }\exists y\in Y\ :\ (z,y)\in S\ \mbox{ and }\
(y,x)\in R$

The category of relations also has a dagger $(\ )^{c}:{\bf
Rel}^{op}\rightarrow{\bf Rel}$, given by relational converse
$R^{c}=\\{(x,y):(y,x)\in R\\}$.

A partial function is a relation satisfying $(y,x),(z,x)\in R\Rightarrow y=z$,
and a partial injection is a partial function whose converse is also a partial
function. It is standard to write partial functions and partial injections in
functional form, as $f(x)=y$, rather than $(y,x)\in f$. Partial functions and
partial injections form wide subcategories of $\bf Rel$, denoted $\bf pFun$
and $\bf pInj$ respectively.

The category $\bf Rel$ also has a biproduct, the disjoint union
$\\_\uplus\\_:{\bf Rel}\times{\bf Rel}\rightarrow{\bf Rel}$ given by on
objects by disjoint union $A\uplus B=A\times\\{0\\}\cup B\times\\{1\\}$ and
extended to arrows in the obvious manner.

The biproduct structure implies the existence of projection and injection
arrows. For all $A,B\in Ob({\bf Rel})$, the projection arrows are the
following partial injections

  * •

$\pi_{0}=\\{(a,(a,0)):a\in A\\}\in{\bf Rel}(A\uplus B,A)$

  * •

$\pi_{1}=\\{(b,(b,1)):b\in B\\}\in{\bf Rel}(A\uplus B,B)$

and the injection arrows are their relational converses

  * •

$\iota_{0}=\\{((a,0),a):a\in A\\}\in{\bf Rel}(A,A\uplus B)$

  * •

$\iota_{1}=\\{((b,1),b):b\in B\\}\in{\bf Rel}(B,A\uplus B)$

Both $\bf pFun$ and $\bf pInj$ are closed under $\\_\uplus\\_$; however it is
simply a symmetric monoidal tensor on these subcategories and neither a
product nor a coproduct. In all three settings, the disjoint union has as unit
object the empty set $I=\\{\\}$, and hence a trivial monoid of scalars.

######  Remark 62 (Units, scalars, and strict associativity).

The unit object of $\bf Rel$ is not a strict unit; rather, $A\uplus
I=A\times\\{0\\}\cup\\{\\}\times\\{1\\}=A\times\\{0\\}\cong A$.

The unique arrow of the endomorphism monoid of $I$ is the nowhere-defined
function on the empty set, thus $\bf Rel$ and the distinguished monoidal
subcategories described above provide good examples of unit objects with
trivial scalars. The elements (i.e. arrows of the form $f:I\rightarrow X$) are
similarly uninteresting; they are the nowhere-defined partial injections whose
domain is the empty set. These categories will therefore illustrate how the
$\bf Int$ or $\bf GoI$ construction builds a rich structure of elements and
names that is essentially unrelated to that of the underlying traced category.

Note that disjoint union is associative up to canonical isomorphism, but is
not strictly associative. In [40], Joyal, Street,& Verity implicitly appeal to
MacLane’s strictification procedure for associativity & units [51], and work
within a suitably strictified version of $({\bf Rel},\uplus)$. As well as
eliminating repeated re-bracketings, this also provides the justification for
working with arbitrary (finite) matrices, as discussed below.

In our setting we need to be cautious of the result of [31], that we cannot
simultaneously strictify associativity and self-similarity (see also Section
5.2). Hence, following Section 9, we are not able to assume strict
associativity in a setting where we wish to find strictly reflexive objects –
at least, in the compact closed setting.

In the following sections we therefore do not assume strict associativity,
although canonical isomorphisms may occasionally be omitted for reasons of
clarity. We also restrict ourselves to $(2\times 2)$ matrices, and consider
larger matrices as “matrices of matrices”, with the precise interpretation
determined by the source / target objects.

###  11.2 Matrices of relations

The following is well-established, and is a corollary of the biproduct
structure described above. It is also heavily used in [40].

######  Proposition 63.

Given arbitrary $F\in{\bf Rel}(A\uplus B,P\uplus Q)$, then $F$ uniquely
determines & is uniquely determined by a $2\times 2$ matrix of relations
$[f_{ij}]_{i,j\in\\{0,1\\}}$ whose entries are given in terms of the
projection / injection arrows by $f_{ij}=\pi_{i}F\iota_{j}$. it is standard to
abuse notation and write $\small F=\left(\begin{array}[]{cc}f_{00}&f_{01}\\\
f_{10}&f_{11}\end{array}\right)$. The composite of relations in matrix form is
then given by the usual formula for matrix composition, with addition and
multiplication interpreted by union and relational composition respectively:

$\left(\begin{array}[]{ccc}g_{00}&&g_{01}\\\
g_{10}&&g_{11}\end{array}\right)\left(\begin{array}[]{ccc}f_{00}&&f_{01}\\\
f_{10}&&f_{11}\end{array}\right)=\left(\begin{array}[]{ccc}g_{00}f_{00}\cup
g_{01}f_{10}&&g_{11}f_{11}\cup g_{10}f_{01}\\\ g_{10}f_{00}\cup
g_{11}f_{10}&&g_{11}f_{11}\cup g_{10}f_{01}\end{array}\right)$

This may also be drawn via the usual ‘summing over paths’ description of
matrix composition where these matrices are drawn as digraphs:

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{00}}$$\scriptstyle{f_{10}}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{00}}$$\scriptstyle{g_{10}}$$\textstyle{X}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{11}}$$\scriptstyle{f_{01}}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{11}}$$\scriptstyle{g_{01}}$$\textstyle{Y}$

and matrix composition interprets as ‘summing over paths from source to
target’:

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{00}f_{00}\cup
g_{01}f_{10}}$$\scriptstyle{g_{10}f_{00}\cup
g_{11}f_{10}}$$\textstyle{X}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{11}f_{11}\cup
g_{10}f_{01}}$$\scriptstyle{g_{00}f_{01}\cup g_{01}f_{11}}$$\textstyle{Y}$

###### Proof.

[Outline] This is very well-established, and the formula for matrix
composition may be derived from the observation that the composite of a
projection and an injection acts like a Kronecker delta, so $\pi_{j}\iota_{i}\
=\ \left\\{\begin{array}[]{lcr}0&&i\neq j\\\ 1&&i=j\end{array}\right.$ ∎

The category $\bf Rel$ was used as an illustration of a traced symmetric
monoidal category in [40], and the structure of the resulting compact closed
category $\bf Int(Rel)$ was also described in detail. The following, from this
reference, is key:

######  Theorem 64.

The category $({\bf Rel},\uplus)$ is traced, with the trace defined in terms
of the reflexive transitive closure of relations. Given
$F=\left(\begin{array}[]{cc}f_{00}&f_{01}\\\
f_{10}&f_{11}\end{array}\right):X\uplus U\rightarrow Y\uplus U$, then

$Tr_{X,Y}^{U}(F)\ =\ f_{00}\cup
f_{01}\left(\bigcup_{j=0}^{\infty}f_{11}^{j}\right)f_{10}$

###### Proof.

The proof that this operation satisfies the axioms of Definition 33 is given
in [40], and relies heavily on the properties of the Kleene star (i.e.
reflexive transitive closure) of relations in endomorphism monoids. ∎

######  Remark 65.

In [1], concrete examples of categorical traces were described as belonging to
one of two classes : either ‘particle-style’ (based on iteration or feedback),
or ‘wave-style’ (based on fixed-points). The above trace on $({\bf
Rel},\uplus)$ is the canonical example of a particle-style trace.

##  12 A matrix formalism for partial injections

As they are monoidal subcategories of $({\bf Rel},\uplus)$, both $({\bf
pFun},\uplus)$ and $({\bf pInj},\uplus)$ admit matrix representations of
arrows. However, unlike $\bf Rel$, their homsets are not closed under
arbitrary unions, so some care is needed when using a matrix formalism. The
case of partial functions was covered by Manes & Arbib in their study of
algebraic program semantics [8], and based on this, necessary and sufficient
conditions for a matrix of partial injections to represent a partial injection
was given in [26].

######  Proposition 66.

Given $X,V,Y,U\in Ob({\bf pInj})$, the matrix representations of partial
injections in ${\bf pInj}(X\uplus V,Y\uplus U)$ are precisely those matrices
$\small\left(\begin{array}[]{cc}a&b\\\ c&d\end{array}\right)$ whose entries
are partial injections such that the following diagrams commute:

$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c^{\ddagger}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{b}$$\scriptstyle{0_{XV}}$$\textstyle{Y}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\textstyle{V}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d^{\ddagger}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{b^{\ddagger}}$$\scriptstyle{d^{\ddagger}}$$\scriptstyle{0_{UY}}$

###### Outline.

This was first proved in [26]. The key points of this proof are given below,
in order to give some insight into the structure of matrix representations
within $\bf pInj$.
The starting point is the observation that, given a family of partial
injections $\\{f_{j}\\}_{j\in J}\in{\bf pInj}(X,Y)$, their union
$\bigcup_{j\in J}f_{j}\in{\bf Rel}(X,Y)$ is a partial injection iff
$f_{i}^{\ddagger}f_{j}$ and $f_{i}g_{j}^{\ddagger}$ are idempotent, for all
$i,j\in J$. An important special case is when $f_{i}^{\ddagger}f_{j}=0_{X}$
and $f_{i}f_{j}^{\ddagger}=0_{Y}$, so $f_{i}\cap f_{j}=\emptyset$, and hence
the union $\bigcup_{j\in J}f_{j}$ is trivially a partial injection.

Now consider the above matrix of partial injections. The commutativity of the
above two diagrams is equivalent (up to the appropriate inclusions) to this
condition. In the other direction, the projection / injection arrows impose
this condition when writing down the matrix form of a partial injection. ∎

######  Definition 67.

The above condition is sometimes known as the rook matrix condition, since it
states that elements in the same row of a matrix have disjoint images, and
elements in the same column have disjoint domains. This description is more
useful for matrix calculations within $\bf pInj$, but the characterisation as
commuting squares is more useful when working with the compact closed category
$\bf Int(pInj)$.

We therefore refer to a square
$\textstyle{Y}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{b}$$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c}$$\scriptstyle{d}$$\textstyle{U}$
of arrows in $\bf pInj$ as a rook square when the two diagrams of Proposition
66 above commute.

As a corollary of the above characterisation, it was shown in [26] that $({\bf
pInj},\uplus)$ is closed under the trace described in Theorem 64.

######  Theorem 68.

The symmetric monoidal category $({\bf pInj},\uplus)$ is traced, with the
trace given by

$Tr^{U}_{X,Y}\left(\begin{array}[]{cc}f_{00}&f_{01}\\\
f_{10}&f_{11}\end{array}\right)\ =\
f_{00}\cup\bigcup_{j=0}^{\infty}\left(f_{01}f_{11}^{j}f_{10}\right)$

###### Proof.

This was first given in [26], but also proved independently in [24, 61, 6]. ∎

######  Remark 69.

Unlike the case of $\bf Rel$, it is inaccurate to write the above trace in
$\bf pInj$ in terms of the Kleene star, as $f_{00}\cup
f_{01}\left(\bigcup_{j=0}^{\infty}f_{11}^{j}\right)f_{10}$. The reflexive
transitive closure $\left(\bigcup_{j=0}^{\infty}f_{11}^{j}\right)$ is in
general simply a relation, and not a partial injection.

##  13 The compact closed category $\bf Int(pInj)$

We now describe the compact closed category that results from applying Joyal,
Street, & Verity’s $\bf Int$ construction to the traced category $({\bf
pInj},\uplus)$ of partial injections. We emphasise that this is simply the
explicit description of $\bf Int(Rel)$, as found in [40], restricted to the
traced symmetric monoidal subcategory of partial injections.

######  Definition 70.

Plugging in the traced monoidal category $(\bf pInj,\uplus)$ into the $\bf
Int$ construction of [40] gives the following:

Objects

These are pairs of objects of $\bf pInj$ (i.e. pairs of sets).

Arrows

Homsets are given by ${\bf Int(pInj)}((X,U),(Y,V))={\bf pInj}(X\uplus
V,Y\uplus U)$. Arrows of ${\bf pInj}(X\uplus V,Y\uplus U)$ are given as
$(2\times 2)$ matrices of partial injections satisfying the rook matrix
condition such as $\left(\begin{array}[]{cc}f_{00}&f_{01}\\\
f_{10}&f_{11}\end{array}\right)\in{\bf Rel}(X\uplus V,Y\uplus U)$. Following
[Joyal et al. 96], we draw the corresponding arrow of ${\bf
Int(pInj)}((X,U),(Y,V))$ as a (planar) graphical 4-tuple of partial injections
satisfying the rook square condition (Definition 67), as follows:
$\textstyle{Y}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{00}}$$\scriptstyle{f_{10}}$$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{01}}$$\scriptstyle{f_{11}}$$\textstyle{U}$
.

Composition

To compose such digraphs, we simply glue then along their common edge,
followed by taking the union over all paths with identical source & target:

$\textstyle{Z}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{00}}$$\scriptstyle{g_{10}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{00}}$$\scriptstyle{f_{10}}$$\textstyle{Z}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\bigcup_{j=0}^{\infty}g_{00}\left(f_{01}g_{10}\right)^{j}f_{00}}$$\scriptstyle{f_{10}\cup\
\bigcup_{j=0}^{\infty}f_{11}g_{10}\left(f_{01}g_{10}^{j}\right)f_{00}}$$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{01}}$$\scriptstyle{g_{11}}$$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{01}}$$\scriptstyle{f_{11}}$$\textstyle{U}$$\textstyle{W\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{01}\cup\
\bigcup_{j=0}^{\infty}g_{00}f_{01}\left(g_{10}f_{01}^{j}\right)g_{11}}$$\scriptstyle{\bigcup_{j=0}^{\infty}f_{11}\left(g_{01}f_{10}\right)^{j}g_{11}}$$\textstyle{U}$

Monoidal tensor

The tensor $\\_\Box\\_$ is defined on objects by
$(X,U)\Box(X^{\prime},U^{\prime})=(X\uplus X^{\prime},U^{\prime}\uplus U)$ and
on arrows by:

$\vbox{ \vbox{ \small\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
8.70375pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{Y}$}}}}}}}{\hbox{\kern 30.625pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.18806pt\raise 4.35625pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.35625pt\hbox{$\scriptstyle{a}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.6125pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
37.70624pt\raise-18.07498pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.35625pt\hbox{$\scriptstyle{c}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
37.70624pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.1875pt\hbox{$\scriptstyle{b}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.2136pt\raise-41.33746pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.1875pt\hbox{$\scriptstyle{d}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
31.14313pt\raise-36.14996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.14313pt\raise-36.14996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{U}$}}}}}}}\ignorespaces}}}}\ignorespaces} }\
{\large{\Box}}\ \vbox{ \vbox{ \small\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
9.69374pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{Y^{\prime}}$}}}}}}}{\hbox{\kern 31.318pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.38606pt\raise 4.85625pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.85625pt\hbox{$\scriptstyle{a^{\prime}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 7.3055pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
39.09222pt\raise-18.77498pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.85625pt\hbox{$\scriptstyle{c^{\prime}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
39.09222pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{V^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.6875pt\hbox{$\scriptstyle{b^{\prime}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.41159pt\raise-43.23746pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.6875pt\hbox{$\scriptstyle{d^{\prime}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
31.83612pt\raise-37.54996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.83612pt\raise-37.54996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{U^{\prime}}$}}}}}}}\ignorespaces}}}}\ignorespaces} }\
=\ \vbox{ \vbox{ \small\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.293pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{Y\uplus Y^{\prime}}$}}}}}}}{\hbox{\kern
67.89304pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{X\uplus
X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
27.58153pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-2.59721pt\hbox{$\scriptstyle{\tiny\left(\begin{array}[]{cc}a&0\\\
0&a^{\prime}\end{array}\right)}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
16.293pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
70.45435pt\raise-26.87495pt\hbox{\hbox{\kern
0.0pt\raise-2.59721pt\hbox{$\scriptstyle{\tiny\left(\begin{array}[]{cc}0&c^{\prime}\\\
c&0\end{array}\right)}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
85.12352pt\raise-43.19994pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{V^{\prime}\uplus
V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise-3.24405pt\hbox{$\scriptstyle{\tiny\left(\begin{array}[]{cc}0&b\\\
b^{\prime}&0\end{array}\right)}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-4.79999pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
27.62202pt\raise-53.74991pt\hbox{\hbox{\kern
0.0pt\raise-3.24405pt\hbox{$\scriptstyle{\tiny\left(\begin{array}[]{cc}d^{\prime}&0\\\
0&d\end{array}\right)}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
69.9293pt\raise-53.74991pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
69.9293pt\raise-53.74991pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{U^{\prime}\uplus
U}$}}}}}}}\ignorespaces}}}}\ignorespaces} }$

The unit object

This is simply the object $(\emptyset,\emptyset)$.

The dual

The contravariant dual $(\ )^{*}:{\bf Int(pInj)}^{op}\rightarrow{\bf
Int(pInj)}$ is defined on objects by $(X,U)^{*}=(U,X)$, and on arrows by
$\left(\vbox{ \vbox{ \small\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
8.70375pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{Y}$}}}}}}}{\hbox{\kern 30.625pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.18806pt\raise 4.35625pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.35625pt\hbox{$\scriptstyle{a}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.6125pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
37.70624pt\raise-18.07498pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.35625pt\hbox{$\scriptstyle{c}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
37.70624pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.1875pt\hbox{$\scriptstyle{b}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.2136pt\raise-41.33746pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.1875pt\hbox{$\scriptstyle{d}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
31.14313pt\raise-36.14996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.14313pt\raise-36.14996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{U}$}}}}}}}\ignorespaces}}}}\ignorespaces} }\right)^{*}\
\ {\large=}\ \ \vbox{ \vbox{ \small\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
8.72636pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{U}$}}}}}}}{\hbox{\kern 31.08124pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{V\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.2136pt\raise 5.1875pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.1875pt\hbox{$\scriptstyle{d}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.56311pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
37.70624pt\raise-18.07498pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.1875pt\hbox{$\scriptstyle{b}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
37.70624pt\raise-26.99998pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.35625pt\hbox{$\scriptstyle{c}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 0.0pt\raise-3.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.18806pt\raise-40.50621pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.35625pt\hbox{$\scriptstyle{a}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern
31.09373pt\raise-36.14996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
31.09373pt\raise-36.14996pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{Y}$}}}}}}}\ignorespaces}}}}\ignorespaces} }$ .

The compact closed structure

The unit and co-unit arrows for the compact closed structure,

$\eta_{(X,U)}:(\emptyset,\emptyset)\rightarrow(X,U)\Box(X,U)^{*}\ \mbox{ and
}\ \epsilon_{(X,U)}:(X,U)^{*}\Box(X,U)\rightarrow(\emptyset,\emptyset)$

are given by, respectively:

$\textstyle{X\uplus
U}$$\textstyle{\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{0}$$\scriptstyle{0}$$\textstyle{U\uplus
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{\tiny\left(\begin{array}[]{cc}0&1\\\
1&0\end{array}\right)}}$$\scriptstyle{0}$$\textstyle{\emptyset}$ and
$\textstyle{\emptyset}$$\textstyle{U\uplus
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{0}$$\scriptstyle{\tiny\left(\begin{array}[]{cc}0&1\\\
1&0\end{array}\right)}$$\textstyle{\emptyset\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{0}$$\scriptstyle{0}$$\textstyle{X\uplus
U}$

######  Remark 71.

[On the formulæ for composition]The seemingly intricate formula for the
composition of two rook squares arises in a very natural way from the
diagrammatic representation of matrix composition, described in Proposition
63.

Taking the ‘summing over paths’ intuition seriously, the formula for the trace
of $({\bf Rel},\uplus)$, and hence $({\bf pInj},\uplus)$, arises by
introducing a feedback loop to the matrix representation of an arrow, and
again summing over paths as shown :

$\textstyle{Y}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{U}}$$\textstyle{Y}$
giving :
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{c}$$\textstyle{U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{b}$$\scriptstyle{d}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a\cup\bigcup_{j=0}^{\infty}bd^{j}c}$

In $\bf pInj$, both composition and trace are given by ‘summing over paths’
constructions. Bringing these together gives the formula, and formalism, for
composition in $\bf Int(pInj)$; consider arrows $F:(X,U)\rightarrow(Y,V)$ and
$G:(Y,V)\rightarrow(Z,W)$ determined by rook matrices
$\tiny\left(\begin{array}[]{cc}f_{00}&f_{01}\\\
f_{10}&f_{11}\end{array}\right)$ and
$\tiny\left(\begin{array}[]{cc}g_{00}&g_{01}\\\
g_{10}&g_{11}\end{array}\right)$ respectively. The composite $GF\in{\bf
Int(pInj)}((X,U),(Z,W))$ is then given by summing over paths in the following
diagram :