# Classical Distributive Restriction Categories

Robin Cockett and Jean-Simon Pacaud Lemay

###### Abstract

In the category of sets and partial functions, $\mathsf{PAR}$, while the
disjoint union $\sqcup$ is the usual categorical coproduct, the Cartesian
product $\times$ becomes a restriction categorical analogue of the categorical
product: a restriction product. Nevertheless, $\mathsf{PAR}$ does have a usual
categorical product as well in the form $A\&B:=A\sqcup B\sqcup(A\times B)$.
Surprisingly, asking that a distributive restriction category (a restriction
category with restriction products $\times$ and coproducts $\oplus$) has
$A\&B$ a categorical product is enough to imply that the category is a
classical restriction category. This is a restriction category which has joins
and relative complements and, thus, supports classical Boolean reasoning. The
first and main observation of the paper is that a distributive restriction
category is classical if and only if $A\&B:=A\oplus B\oplus(A\times B)$ is a
categorical product in which case we call $\&$ the “classical” product.

In fact, a distributive restriction category has a categorical product if and
only if it is a classified restriction category. This is in the sense that
every map $A\allowbreak\mathrel{\mathop{\hbox
to11.99998pt{\rightarrowfill}}\limits}B$ factors uniquely through a total map
$A\allowbreak\mathrel{\mathop{\hbox
to11.99998pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$, where $\mathsf{1}$
is the restriction terminal object. This implies the second significant
observation of the paper, namely, that a distributive restriction category has
a classical product if and only if it is the Kleisli category of the exception
monad $\\_\oplus\mathsf{1}$ for an ordinary distributive category.

Thus having a classical product has a significant structural effect on a
distributive restriction category. In particular, the classical product not
only provides an alternative axiomatization for being classical but also for
being the Kleisli category of the exception monad on an ordinary distributive
category.

Acknowledgements. The authors would like to thank Masahito Hasegawa and RIMS
at Kyoto University for helping fund research visits so that the authors could
work together on this project. For this research, the first named author was
partially funded by NSERC, while the second named author was financially
supported by a JSPS Postdoctoral Fellowship, Award #: P21746.

We would like to dedicate this paper to Pieter Hofstra (1975-2022).

### From Robin:

I met Pieter in 2004, while I was visiting the University of Ottawa. I was
assigned a desk in the postdoc’s office of the math department and Pieter was
a postdoc there at the time. On the pretext that we would develop a
restriction categorical version of recursion theory, I persuaded Pieter to
come to Calgary. He actually did come and he was a postdoc in Computer Science
at the University of Calgary 2005-2007. Furthermore, we actually did introduce
a formulation of recursion theory in a restriction category which we called a
Turing category [4]. I am immensely proud of this foundational work. Pieter
brought an uncompromising high standard of exposition to the table … and a
deep understanding of recursion theory. We ended up writing a number of joint
papers some of which are still not finished. Much of our work together
involved restriction categories, which is, appropriately, the subject of this
paper.

Pieter, besides being a highly valued colleague, was a frequent visitor to our
home and he and his family became close friends to my wife, Polly, and I. He
is greatly missed.

### From JS:

Pieter played an important role in my life. Pieter was my first academic
mentor: he taught me category theory and I did my first research project with
him while I was an undergrad student at the University of Ottawa. In fact, the
last lecture of my undergrad was with Pieter, where he taught us how to kill
Hydras. Afterwards, Pieter became a great colleague and friend, with whom I
enjoyed spending time with whenever we crossed paths at conferences and
workshops. What I enjoyed most about Pieter is while we did have many
interesting discussions about math, we also had great discussions about
numerous other subjects during hikes or over food and drinks. Pieter will be
greatly missed by myself and many others. May he rest in peace.

###### Contents

  1. 1 Introduction
  2. 2 Distributive Restriction Categories
  3. 3 Classical Products
  4. 4 Classical Restriction Categories
  5. 5 From Classical Products to Restriction Products and Coproducts
  6. 6 Classical Distributive Restriction Categories
  7. 7 Classical Classification

##  1 Introduction

In the category of sets and partial functions, $\mathsf{PAR}$, it is well
known that while the disjoint union of sets $A\sqcup B$ is the coproduct, the
Cartesian product of sets $A\times B$ on the other hand is no longer a
categorical product. It is a curiosity that there is, nonetheless, a real
categorical product in $\mathsf{PAR}$ which takes the form $A\sqcup
B\sqcup(A\times B)$. This raises the general question of what properties are
required of a partial map category to come equipped with a categorical product
of this form.

To answer this question it is expedient to utilize the formulation of partial
map categories as restriction categories: these were introduced by Cockett and
Lack in [5]. Briefly, a restriction category (Def. 2.1) is a category equipped
with a restriction operator which associates to every map $f$ its restriction
$\overline{f}$, capturing the domain of definition of $f$. The main example of
a restriction category is $\mathsf{PAR}$ (Ex. 2.6), but there are also many
other interesting examples including the opposite category of commutative
algebras and _non-unital_ algebra morphisms (Ex. 2.7).

As mentioned, while in $\mathsf{PAR}$ the Cartesian product $\times$ is not a
categorical product, it is instead a restriction product (Def 2.3): this is
the restriction categorical analogue of a product which is, in fact, a lax
limit. This means that it is, in general, not a categorical product as it need
not be a strict limit. On the other hand, the notion of a restriction
coproduct $\oplus$ is a coproduct in the usual categorical sense (Def 2.4). A
_distributive_ restriction category (Def 2.5) is a restriction category with
both restriction products and coproducts, such that the restriction product
distributes over the coproduct in the sense that the natural map $(A\times
B)\oplus(A\times C)\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times(B\oplus C)$ is an isomorphism.

As was discussed in [7, Sec 4.3], there is no reason why a restriction
category should not possess a categorical product. In fact, it may be tempting
to think that in a distributive restriction category, $A\oplus B\oplus(A\times
B)$ will always be a categorical product. However, this is not so. Indeed, any
category is a restriction category with the trivial restriction operator where
for any map $f$, $\overline{f}$ is the simply identity on the domain of $f$.
Thus when a distributive restriction category has a trivial restriction, in
this sense, the restriction product $\times$ is already a categorical product
and it is not of the desired form. This means that the question of when a
distributive restriction category has ${A\oplus B\oplus(A\times B)}$ a
categorical product, is nontrivial. Surprisingly, as we shall see, demanding
that ${A\oplus B\oplus(A\times B)}$ be a categorical product forces a
distributive restriction category to be both _classical_ and _classified_.

Classical restriction categories were explored by Cockett and Manes in [8]. In
any restriction category there is a canonical partial order $\leq$ on parallel
maps (Def. 4.1). A restriction category is classical if it has joins (Def.
4.2) and relative complements (Def. 4.5) with respect to $\leq$. These are
both desirable notions to have in a restriction category as they allow for
Boolean classical reasoning. The main result of this paper is that a
distributive restriction category is classical if and only if $A\oplus
B\oplus(A\times B)$ is a categorical product (Thm. 6.8). Consequently, when
$A\oplus B\oplus(A\times B)$ is a categorical product we refer to it as a
_classical_ product, which we denote as $A\&B=A\oplus B\oplus(A\times B)$ to
distinguish it from the restriction product. This allows us to restate our
main result: a distributive restriction category is classical if and only if
it has classical products. To prove that a classical distributive restriction
category has classical products (Prop. 6.2), we use joins and complements of
restriction idempotents (Def. 4.8) to construct the necessary unique map
$C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$ for the universal property of the
product. Conversely, to show that having classical products implies being
classical (Prop. 6.7), we use the universal property of $\&$ to build the
joins and relative complements, and make use of the notion of decisions (Def.
6.3) in the proof. Thus classical products give a novel and somewhat
unexpected way of axiomatizing classical distributive restriction categories.

Important examples of distributive restriction categories are Kleisli
categories for the exception monad111The exception monad has been popularized
in Haskell as the “maybe” monad.. Indeed, recall that a distributive category
[1, 2] is a category $\mathbb{D}$ that has products $\times$ and coproducts
$\oplus$ (in the usual categorical sense) where $\times$ distributes over
$\oplus$. The exception monad of a distributive category $\mathbb{D}$ is the
monad defined on $\\_\oplus\mathsf{1}$, where $\mathsf{1}$ is the terminal
object. For any distributive category $\mathbb{D}$, the Kleisli category of
its exception monad, $\mathbb{D}_{\\_\oplus\mathsf{1}}$, is a distributive
restriction category (Prop 7.4), where the (co)product $\times$ (resp.
$\oplus$) of $\mathbb{D}$ becomes the restriction (co)product in
$\mathbb{D}_{\\_\oplus\mathsf{1}}$. Furthermore, it is already known that
$A\oplus B\oplus(A\times B)$ is a categorical product in
$\mathbb{D}_{\\_\oplus\mathsf{1}}$ [9, Prop. 3.4]. Thus,
$\mathbb{D}_{\\_\oplus\mathsf{1}}$ has classical products and is therefore
also classical. Less obviously, the converse is also true.

To prove this, we use the concept of classified restriction categories, which
were introduced by Cockett and Lack in [6]. Briefly, a restriction category is
classified if it has an abstract partial map classifier and every map factors
through this classifier via a unique total map (Def. 7.5). It turns out every
classified restriction category is equivalent to the Kleisli category of the
canonical monad induced on its subcategory of total maps (Prop. 7.6). From
this, we obtain that a distributive restriction category is the Kleisli
category of the exception monad of a distributive category if and only if it
is classically classified (Def. 7.7) in the sense that every map
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
factors uniquely as a total map
$\mathcal{T}(f):A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$ (Cor. 7.12). Thus a
distributive restriction category is classical if and only if it is
classically classified if and only if is equivalent to the Kleisli category of
an exception monad on an ordinary distributive category (Thm. 7.16).
Therefore, a distributive restriction category has classical products
precisely when it is the Kleisli category of the exception monad on an
ordinary distributive category.

In this manner, for a distributive restriction category to have classical
products embodies some surprisingly strong structural properties.

### Outline:

Section 2 reviews the basics of distributive restriction categories. Section 3
introduces the notion of classical products for distributive restriction
categories. Section 4 provides a review of classical restriction categories,
as well as some new observations about the complements of restriction
idempotents. In Section 5 we show how restriction (co)products and categorical
products (no matter their form) are related via splitting restriction
idempotent, and how in a classical restriction category, the categorical
product must always be of the form $A\oplus B\oplus(A\times B)$. In Section 6
we prove the main result of this paper: distributive restriction categories
are classical if and only if they have classical products. Finally, in Section
7, we extend the main result and show that a distributive restriction category
is classical if and only if it is equivalent to the Kleisli category of the
exception monad on a distributive category.

### Conventions

In an arbitrary category $\mathbb{X}$, we denote objects by capital letters
$A$, $B$, etc. and maps by lower case letters $f$, $g$, $h$, etc. Identity
maps are written as $1_{A}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, while composition is written in
diagrammatic order, that is, the composite of maps
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
and $g:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ is denoted
$fg:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$, which first does $f$ then $g$.

##  2 Distributive Restriction Categories

In this background section, we review distributive restriction categories –
mostly to introduce notation and terminology. As such, we will quickly review
restriction categories, restriction products, and restriction coproducts, as
well as some basic identities and our two main running examples. For a more
in-depth introduction to restriction categories, we invite the reader to see
[5, 6, 7, 8].

###### Definition 2.1

A restriction category [5, Sec 2.1.1] is a category $\mathbb{X}$ equipped with
a restriction operator $\overline{(\phantom{f})}$, which associates every map
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
to a map ${\overline{f}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A}$, called the restriction of $f$, and
such that the following four axioms hold:

  1. [R.1]

$\overline{f}f=f$

  2. [R.2]

$\overline{f}\overline{g}=\overline{g}\overline{f}$

  3. [R.3]

$\overline{\overline{g}f}=\overline{g}\overline{f}$

  4. [R.4]

$f\overline{g}=\overline{fg}f$

Furthermore, in a restriction category $\mathbb{X}$:

  1. (i)

A total map [5, Sec 2.1.2] is a map $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ such that $\overline{f}=1_{A}$. We
denote $\mathcal{T}\left[\mathbb{X}\right]$ to be the subcategory of total
maps of $\mathbb{X}$.

  2. (ii)

A restriction idempotent [5, Sec 2.3.3] is a map
$e:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
such that $\overline{e}=e$.

The canonical example of a restriction category is the category of sets and
partial functions, which we review in Ex 2.6 below. For a list of many other
examples of restriction categories, see [5, Sec 2.1.3]. Here are some basic
identities that will be useful for the proofs in this paper:

###### Lemma 2.2

[5, Lemma 2.1 & 2.2] In a restriction category $\mathbb{X}$:

  1. (i)

$\overline{fg}=\overline{f\overline{g}}$

  2. (ii)

If $g$ is total, then $\overline{fg}=\overline{f}$

  3. (iii)

If $f$ is monic, then $f$ is total;

  4. (iv)

If $e$ is a restriction idempotent, then it is an idempotent, that is, $ee=e$;

  5. (v)

If $e$ and $e^{\prime}$ are restriction idempotents of the same type, then
their composite is a restriction idempotent and $ee^{\prime}=e^{\prime}e$;

  6. (vi)

If $e$ is a restriction idempotent, then
$\overline{ef}=e\overline{f}=\overline{f}e$;

  7. (vii)

If $e$ is a restriction idempotent, then $fe=\overline{fe}f$;

  8. (viii)

For any map $f$, $\overline{f}$ is a restriction idempotent, so
$\overline{\overline{f}}=\overline{f}$ and
$\overline{f}~{}\overline{f}=\overline{f}$

We now turn our attention to restriction products. As mentioned in the
introduction, restriction products are not products in the usual sense, since
they satisfy a lax universal property. A 2-categorical explanation of why
restriction products are the appropriate analogue of products for restriction
categories can be found in [7, Sec 4.1] (briefly it is what arises when one
considers Cartesian objects in the appropriate 2-category of restriction
categories).

###### Definition 2.3

A Cartesian restriction category is a restriction category $\mathbb{X}$ with:

  1. (i)

A restriction terminal object [7, Sec 4.1], that is, an object $\mathsf{1}$
such that for every object $A$ there exists a unique total map
$t_{A}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}\mathsf{1}$ such that for every map
$f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, the following equality holds:

$\displaystyle ft_{B}=\overline{f}t_{A}$ (1)

  2. (ii)

Binary restriction products [7, Sec 4.1], that is, every pair of objects $A$
and $B$, there is an object $A\times B$ with total maps $\pi_{0}:A\times
B\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
and $\pi_{1}:A\times B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ such that for every pair of maps
$f:C\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
and ${g:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B}$, there exists a unique map $\langle
f,g\rangle:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times B$ such that the following
equalities hold:

$\displaystyle\langle f,g\rangle\pi_{0}=\overline{g}f$ $\displaystyle\langle
f,g\rangle\pi_{1}=\overline{f}g$ (2)

On the other hand, restriction coproducts are actual coproducts in the usual
sense. The justification for this is that actual coproducts are required if
one wishes that a restriction category admits a “calculus of matrices” [7, Sec
2.3], as well as providing the appropriate restriction analogue of an
extensive category [7, Def 3] (which we discuss in Def 6.3 below). A
2-categorical explanation for why restriction coproducts are simply coproducts
can be found in [7, Sec 2.1] (briefly it is what arises when one considers
coCartesian objects in the appropriate 2-category of restriction categories).

In this paper, while we will only need to work with binary restriction
products, for simplicity, it will be easier to work with finite (restriction)
coproducts. So for a category $\mathbb{X}$ with finite coproducts, we denote
the coproduct as $\oplus$, with injection maps
${\iota_{j}:A_{j}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A_{0}\oplus\ldots\oplus A_{n}}$, where
the copairing operation is denoted by $[-,\ldots,-]$, and we denote the
initial object as $\mathsf{0}$ with unique map
$z_{A}:\mathsf{0}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$.

###### Definition 2.4

A coCartesian restriction category is a restriction category $\mathbb{X}$ with
finite restriction coproducts [7, Sec 2.1], that is, $\mathbb{X}$ has finite
coproducts where all the injection maps
${\iota_{j}:A_{j}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A_{0}\oplus\ldots\oplus A_{n}}$ are
total.

Lastly, we may ask that restriction products distribute over restriction
coproducts:

###### Definition 2.5

A distributive restriction category [7, Sec 5.3] is a restriction category
$\mathbb{X}$ which is both a Cartesian restriction category and a coCartesian
restriction category such that the canonical maps:

$\displaystyle\left\langle
1_{A}\times\iota_{0},1_{A}\times\iota_{1}\right\rangle:(A\times
B)\oplus(A\times C)\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times(B\oplus C)$
$\displaystyle\langle
z_{A},1_{\mathsf{0}}\rangle:\mathsf{0}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times\mathsf{0}$ (3)

are isomorphisms.

Here are our main examples of distributive restriction categories, which we
will use as running examples throughout this paper:

###### Example 2.6

Let $\mathsf{PAR}$ be the category whose objects are sets and whose maps are
partial functions between sets. Then $\mathsf{PAR}$ is a distributive
restriction category where:

  1. (i)

The restriction of a partial function $f:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Y$ is the partial function
$\overline{f}:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}X$ defined as follows:

$\overline{f}(x)=\begin{cases}x&\text{if }f(x)\downarrow\\\ \uparrow&\text{if
}f(x)\uparrow\end{cases}$

where $\downarrow$ means defined and $\uparrow$ means undefined.

  2. (ii)

The restriction terminal object is a chosen singleton $\mathsf{1}=\\{\ast\\}$,
and $t_{X}:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}\\{\ast\\}$ maps everything to the
single element, $t_{X}(x)=\ast$.

  3. (iii)

The restriction product is given by the Cartesian product $A\times B$, where
the projections $\pi_{0}:X\times Y\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}X$ and $\pi_{1}:X\times
Y\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}Y$
are defined as $\pi_{0}(x,y)=x$ and $\pi_{1}(x,y)=y$, and the pairing of
partial functions is defined as:

$\langle f,g\rangle(x)=\begin{cases}(f(x),g(x))&\text{if }f(x)\downarrow\text{
and }g(x)\downarrow\\\ \uparrow&\text{otherwise}\end{cases}$

  4. (iv)

The initial object is the empty set $\mathsf{0}=\emptyset$ and the coproduct
is given by disjoint union $X\oplus Y=X\sqcup Y$.

The total maps are precisely functions that are everywhere defined, so
$\mathcal{T}\left[\mathsf{PAR}\right]=\mathsf{SET}$, the category of sets and
functions. Restriction idempotents of type $X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}X$ correspond precisely to the subsets
of $X$. Explicitly, given a subset $U\subseteq X$, its associated restriction
idempotent is the partial function $e_{U}:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}X$ defined as follows:

$e_{U}=\begin{cases}x&\text{if }x\in U\\\ \uparrow&\text{if }x\notin
U\end{cases}$

In particular, for a partial function $f:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Y$, we have that its restriction
$\overline{f}$ is the restriction idempotent associated to the domain of $f$,
$\mathsf{dom}(f)=\\{x\in X|~{}f(x)\downarrow\\}\subseteq X$, that is,
$\overline{f}=e_{\mathsf{dom}(f)}$.

###### Example 2.7

Let $k$ be a commutative ring and let $k\text{-}\mathsf{CALG}_{\bullet}$ be
the category whose objects are commutative $k$-algebras and whose maps are
_non-unital_ $k$-algebra morphisms, that is, $k$-linear morphisms
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
that preserve the multiplication, $f(ab)=f(a)f(b)$, but not necessarily the
multiplicative unit, so $f(1)$ may not equal $1$. Then
$k\text{-}\mathsf{CALG}^{op}_{\bullet}$ is a distributive restriction
category, so $k\text{-}\mathsf{CALG}_{\bullet}$ is a codistributive
corestriction category where:

  1. (i)

The corestriction of a non-unital $k$-algebra morphism
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
is the non-unital $k$-algebra morphism
${\overline{f}:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B}$ defined as:

$\overline{f}(b)=f(1)b$

  2. (ii)

The corestriction initial object is $k$, and
$t_{A}:k\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ is defined by the $k$-algebra
structure of $A$.

  3. (iii)

The corestriction coproduct is given by the tensor product $A\otimes B$, where
the injections $\iota_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\otimes B$ and
${\iota_{1}:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\otimes B}$ are defined as
$\iota_{0}(a)=a\otimes 1$ and $\iota_{1}(b)=1\otimes b$, and where the
copairing is given by:

$[f,g](a\otimes b)=f(a)g(b)$

  4. (iv)

The terminal object is the zero algebra $\mathsf{0}$ and the product is given
by the product of $k$-algebras $A\times B$.

The total maps correspond precisely to the maps that do preserve the
multiplicative unit, $f(1)=1$. In other words, the total maps are the actual
$k$-algebra morphisms. So
$\mathcal{T}[k\text{-}\mathsf{CALG}^{op}_{\bullet}]=k\text{-}\mathsf{CALG}^{op}$,
where $k\text{-}\mathsf{CALG}$ is the category of commutative $k$-algebras and
$k$-algebra morphisms. Restriction idempotents in
$k\text{-}\mathsf{CALG}^{op}$, so corestriction idempotents in
$k\text{-}\mathsf{CALG}_{\bullet}$, of type
$A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
correspond precisely to idempotent elements of $A$, that is, elements $u\in A$
such that $u^{2}=1$. Explicitly, for an idempotent element $u\in A$, its
associated corestriction idempotent is the non-unital $k$-algebra morphism
$e_{u}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ defined as:

$e_{u}(a)=ua$

So for a non-unital $k$-algebra morphism $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, the corresponding idempotent element
of its corestriction $\overline{f}$ is $f(1)\in B$, and so
$\overline{f}=e_{f(1)}$.

##  3 Classical Products

In this section, we introduce classical products for distributive restriction
categories, which is the main concept of interest in this paper. Classical
products are actual products in the usual sense. The nomenclature is justified
since in Sec 6 we will show that a distributive restriction category has
classical products if and only if it is a classical restriction category
(which we review in Sec 4).

To distinguish between products and restriction products, we will use linear
logic inspired notation for the former. So for a category $\mathbb{X}$ with
finite products, we denote the binary product by $\&$, the projection maps as
$p_{0}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ and
$p_{1}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, and the pairing operation by
$\llangle-,-\rrangle$. Concretely, if only to avoid confusion with the
restriction product, for every pair of maps
$f:C\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
and $g:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, $\llangle
f,g\rrangle:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$ is the unique map such that the
following equalities hold:

$\displaystyle\llangle f,g\rrangle p_{0}=f$ $\displaystyle\llangle f,g\rrangle
p_{1}=g$ (4)

We stress that, unlike the projections of restriction products, the
projections $p_{i}$ are not assumed to be total. We denote the terminal object
by $\mathsf{0}$ and unique maps to it by
$!_{A}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}\mathsf{0}$. Keen-eyed readers will note
that we are using the same notation for both the terminal object and the
restriction initial object. This is justified in Lemma 3.6.(i) below.

Here are some basic identities regarding compatibility between the restriction
and the product structure:

###### Lemma 3.1

In a restriction category $\mathbb{X}$ with finite products:

  1. (i)

$f\overline{!_{B}}=\overline{!_{A}}f$;

  2. (ii)

$\left\llangle f,g\right\rrangle\overline{p_{0}}=\left\llangle
f,\overline{f}g\right\rrangle$ and $\left\llangle
f,g\right\rrangle\overline{p_{1}}=\left\llangle\overline{g}f,g\right\rrangle$;

  3. (iii)

$\left\llangle
f,g\right\rrangle\overline{p_{0}}~{}\overline{p_{1}}=\left\llangle\overline{g}f,\overline{f}g\right\rrangle$

Proof: Recall that the pairing $\llangle-,-\rrangle$ is compatible with
composition in the following sense:

$\displaystyle h\llangle f,g\rrangle(p\&q)=\left\llangle
hfk,hgk\right\rrangle$ (5)

  1. (i)

Here we use [R.4]:

$\displaystyle f\overline{!_{B}}$ $\displaystyle=~{}\overline{f!_{B}}f$ [R.4]
$\displaystyle=~{}\overline{!_{A}}f$ Uniqueness of $!$

  2. (ii)

Here we use [R.4] and [R.1]:

$\displaystyle\left\llangle f,g\right\rrangle\overline{p_{0}}$
$\displaystyle=~{}\overline{\left\llangle f,g\right\rrangle
p_{0}}\left\llangle f,g\right\rrangle$ [R.4]
$\displaystyle=~{}\overline{f}\left\llangle f,g\right\rrangle$ (4)
$\displaystyle=~{}\left\llangle\overline{f}f,\overline{f}g\right\rrangle$ (5)
$\displaystyle=~{}\left\llangle f,\overline{f}g\right\rrangle$ [R.4]

So $\left\llangle f,g\right\rrangle\overline{p_{0}}=\left\llangle
f,\overline{f}g\right\rrangle$, and similarly we can compute that
$\left\llangle
f,g\right\rrangle\overline{p_{1}}=\left\llangle\overline{g}f,g\right\rrangle$.

  3. (iii)

Here we apply the above two identities, and also [R.2] and [R.3]:

$\displaystyle\left\llangle
f,g\right\rrangle\overline{p_{0}}~{}\overline{p_{1}}$
$\displaystyle=~{}\left\llangle f,\overline{f}g\right\rrangle\overline{p_{1}}$
Lemma 3.1.(ii)
$\displaystyle=~{}\left\llangle\overline{\overline{f}g}f,\overline{f}g\right\rrangle$
Lemma 3.1.(ii)
$\displaystyle=~{}\left\llangle\overline{f}\overline{g}f,\overline{f}g\right\rrangle$
[R.3]
$\displaystyle=~{}\left\llangle\overline{g}\overline{f}f,\overline{f}g\right\rrangle$
[R.2]
$\displaystyle=~{}\left\llangle\overline{g}f,\overline{f}g\right\rrangle$
[R.1]

So the desired identities hold. $\Box$

We now turn our attention to properly defining classical products. So in a
distributive restriction category, we wish to know when $A\oplus
B\oplus(A\times B)$ is a product of $A$ and $B$. In order to define the
projections, we will need restriction zero maps. Intuitively, a restriction
zero map is a map which is nowhere defined. For a category $\mathbb{X}$ with
zero maps, we denote the zero maps by $0:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, and recall that zero maps satisfy
the annihilation property that $f0=0=0f$ for all maps $f$.

###### Definition 3.2

A restriction category $\mathbb{X}$ is said to have restriction zeroes [7, Sec
2.2] if $\mathbb{X}$ has zero maps such that $\overline{0}=0$.

###### Example 3.3

$\mathsf{PAR}$ has restriction zeroes, where the restriction zero maps are the
partial functions $0:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Y$ which is nowhere defined,
$0(x)\uparrow$ for all $x\in X$.

###### Example 3.4

$k\text{-}\mathsf{CALG}^{op}_{\bullet}$ has restriction zeroes, so
$k\text{-}\mathsf{CALG}_{\bullet}$ has corestriction zeroes, where
$0:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
is the zero morphism, $0(a)=0$.

In a coCartesian restriction category with restriction zeroes, the restriction
terminal object becomes a zero object and we can define “quasi-projections”
for the restriction coproduct (which make the injections into
restriction/partial isomorphisms [5, Sec 2.3.1]).

###### Definition 3.5

In a coCartesian restriction $\mathbb{X}$ with restriction zeroes, define the
maps $\iota^{\circ}_{j}:A_{0}\oplus\ldots\oplus
A_{n}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A_{j}$ as the copairing
$\iota^{\circ}_{j}:=[0,\ldots,0,1_{A_{j}},0,\ldots,0]$.

###### Lemma 3.6

[7, Lemma 2.10] In a coCartesian restriction $\mathbb{X}$ with restriction
zeroes,

  1. (i)

The restriction initial object $\mathsf{0}$ is a zero object, so in particular
a terminal object;

  2. (ii)

$\overline{\iota^{\circ}_{j}}=0\oplus\ldots\oplus 0\oplus 1_{A_{j}}\oplus
0\oplus\ldots\oplus 0$;

  3. (iii)

$\iota_{j}\iota^{\circ}_{j}=1_{A_{j}}$ and $\iota_{i}\iota^{\circ}_{j}=0$ for
$i\neq j$;

  4. (iv)

$\iota^{\circ}_{j}\iota_{j}=\overline{\iota^{\circ}_{j}}$;

  5. (v)

$\overline{\iota^{\circ}_{j}}\overline{\iota^{\circ}_{j}}=\overline{\iota^{\circ}_{j}}$
and $\overline{\iota^{\circ}_{i}}\overline{\iota^{\circ}_{j}}=0$ for $i\neq
j$;

  6. (vi)

$\iota^{\circ}\iota_{0}\oplus\ldots\oplus\iota^{\circ}_{n}\iota_{n}=1_{A_{0}\oplus\ldots\oplus
A_{n}}$.

We now use restriction zero maps to define the projections for our desired
classical product.

###### Definition 3.7

In a distributive restriction category $\mathbb{X}$,

  1. (i)

For every pair of objects $A$ and $B$, define the object $A\&B$ as
$A\&B:=A\oplus B\oplus(A\times B)$;

  2. (ii)

If $\mathbb{X}$ has restriction zeroes, then for every pair of objects $A$ and
$B$, define the maps ${p_{0}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A}$ and
${p_{1}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B}$ respectively as follows:

$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.375pt\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{A}$}}}}}}}{\hbox{\kern 90.375pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
A\oplus B\oplus(A\times
B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
28.86957pt\raise 6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.575pt\hbox{$\scriptstyle{p_{0}:=[1_{A},0,\pi_{0}]}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.37502pt\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
186.82027pt\raise 6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.575pt\hbox{$\scriptstyle{p_{1}:=[0,1_{B},\pi_{1}]}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 248.43134pt\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}}{\hbox{\kern
248.43134pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{B}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$
(6)

A distributive restriction category $\mathbb{X}$ is said to have classical
products if $\mathbb{X}$ has restriction zeroes and for every pair of objects
$A$ and $B$, (6) is a product diagram, that is, $A\&B$ is the product of $A$
and $B$ with projections $p_{0}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ and
$p_{1}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$.

To distinguish between classical products and restriction products, the maps
$p_{i}$ will now be referred to as the classical projections, and
$\llangle-,-\rrangle$ as the classical pairing. It follows from Lemma 3.6.(i)
that having classical products implies having finite products:

###### Corollary 3.8

A distributive restriction category with classical products has finite
products.

Here are our main examples of classical products:

###### Example 3.9

$\mathsf{PAR}$ has classical products where $X\&Y=X\sqcup Y\sqcup(X\times Y)$
and the classical projections are defined as:

$\displaystyle p_{0}(x)=x\qquad p_{1}(x)\uparrow\qquad\forall x\in X$
$\displaystyle p_{0}(y)\uparrow\qquad p_{1}(y)=y\qquad\forall y\in Y$
$\displaystyle p_{0}(x,y)=x\qquad p_{1}(x,y)=y\qquad\forall(x,y)\in X\times Y$

The classical pairing $\llangle-,-\rrangle$ of partial functions is defined as
follows

$\llangle f,g\rrangle(x)=\begin{cases}f(x)&\text{if }f(x)\downarrow\text{ and
}g(x)\uparrow\\\ g(x)&\text{if }f(x)\uparrow\text{ and }g(x)\downarrow\\\
(f(x),g(x))&\text{if }f(x)\downarrow\text{ and }g(x)\downarrow\\\
\uparrow&\text{if }f(x)\uparrow\text{ and }g(x)\uparrow\end{cases}$

###### Example 3.10

$k\text{-}\mathsf{CALG}^{op}_{\bullet}$ has classical products, so
$k\text{-}\mathsf{CALG}_{\bullet}$ has coclassical coproducts where
$A\&B=A\times B\times(A\otimes B)$, and the coclassical injections
$p_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$ and
${p_{1}:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B}$ are defined as:

$\displaystyle p_{0}(a)=(a,0,a\otimes 1)$ $\displaystyle
p_{1}(b)=(0,b,1\otimes b)$

The coclassical copairing $\llangle
f,g\rrangle:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ is defined as follows:

$\displaystyle\llangle f,g\rrangle(a,b,x\otimes
y)=f(a)-f(a)g(1)+g(b)-f(1)g(b)+f(x)g(y)$

It is important to note that for classical products, while on objects we have
that ${A\&B=A\oplus B\oplus(A\times B)}$, on maps
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
and $g:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}D$, the map $f\&g=\llangle
p_{0}f,p_{1}g\rrangle$ may not be equal to $f\oplus g\oplus(f\times
g)=\left[\iota_{0}f,\iota_{1}g,\iota_{2}\langle\pi_{0}f,\pi_{1}g\rangle\right]$,
even though they are of the same type $A\oplus B\oplus(A\times
B)\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C\oplus D\oplus(C\times D)$.
Intuitively, the main difference between the two is that for $f\oplus
g\oplus(f\times g)$, the third component $C\times D$ of its output in only
depends on the third component $A\times B$ of the input, while for $f\&g$, the
third component $C\times D$ of its output can depend on all three components
$A$, $B$, and $A\times B$ of the input. To help better understand this
difference, let us compare them explicitly in our main examples.

###### Example 3.11

In $\mathsf{PAR}$, for partial functions $f:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Z$ and
$g:Y\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}W$, let us compare $f\&g$ and $f\sqcup
g\sqcup(f\times g)$, both of which are of type $X\sqcup Y\sqcup(X\times
Y)\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Z\sqcup W\sqcup(Z\times W)$. On the one
hand, for $u\in X\sqcup Y\sqcup(X\times Y)$, we have that:

$\left(f\sqcup g\sqcup(f\times g)\right)(u)=\begin{cases}f(u)&\text{if }u\in
X\text{ and }f(u)\downarrow\\\ g(u)&\text{if }u\in Y\text{ and
}g(u)\downarrow\\\ (f(u_{0}),g(u_{1}))&\text{if }u=(u_{0},u_{1})\in X\times
Y\text{ and }f(u_{0})\downarrow\text{ and }g(u_{1})\downarrow\\\
\uparrow&\text{o.w.}\end{cases}$

while on the other hand, we have that:

$\left(f\&g\right)(u)=\begin{cases}f(u)&\text{if }u\in X\text{ and
}f(u)\downarrow\\\ g(u)&\text{if }u\in Y\text{ and }g(u)\downarrow\\\
(f(u_{0}),g(u_{1}))&\text{if }u=(u_{0},u_{1})\in X\times Y\text{ and
}f(x)\downarrow\text{ and }g(x)\downarrow\\\ f(u_{0})&\text{if
}u=(u_{0},u_{1})\in X\times Y\text{ and }f(u_{0})\downarrow\text{ and
}g(u_{1})\uparrow\\\ g(u_{1})&\text{if }u=(u_{0},u_{1})\in X\times Y\text{ and
}f(u_{0})\uparrow\text{ and }g(u_{1})\downarrow\\\ \uparrow&\text{o.w.
}\end{cases}$

As such, we clearly see that $f\&g$ and $f\sqcup g\sqcup(f\times g)$ are
indeed different. The main difference between the two is that for $(x,y)\in
X\times Y$, we have that $\left(f\sqcup g\sqcup(f\times
g)\right)(x,y)=(f(x),g(y))\in Z\times W$ always (when defined), while
$(f\&g)(x,y)$ can equal $f(x)\in Z$, or $g(y)\in W$, or even $(f(x),g(y))\in
Z\times W$. As a particular case, consider when $g=0$. Then $(f\sqcup 0\sqcup
f\times 0)(x)=f(x)$ for all $x\in X$ when $f(x)\downarrow$ but is undefined
for all $y\in Y$ and $(x,y)\in X\times Y$, while $(f\&0)(x)=f(x)$ and
$(f\&0)(x,y)=f(x)$ for all $x\in X$ and $(x,y)\in X\times Y$ when
$f(x)\downarrow$ and is undefined for all $y\in Y$.

###### Example 3.12

In $k\text{-}\mathsf{CALG}_{\bullet}$, for a pair of non-unital $k$-algebra
morphism $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ and
$g:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}D$, let us compare $f\&g$ and $f\times
g\times(f\otimes g)$, which recall both are of type $A\times B\times(A\otimes
B)\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C\times D\times(C\times D)$. On the one
hand, we have that:

$\displaystyle\left(f\times g\times(f\otimes g)\right)(a,b,x\otimes
y)=(f(a),g(b),f(x)\otimes g(y))$

while on the other hand we have that:

$\displaystyle(f\&g)(a,b,x\otimes y)$
$\displaystyle=\left(f(a),g(b),f(a)\otimes 1-f(a)\otimes g(1)+1\otimes
g(b)-f(1)\otimes g(b)+f(x)\otimes g(y)\right)$

Thus, we clearly see that the main difference between the two is that the
resulting third component of $f\times g\times(f\otimes g)$ only depends on the
third input, while the third component of $f\&g$ depends on all three inputs.
In particular, taking $g=0$, we see that $\left(f\times 0\times(f\otimes
0)\right)(a,b,x\otimes y)=(f(a),0,0)$ while $(f\&g)(a,b,x\otimes
y)=(f(a),0,f(a)\otimes 1)$.

We conclude this section with some useful identities regarding classical
products, which we will need for the main results of this paper in Sec 6.

###### Lemma 3.13

In a distributive restriction category $\mathbb{X}$ with classical products,

  1. (i)

$\overline{p_{0}}=1_{A}\oplus 0\oplus 1_{A\times B}$ and
$\overline{p_{1}}=0\oplus 1_{B}\oplus 1_{A\times B}$;

  2. (ii)

$\overline{p_{1}}p_{0}=\iota^{\circ}_{2}\pi_{0}$ and
$\overline{p_{0}}p_{1}=\iota^{\circ}_{2}\pi_{1}$;

  3. (iii)

$\llangle f,g\rrangle\iota_{2}^{\circ}=\langle f,g\rangle$;

  4. (iv)

$\llangle f,0\rrangle=f\iota_{0}$ and $\llangle 0,f\rrangle=f\iota_{1}$;

  5. (v)

$\llangle f,f\rrangle=\langle f,f\rangle\iota_{2}$;

  6. (vi)

$\llangle 0,0\rrangle=0$

Proof: First recall that the copairing is compatible with composition in the
following sense:

$\displaystyle(g_{0}\oplus\ldots\oplus
g_{n})[f_{0},\ldots,f_{n}]h=[g_{0}f_{0}h,\ldots,g_{n}f_{n}h]$ (7)

Also recall that the restriction of a copairing is the coproduct of the
restrictions [7, Lemma 2.1]:

$\displaystyle\overline{[f_{0},\ldots,f_{n}]}=\overline{f_{0}}\oplus\ldots\oplus\overline{f_{n}}$
(8)

  1. (i)

Taking the restriction of the copairing, we compute that:

$\displaystyle\overline{p_{0}}$
$\displaystyle=~{}\overline{\left[1_{A},0,\pi_{0}\right]}$ Def. of $p_{0}$
$\displaystyle=~{}\overline{1_{A}}\oplus\overline{0}\oplus\overline{\pi_{0}}$
(8) $\displaystyle=~{}1_{A}\oplus 0\oplus 1_{A\times B}$ $1_{A}$ and $\pi_{0}$
are total, and rest. zero

So $\overline{p_{0}}=1_{A}\oplus 0\oplus 1_{A\times B}$, and similarly we can
show that $\overline{p_{1}}=0\oplus 1_{B}\oplus 1_{A\times B}$.

  2. (ii)

This follows from (i) above:

$\displaystyle\overline{p_{1}}p_{0}$ $\displaystyle=~{}(0\oplus 1_{B}\oplus
1_{A\times B})\left[1_{A},0,\pi_{0}\right]$ Lemma 3.13.(i) and Def. of $p_{0}$
$\displaystyle=~{}\left[0,0,1_{A\times B}\right]\pi_{0}$ (7)
$\displaystyle=~{}\iota^{\circ}_{2}\pi_{0}$ Def. of $\iota^{\circ}_{2}$

So $\overline{p_{1}}p_{0}=\iota^{\circ}_{2}\pi_{0}$, and similarly we can show
that $\overline{p_{0}}p_{1}=\iota^{\circ}_{2}\pi_{1}$.

  3. (iii)

We use (ii) above to show that $\llangle f,g\rrangle\iota_{2}^{\circ}$
satisfies (2). So we compute:

$\displaystyle\llangle f,g\rrangle\iota_{2}^{\circ}\pi_{0}$
$\displaystyle=~{}\llangle f,g\rrangle\overline{p_{1}}p_{0}$ Lemma 3.13.(ii)
$\displaystyle=~{}\left\llangle\overline{g}f,\overline{f}g\right\rrangle
p_{0}$ Lemma 3.1.(ii) $\displaystyle=~{}\overline{g}f$ (4)

So $\llangle f,g\rrangle\iota_{2}^{\circ}\pi_{0}=\overline{g}f$, and similarly
we can show that $\llangle f,g\rrangle\iota_{2}^{\circ}\pi_{1}=\overline{f}g$.
So by the universal property of the restriction product, it follows that
$\llangle f,g\rrangle\iota_{2}^{\circ}=\langle f,g\rangle$.

  4. (iv)

By definition of the classical projections, we have that $f\iota_{0}p_{0}=f$
and $f\iota_{0}p_{1}=0$. Then by the universal property of the classical
product, it follows that $\llangle f,0\rrangle=f\iota_{0}$. Similarly, we also
have that $\llangle 0,f\rrangle=f\iota_{1}$.

  5. (v)

By definition of the classical projections, the pairing $\langle-,-\rangle$,
and [R.1], we have that $\langle f,f\rangle\iota_{2}p_{0}=f$ and $\langle
f,f\rangle\iota_{2}p_{1}=f$. Then by the universal property of the classical
product, it follows that $\llangle f,f\rrangle=\langle f,f\rangle\iota_{2}$.

  6. (vi)

This follows from (iv), so $\llangle 0,0\rrangle=0$.

$\Box$

##  4 Classical Restriction Categories

The main objective of this paper is to prove that a distributive restriction
category with classical products is classical. In this section, we review the
basics of classical restriction categories, as well as provide some new
results regarding complements of restriction idempotents. For a more in-depth
introduction to classical restriction categories, we refer the reader to [8,
3].

A restriction category is classical if we can take the joins of maps and
relative complements of maps. In order to properly define joins, we first need
to discuss certain relations between maps in a restriction category.

###### Definition 4.1

In a restriction category $\mathbb{X}$, for parallel maps
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
and $g:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ we say that:

  1. (i)

$f$ is less than or equal to $g$ [5, Sec 2.1.4], written $f\leq g$, if
$\overline{f}g=f$;

  2. (ii)

$f$ and $g$ are compatible [8, Prop 6.3], written $f\smile g$, if
$\overline{f}g=\overline{g}f$;

If $\mathbb{X}$ has restriction zeroes, then we say that:

  1. (iii)

$f$ and $g$ are disjoint [8, Prop 6.2], written $f\perp g$, if
$\overline{f}g=0$ (or equivalently $\overline{g}f=0)$.

Intuitively, $f\leq g$ means that whenever $f$ is defined, $g$ is equal to
$f$; $f\smile g$ means that whenever they are both defined, they are equal;
and $f\perp g$, means that whenever one is defined, the other is not. Note
that disjoint maps are compatible, so if $f\perp g$ then $f\smile g$ as well.
We can also consider the join of compatible maps with respect to the partial
order.

###### Definition 4.2

In a restriction category $\mathbb{X}$, the join [8, Def 6.7] (if it exists)
of a finite family of parallel maps $f_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, …,
$f_{n}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ that is pairwise compatible, so
$f_{i}\smile f_{j}$ for all $0\leq i,j,\leq n$, is a (necessarily unique) map
$f_{0}\vee\ldots\vee f_{n}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ such that:

  1. [J.1]

$f_{i}\leq f_{0}\vee\ldots\vee f_{n}$ for all $0\leq i\leq n$;

  2. [J.2]

If $g:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ is a map such that $f_{i}\leq g$ for
all $0\leq i\leq n$ then $f_{0}\vee\ldots\vee f_{n}\leq g$;

A join restriction category [8, Def 10.1] is a restriction category
$\mathbb{X}$ such that the join of any finite family of pairwise compatible
maps exists and is preserved by pre-composition, that is:

  1. [J.3]

For any map $h:A^{\prime}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, $h\left(f_{0}\vee\ldots\vee
f_{n}\right)=hf_{0}\vee\ldots\vee hf_{n}$.

Here are now some useful identities regarding joins. In particular, join
restriction categories have restriction zeroes, given by the join of the empty
family, and joins are also preserved by post-composition.

###### Lemma 4.3

[3, Prop 2.14] In a join restriction category $\mathbb{X}$,

  1. (i)

$\mathbb{X}$ has restriction zeroes;

  2. (ii)

$f\vee 0=f$;

  3. (iii)

$\left(f_{0}\vee\ldots\vee f_{n}\right)k=f_{0}k\vee\ldots\vee f_{n}k$

  4. (iv)

$\overline{f_{0}\vee\ldots\vee
f_{n}}=\overline{f_{0}}\vee\ldots\vee\overline{f_{n}}$

  5. (v)

$\overline{f_{j}}\left(f_{0}\vee\ldots\vee f_{n}\right)=f_{j}$

  6. (vi)

Restriction idempotents $e_{i}$ are always pairwise compatible and
$e_{0}\vee\ldots\vee e_{n}$ is a restriction idempotent;

  7. (vii)

If $e_{1}$ and $e_{2}$ are restriction idempotents, then $e_{1}\perp e_{2}$ if
and only if $e_{1}e_{2}=0$.

Here are also some compatibility identities between joins and restriction
coproducts which will be useful for proofs in later sections.

###### Lemma 4.4

In a coCartesian restriction category $\mathbb{X}$ which is also a join
restriction category,

  1. (i)

For any family of maps $f_{0}$, …, and $f_{n}$, the maps
$\iota^{\circ}_{0}f_{0}\iota_{0}$, …, and $\iota^{\circ}_{n}f_{n}\iota_{n}$
are pairwise disjoint, and
$\iota^{\circ}_{0}f_{0}\iota_{0}\vee\ldots\vee\iota^{\circ}_{n}f_{n}\iota_{n}=f_{0}\oplus\ldots\oplus
f_{n}$;

  2. (ii)

$\iota^{\circ}_{0}\iota_{0}$, …, and $\iota^{\circ}_{n}\iota_{n}$ are pairwise
disjoint, and
$\iota^{\circ}_{0}\iota_{0}\vee\ldots\vee\iota^{\circ}_{n}\iota_{n}=1_{A_{0}\oplus\ldots\oplus
A_{n}}$.

Proof:

  1. (i)

For $i\neq j$, we compute:

$\displaystyle\overline{\iota^{\circ}_{i}f_{i}\iota_{i}}\iota^{\circ}_{j}f_{j}\iota_{j}$
$\displaystyle=~{}\overline{\iota^{\circ}_{i}f_{i}\iota_{i}}\overline{\iota^{\circ}_{j}}\iota^{\circ}_{j}f_{j}\iota_{j}$
[R.1]
$\displaystyle=~{}\overline{\iota^{\circ}_{j}}\overline{\iota^{\circ}_{i}f_{i}\iota_{i}}\iota^{\circ}_{j}f_{j}\iota_{j}$
[R.2]
$\displaystyle=~{}\overline{\overline{\iota^{\circ}_{j}}\iota^{\circ}_{i}f_{i}\iota_{i}}\iota^{\circ}_{j}f_{j}\iota_{j}$
[R.3] $\displaystyle=~{}\overline{0}\iota^{\circ}_{j}f_{j}\iota_{j}$ Lemma
3.6.(v) $\displaystyle=~{}0$ Rest. zero

So we have that
$\iota^{\circ}_{i}f_{i}\iota_{i}\perp\iota^{\circ}_{j}f_{j}\iota_{j}$ for
$i\neq j$. Thus we can take their join
$\iota^{\circ}_{0}f_{0}\iota_{0}\vee\ldots\vee\iota^{\circ}_{n}f_{n}\iota_{n}$.
Precomposing with the injection maps, we compute:

$\displaystyle\iota_{j}\left(\iota^{\circ}_{0}f_{0}\iota_{0}\vee\ldots\vee\iota^{\circ}_{n}f_{n}\iota_{n}\right)$
$\displaystyle=~{}\iota_{j}\iota^{\circ}_{0}f_{0}\iota_{0}\vee\ldots\vee\iota_{j}\iota^{\circ}_{n}f_{n}\iota_{n}$
[J.3] $\displaystyle=~{}0\vee\ldots\vee 0\vee f_{j}\iota_{j}\vee
0\vee\ldots\vee 0$ Lemma 3.6.(iii) $\displaystyle=~{}f_{j}\iota_{j}$ Lemma
4.3.(ii)

So by the couniversal property of the coproduct,
$\iota^{\circ}_{0}f_{0}\iota_{0}\vee\ldots\vee\iota^{\circ}_{n}f_{n}\iota_{n}=[f_{0}\iota_{0},\ldots,f_{n}\iota_{n}]$,
which we can alternatively write as
$\iota^{\circ}_{0}f_{0}\iota_{0}\vee\ldots\vee\iota^{\circ}_{n}f_{n}\iota_{n}=f_{0}\oplus\ldots\oplus
f_{n}$.

  2. (ii)

This is a special case of (i) by setting $f_{j}=1_{A_{j}}$.

$\Box$

We now turn our attention to classical restriction categories, which are join
restriction categories that also have relative complements of maps.

###### Definition 4.5

In a join restriction category $\mathbb{X}$, for parallel maps
$f:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
and $g:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ such that $f\leq g$, the relative
complement [8, Sec 13] of $f$ in $g$ (if it exists) is a (necessarily unique)
map $g\backslash f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ such that222We note that in [8], the
axioms were written as (1) $g\backslash f\leq g$, (2) $g\backslash f\perp f$,
and (3) $g\leq g\backslash f\vee f$. However, it is straightforward to check
that [RC.2] is an equivalent way of expressing (1) and (3).:

  1. [RC.1]

$g\backslash f\perp f$

  2. [RC.2]

$g\backslash f\vee f=g$

A classical restriction category [8, Prop 13.1] is a join restriction category
$\mathbb{X}$ such that all relative complements exists

Intuitively, $g\backslash f$ is undefined when $f$ is defined and is equal to
$g$ whenever $f$ is undefined. Here are our main examples of classical
restriction categories.

###### Example 4.6

$\mathsf{PAR}$ is a classical restriction category where:

  1. (i)

$f\leq g$ if $g(x)=f(x)$ whenever $f(x)\downarrow$.

  2. (ii)

$f\smile g$ if $f(x)=g(x)$ whenever both $f(x)\downarrow$ and
$g(x)\downarrow$.

  3. (iii)

$f\perp g$ if $f(x)\uparrow$ whenever $g(x)\downarrow$, and $g(x)\uparrow$
whenever $f(x)\downarrow$.

  4. (iv)

If $f\smile g$, then their join $f\vee g$ is defined as follows:

$(f\vee g)(x)=\begin{cases}f(x)&\text{if }f(x)\downarrow\text{ and
}g(x)\uparrow\\\ g(x)&\text{if }f(x)\uparrow\text{ and }g(x)\downarrow\\\
f(x)=g(x)&\text{if }f(x)\downarrow\text{ and }g(x)\downarrow\\\
\uparrow&\text{if }f(x)\uparrow\text{ and }g(x)\uparrow\end{cases}$

  5. (v)

If $f\leq g$, then the relative complement $g\backslash f$ is defined as
follows:

$(g\backslash f)(x)=\begin{cases}g(x)&\text{if }f(x)\uparrow\text{ and
}g(x)\downarrow\\\ \uparrow&\text{if }f(x)\downarrow\text{ or
}g(x)\uparrow\end{cases}$

###### Example 4.7

$k\text{-}\mathsf{CALG}^{op}_{\bullet}$ is a classical restriction category,
so $k\text{-}\mathsf{CALG}_{\bullet}$ is a coclassical corestriction category
where:

  1. (i)

$f\leq g$ if $f(1)g(a)=f(a)$.

  2. (ii)

$f\smile g$ if $g(1)f(a)=f(1)g(a)$.

  3. (iii)

$f\perp g$ if $g(1)f(a)=0=f(1)g(a)$.

  4. (iv)

If $f\smile g$, then their join $f\vee g$ is defined as follows:

$(f\vee g)(a)=f(a)+g(a)-g(1)f(a)=f(a)+g(a)-f(1)g(a)$

  5. (v)

If $f\leq g$, then the relative complement $g\backslash f$ is defined as
follows:

$(g\backslash f)(a)=g(a)-f(1)g(a)$

That $k\text{-}\mathsf{CALG}^{op}_{\bullet}$ is a classical restriction
category is a new observation that follows from the main results of this
paper.

We conclude this section by discussing complements of restriction idempotents.
Indeed, note that a restriction idempotent
$e:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
is always less than or equal to the identity
$1_{A}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, so $e\leq 1_{A}$. As such, we can
consider the relative complement of a restriction idempotent in the identity.

###### Definition 4.8

In a classical restriction category $\mathbb{X}$, if
${e:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A}$ is a restriction idempotent, we
denote the relative complement of $e$ in $1_{A}$ by $e^{c}=1_{A}\backslash e$.
We call $e^{c}$ the complement of $e$.

Complements of restriction idempotents will play a crucial role in proving
that a classical distributive restriction category has classical products.
Indeed, we will be able to define the classical pairing $\llangle-,-\rrangle$
using joins and complements of restrictions. Here are now some useful
identities regarding complements of restriction idempotents.

###### Lemma 4.9

In a classical restriction category $\mathbb{X}$,

  1. (i)

If $e$ is a restriction idempotent, then $e^{c}$ is a restriction idempotent
and ${e^{c}}^{c}=e$;

  2. (ii)

If $e$ is a restriction idempotent, then $ee^{c}=0$ and $e\vee e^{c}=1$;

  3. (iii)

If $e^{\prime}$ is a restriction idempotent such that $ee^{\prime}=0$ and
$e\vee e^{\prime}=1$, then $e^{c}=e^{\prime}$;

  4. (iv)

If $e_{1}$ and $e_{2}$ are restriction idempotents, then $e^{c}_{1}\vee
e^{c}_{2}=(e_{1}e_{2})^{c}$ and $e^{c}_{1}e_{2}^{c}=(e_{1}\vee e_{2})^{c}$;

  5. (v)

$1^{c}=0$ and $0^{c}=1$;

  6. (vi)

$\overline{f}^{c}f=0$;

  7. (vii)

$\overline{f}^{c}\overline{g}^{c}=\overline{g}^{c}\overline{f}^{c}$;

  8. (viii)

$\overline{\overline{g}^{c}f}^{c}=\overline{g}\vee\overline{f}^{c}$;

  9. (ix)

$f\overline{g}^{c}=\overline{fg}^{c}f$.

Proof: First recall some useful identities about the relative complement [8,
Lemma 13.14]:

$\displaystyle\overline{g\backslash f}=\overline{g}\backslash\overline{f}$ (9)
$\displaystyle g\backslash\left(g\backslash f\right)=f$ (10)
$\displaystyle(g_{1}\backslash f_{1})(g_{2}\backslash
f_{2})=g_{1}g_{2}\backslash\left(g_{1}f_{2}\vee f_{1}g_{2}\right)$ (11)
$\displaystyle h\left(g\backslash f\right)k=hgk\backslash hfk$ (12)
$\displaystyle f\backslash f=0$ (13) $\displaystyle g\backslash 0=g$ (14)

  1. (i)

We compute that:

$\displaystyle\overline{e^{c}}$ $\displaystyle=~{}\overline{1_{A}\backslash
e}$ Def. of $e^{c}$ $\displaystyle=~{}\overline{1_{A}}\backslash\overline{e}$
(9) $\displaystyle=~{}1_{A}\backslash e$ $1_{A}$ and $e$ rest. idemp.
$\displaystyle=~{}e^{c}$ Def. of $e^{c}$

So $\overline{e^{c}}=e^{c}$, and thus $e^{c}$ is a restriction idempotent.
Taking its complement we get:

$\displaystyle{e^{c}}^{c}$
$\displaystyle=~{}1_{A}\backslash\left(1_{A}\backslash e\right)$ Def. of
$e^{c}$ $\displaystyle=~{}e$ (9)

So ${e^{c}}^{c}=e$, as desired.

  2. (ii)

We first compute that:

$\displaystyle e\overline{e^{c}}$ $\displaystyle=~{}e\overline{1_{A}\backslash
e}$ Def. of $e^{c}$ $\displaystyle=~{}e\backslash(ee)$ (12)
$\displaystyle=~{}e\backslash e$ Lemma 2.2.(iv) $\displaystyle=~{}0$ (13)

So $e\overline{e^{c}}=0$. On the other hand, $e\vee e^{c}=1$ is simply [RC.2].

  3. (iii)

Since $e$ and $e^{\prime}$ are both restriction idempotents, we have that
$e,e^{\prime}\leq 1$. Now $ee^{\prime}=0$ implies that $e\perp e^{\prime}$,
which is [RC.1], while $e\vee e^{\prime}=1$ is [RC.2]. Therefore by the
uniqueness of relative complements, we have that $e^{\prime}=1\backslash e$.
So $e^{\prime}=e^{c}$.

  4. (iv)

These are the de Morgan laws. We first compute that:

$\displaystyle e^{c}_{1}e^{c}_{2}$ $\displaystyle=~{}(1\backslash
e_{1})(1\backslash e_{2})$ Def. of $e^{c}_{i}$
$\displaystyle=~{}1\backslash(e_{1}\vee e_{2})$ (11)
$\displaystyle=~{}(e_{1}\vee e_{2})^{c}$ Def. of $(e_{1}\vee e_{2})^{c}$

So $e^{c}_{1}e^{c}_{2}=(e_{1}\vee e_{2})^{c}$. Then applying (i), we also get
$e^{c}_{1}\vee e^{c}_{2}=(e_{1}e_{2})^{c}$.

  5. (v)

By (13), $1^{c}=0$, and by (14), $0^{c}=1$.

  6. (vi)

This is the analogue of [R.1] for the complement of the restriction. So we
compute:

$\displaystyle\overline{f}^{c}f$
$\displaystyle=~{}(1_{A}\backslash\overline{f})f$ Def. of $\overline{f}^{c}$
$\displaystyle=~{}f\backslash(\overline{f}f)$ (12)
$\displaystyle=~{}f\backslash f$ [R.1] $\displaystyle=~{}0$ (13)

So $\overline{f}^{c}f=0$.

  7. (vii)

This is the analogue of [R.2] for the complement of the restriction. Since by
(i), $\overline{f}^{c}$ and $\overline{g}^{c}$ are restriction idempotents,
and restriction idempotents commute (Lemma 2.2.(v)), we have that
$\overline{f}^{c}\overline{g}^{c}=\overline{g}^{c}\overline{f}^{c}$.

  8. (viii)

This is the analogue of [R.3] for the complement of the restriction. So we
compute:

$\displaystyle\overline{\overline{g}^{c}f}^{c}$
$\displaystyle=~{}(\overline{g}^{c}\overline{f})^{c}$ Lemma 2.2.(vi)
$\displaystyle=~{}{\overline{g}^{c}}^{c}\vee\overline{f}^{c}$ Lemma 4.9.(iv)
$\displaystyle=~{}\overline{g}\vee\overline{f}^{c}$ Lemma 4.9.(i)

So $\overline{\overline{g}^{c}f}^{c}=\overline{g}\vee\overline{f}^{c}$.

  9. (ix)

This is the analogue of [R.4] for the complement of the restriction. So we
compute:

$\displaystyle f\overline{g}^{c}$
$\displaystyle=~{}\overline{f\overline{g}^{c}}f$ Lemma 2.2.(vii)
$\displaystyle=~{}\overline{f(1_{B}\backslash\overline{g})}f$ Def. of
$\overline{g}^{c}$ $\displaystyle=~{}\overline{f\backslash f\overline{g}}f$
(12) $\displaystyle=~{}\overline{f\backslash\overline{fg}f}f$ [R.4]
$\displaystyle=~{}\left(\overline{f}\backslash\overline{\overline{fg}f}\right)f$
Lemma 4.9.(9)
$\displaystyle=~{}\left(\overline{f}\backslash\overline{fg}\overline{f}\right)f$
[R.3]
$\displaystyle=~{}\left(1_{A}\backslash\overline{fg}\right)\overline{f}f$ (12)
$\displaystyle=~{}\left(1_{A}\backslash\overline{fg}\right)f$ [R.1]
$\displaystyle=~{}\overline{fg}^{c}f$ Def. of $\overline{fg}^{c}$

So $f\overline{g}^{c}=\overline{fg}^{c}f$

$\Box$

Here are the complements of the restriction idempotents in our two main
examples:

###### Example 4.10

In $\mathsf{PAR}$, for a subset $U\subseteq X$, the complement of its
corresponding restriction idempotent $e_{U}$ is the restriction idempotent
associated to the complement of $U$, $U^{c}=\\{x\in X|x\notin X\\}\subseteq
X$, so $e^{c}_{U}=e_{U^{c}}$. As such we have that:

$e^{c}_{U}(x)=\begin{cases}x&\text{if }x\notin U\\\ \uparrow&\text{if }x\in
U\end{cases}$

So in particular, for a partial function $f:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Y$, the complement of its restriction
$\overline{f}$ is given by:

$\overline{f}^{c}(x)=\begin{cases}x&\text{if }f(x)\uparrow\\\
\uparrow&\text{if }f(x)\downarrow\end{cases}$

###### Example 4.11

In $k\text{-}\mathsf{CALG}_{\bullet}$, for an idempotent element $u\in A$, the
complement of its associated corestriction idempotent $e_{u}$ is the
corestriction idempotent associated to the idempotent $1-u$, that is,
$e^{c}_{u}=e_{1-u}$ and so:

$e^{c}_{u}(a)=a-ua$

So for a non-unital $k$-algebra morphism $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, the complement of its corestriction
$\overline{f}$ is given by:

$\overline{f}^{c}(b)=b-f(1)b$

##  5 From Classical Products to Restriction Products and Coproducts

In this section, we will show how classical products are related to
restriction products and restriction coproducts via restriction idempotent
splitting. Furthermore, using split restriction idempotents, we will also be
able to show that in a classical restriction category, if the product exists,
then it must always be of the form $A\&B=A\oplus B\oplus(A\times B)$.

###### Definition 5.1

In a restriction category $\mathbb{X}$, a restriction idempotent
$e:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
is said to be split [5, Sec 2.3.3] if there exists maps
$r:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}X$
and $s:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ such that $rs=e$ and $sr=1_{X}$.

Suppose we are in a restriction category with products. By Lemma 2.2.(v), we
have that
${\overline{p_{0}}~{}\overline{p_{1}}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B}$ is a restriction idempotent. The
splitting of this restriction idempotent relates the product $A\&B$ to the
restriction product $A\times B$.

###### Lemma 5.2

Let $\mathbb{X}$ be a restriction category with binary products. Then
$\mathbb{X}$ has binary restriction products if and only if for every pair of
objects $A$ and $B$, the restriction idempotent
$\overline{p_{0}}~{}\overline{p_{1}}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$ splits. Explicitly:

  1. (i)

If the restriction product $A\times B$ exists, then
$\overline{p_{0}}~{}\overline{p_{1}}$ splits via $\langle
p_{0},p_{1}\rangle:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times B$ and
$\left\llangle\pi_{0},\pi_{1}\right\rrangle:A\times
B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$.

  2. (ii)

If $\overline{p_{0}}~{}\overline{p_{1}}$ splits via
$r:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times B$ and $s:A\times
B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$, for some object $A\times B$, then
$A\times B$ is a restriction product of $A$ and $B$ with projections
$\pi_{0}:A\times B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ and $\pi_{1}:A\times
B\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
defined as $\pi_{0}=sp_{0}$ and $\pi_{1}=sp_{1}$.

Proof: First recall some useful basic identities about the restriction product
[3, Prop 2.8]:

$\displaystyle k\langle f,g\rangle=\langle kf,kg\rangle$ (15)
$\displaystyle\langle\pi_{0},\pi_{1}\rangle=1_{A\times B}$ (16)

  1. (i)

Suppose that $A\times B$ is a restriction product of $A$ and $B$. We must show
that $\langle
p_{0},p_{1}\rangle\left\llangle\pi_{0},\pi_{1}\right\rrangle=\overline{p_{0}}~{}\overline{p_{1}}$
and $\left\llangle\pi_{0},\pi_{1}\right\rrangle\langle
p_{0},p_{1}\rangle=1_{A\times B}$. So we compute:

$\displaystyle\langle
p_{0},p_{1}\rangle\left\llangle\pi_{0},\pi_{1}\right\rrangle$
$\displaystyle=~{}\left\llangle\langle p_{0},p_{1}\rangle\pi_{0},\langle
p_{0},p_{1}\rangle\pi_{1}\right\rrangle$ (5)
$\displaystyle=~{}\left\llangle\overline{p_{1}}p_{0},\overline{p_{0}}p_{1}\right\rrangle$
(2) $\displaystyle=~{}\left\llangle
p_{0},p_{1}\right\rrangle\overline{p_{0}}~{}\overline{p_{1}}$ Lemma 3.1.(iii)
$\displaystyle=~{}\overline{p_{0}}~{}\overline{p_{1}}$ $\left\llangle
p_{0},p_{1}\right\rrangle=1_{A\&B}$
$\displaystyle\left\llangle\pi_{0},\pi_{1}\right\rrangle\langle
p_{0},p_{1}\rangle$
$\displaystyle=~{}\left\langle\left\llangle\pi_{0},\pi_{1}\right\rrangle
p_{0},\left\llangle\pi_{0},\pi_{1}\right\rrangle p_{1}\right\rangle$ (15)
$\displaystyle=~{}\left\langle\pi_{0},\pi_{1}\right\rangle$ (4)
$\displaystyle=~{}1_{A\times B}$ (16)

So we conclude that $\overline{p_{0}}~{}\overline{p_{1}}$ splits.

  2. (ii)

Suppose that $\overline{p_{0}}~{}\overline{p_{1}}$ splits via
${r:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times B}$ and $s:A\times
B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$, so:

$\displaystyle rs=\overline{p_{0}}~{}\overline{p_{1}}$ $\displaystyle
sr=1_{A\times B}$ (17)

We must first show that the suggested projections are total. First note that
from (17) it follows that:

$\displaystyle s\overline{p_{i}}=s$ (18)

Furthermore, since $s$ is a section, $s$ is monic, and thus $s$ is total
(Lemma 2.2.(iii)). So we compute:

$\displaystyle\overline{\pi_{i}}$ $\displaystyle=~{}\overline{sp_{i}}$ Def. of
$\pi_{i}$ $\displaystyle=~{}\overline{s\overline{p_{i}}}$ Lemma 2.2.(i)
$\displaystyle=~{}\overline{s}$ (18) $\displaystyle=~{}1_{A\times B}$ $s$
total

So $\pi_{0}$ and $\pi_{1}$ are total as needed. Now given a pair of maps
$f:C\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
and $g:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$, define $\langle
f,g\rangle:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\times B$ as the following composite:

$\displaystyle\langle f,g\rangle=\left\llangle f,g\right\rrangle r$ (19)

Then we compute:

$\displaystyle\langle f,g\rangle\pi_{0}$ $\displaystyle=~{}\left\llangle
f,g\right\rrangle rsp_{0}$ Def. of $\langle-,-\rangle$
$\displaystyle=~{}\left\llangle
f,g\right\rrangle\overline{p_{0}}~{}\overline{p_{1}}p_{0}$ (17)
$\displaystyle=~{}\left\llangle\overline{g}f,\overline{f}g\right\rrangle
p_{0}$ Lemma 3.1.(iii) $\displaystyle=~{}\overline{g}f$ (4)

So $\langle f,g\rangle\pi_{0}=\overline{g}f$, and similarly we can compute
that $\langle f,g\rangle\pi_{1}=\overline{f}g$. Lastly for uniqueness, suppose
that there was another map $h$ such that $h\pi_{0}=\overline{f}g$ and
$h\pi_{1}=\overline{g}f$. Then we compute:

$\displaystyle h$ $\displaystyle=~{}hsr$ (17)
$\displaystyle=~{}hs\left\llangle p_{0},p_{1}\right\rrangle r$ $\left\llangle
p_{0},p_{1}\right\rrangle=1_{A\&B}$ $\displaystyle=~{}\left\llangle
hsp_{0},hsp_{1}\right\rrangle r$ (5) $\displaystyle=~{}\left\llangle
h\pi_{0},h\pi_{1}\right\rrangle r$ Def. of $\pi_{i}$
$\displaystyle=~{}\left\llangle\overline{g}f,\overline{g}f\right\rrangle r$
Assumption on $h$ $\displaystyle=~{}\left\llangle
f,g\right\rrangle\overline{p_{0}}~{}\overline{p_{1}}r$ Lemma 3.1.(iii)
$\displaystyle=~{}\left\llangle f,g\right\rrangle r$ (17)
$\displaystyle=~{}\langle f,g\rangle$ Def. of $\langle-,-\rangle$

So $\langle f,g\rangle$ is unique. Thus $A\times B$ is the restriction product
of $A$ and $B$.

$\Box$

To relate the product to the restriction coproduct, we will need to work in a
classical restriction category. By Lemma 4.9.(i) and Lemma 4.3.(vi),
$\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$ is a restriction idempotent. The
splitting of this restriction idempotent relates the product $A\&B$ to the
restriction coproduct $A\oplus B$. Before showing this, here are useful
identities we will need for the proof.

###### Lemma 5.3

In a classical restriction category $\mathbb{X}$ with binary products,

  1. (i)

$\llangle f,g\rrangle\overline{p_{0}}^{c}=\llangle
0,\overline{f}^{c}g\rrangle$ and $\llangle
f,g\rrangle\overline{p_{1}}^{c}=\llangle\overline{g}^{c}f,0\rrangle$;

  2. (ii)

$\llangle f,g\rrangle\overline{p_{0}}^{c}p_{1}=\overline{f}^{c}g$ and
$\llangle f,g\rrangle\overline{p_{1}}^{c}p_{0}=\overline{g}^{c}f$;

  3. (iii)

$\llangle 0,0\rrangle=0$;

  4. (iv)

$\overline{p_{0}}^{c}\perp\overline{p_{1}}^{c}$, or in other words,
$\overline{p_{0}}^{c}~{}\overline{p_{1}}^{c}=0$;

  5. (v)

$\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}=\llangle\overline{p_{1}}^{c}p_{0},\overline{p_{0}}^{c}p_{1}\rrangle$;

  6. (vi)

$\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\perp\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle$ and
$\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle=\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$;

  7. (vii)

$\llangle 1_{A},0\rrangle\overline{p_{0}}^{c}=0$, $\llangle
1_{A},0\rrangle\overline{p_{1}}^{c}=\llangle 1_{A},0\rrangle$, $\llangle
0,1_{B}\rrangle\overline{p_{0}}^{c}=\llangle 0,1_{B}\rrangle$, and $\llangle
0,1_{B}\rrangle\overline{p_{1}}^{c}=0$;

  8. (viii)

$\overline{p_{0}}^{c}$ is a split via the maps
$\overline{p_{0}}^{c}p_{1}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ and ${\llangle
0,1_{B}\rrangle:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B}$, and $\overline{p_{1}}^{c}$ is a
split via the maps
$\overline{p_{1}}^{c}p_{0}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ and $\llangle
1_{A},0\rrangle:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$.

Proof:

  1. (i)

We compute:

$\displaystyle\llangle f,g\rrangle\overline{p_{0}}^{c}$
$\displaystyle=~{}\overline{\llangle f,g\rrangle p_{0}}^{c}\llangle
f,g\rrangle$ Lemma 4.9.(ix) $\displaystyle=~{}\overline{f}^{c}\llangle
f,g\rrangle$ (4)
$\displaystyle=~{}\llangle\overline{f}^{c}f,\overline{f}^{c}g\rrangle$ (5)
$\displaystyle=~{}\llangle 0,\overline{f}^{c}g\rrangle$ Lemma 4.9.(vi)

So $\llangle f,g\rrangle\overline{p_{0}}^{c}=\llangle
0,\overline{f}^{c}g\rrangle$, and similarly we can show that $\llangle
f,g\rrangle\overline{p_{1}}^{c}=\llangle\overline{g}^{c}f,0\rrangle$.

  2. (ii)

This follows immediatly from (i).

  3. (iii)

Postcomposing zero by the projections results in zero, $0p_{i}=0$. So by the
universal property of the product, it follows that $\llangle 0,0\rrangle=0$.

  4. (iv)

By Lemma 4.9.(vi), postcomposing $\overline{p_{0}}^{c}\overline{p_{1}}^{c}$ by
the projections gives ${\overline{p_{0}}^{c}\overline{p_{1}}^{c}p_{i}=0}$.
Thus by the universal property of the product, it follows that
$\overline{p_{0}}^{c}\overline{p_{1}}^{c}=\llangle 0,0\rrangle$. Thus by
(iii), $\overline{p_{0}}^{c}\overline{p_{1}}^{c}=0$, and so
$\overline{p_{0}}^{c}\perp\overline{p_{1}}^{c}$.

  5. (v)

We compute:

$\displaystyle\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)p_{0}$
$\displaystyle=~{}\overline{p_{0}}^{c}p_{0}\vee\overline{p_{1}}^{c}p_{0}$
Lemma 4.3.(iii) $\displaystyle=~{}0\vee\overline{p_{1}}^{c}p_{0}$ Lemma
4.9.(vi) $\displaystyle=~{}\overline{p_{1}}^{c}p_{0}$ Lemma 4.3.(ii)

So
$\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)p_{0}=\overline{p_{1}}^{c}p_{0}$,
and similarly we can show that
$\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)p_{1}=\overline{p_{0}}^{c}p_{1}$.
So by the universal property of the product, it follows that
$\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}=\llangle\overline{p_{1}}^{c}p_{0},\overline{p_{0}}^{c}p_{1}\rrangle$.

  6. (vi)

To show these maps are disjoint, we compute the following:

$\displaystyle\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle p_{0}$
$\displaystyle=~{}\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}0$
(4) $\displaystyle=~{}0$
$\displaystyle\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle p_{1}$
$\displaystyle=~{}\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\overline{p_{0}}^{c}p_{1}$
(4)
$\displaystyle=~{}\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\overline{p_{0}}^{c}\overline{p_{1}}p_{1}$
[R.1]
$\displaystyle=~{}\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\overline{p_{1}}\overline{p_{0}}^{c}p_{1}$
Lemma 2.2.(v)
$\displaystyle=~{}\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle
p_{1}}\overline{p_{0}}^{c}p_{1}$ [R.3]
$\displaystyle=~{}\overline{0}\overline{p_{0}}^{c}p_{1}$ (4)
$\displaystyle=~{}0$ Rest. zero

So by universal property of the product, it follows that
$\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle=\llangle 0,0\rrangle$. By (iii),
this means that
$\overline{\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle}\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle=0$. Thus
$\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\perp\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle$ as desired. So we can take their
join and compute:

$\displaystyle\left(\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle\right)p_{0}$
$\displaystyle=~{}\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle
p_{0}\vee\left\llangle 0,\overline{p_{0}}^{c}p_{1}\right\rrangle p_{0}$ Lemma
4.3.(iii) $\displaystyle=~{}\overline{p_{1}}^{c}p_{0}p_{0}\vee 0$ (4)
$\displaystyle=~{}\overline{p_{1}}^{c}p_{0}$ Lemma 4.3.(ii)

So we have the equality
$\left(\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle\right)p_{0}=\overline{p_{1}}^{c}p_{0}$
holds, and similarly we can also compute that
$\left(\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle\right)p_{1}=\overline{p_{0}}^{c}p_{1}$.
Thus by the universal property of the product, it follows that
$\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle=\llangle\overline{p_{1}}^{c}p_{0},\overline{p_{0}}^{c}p_{1}\rrangle$.
By (v), it follows that
$\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle=\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$
as desired.

  7. (vii)

These follow from (i) and Lemma 4.9.(v).

  8. (viii)

First observe that $\overline{p_{0}}^{c}p_{1}\llangle 0,1_{B}\rrangle p_{0}=0$
and $\overline{p_{0}}^{c}p_{1}\llangle 0,1_{B}\rrangle
p_{1}=\overline{p_{0}}^{c}p_{1}$. By Lemma 4.9.(vi), we also that
$\overline{p_{0}}^{c}p_{0}=0$. Thus by the universal property of the product,
it follows that $\overline{p_{0}}^{c}p_{1}\llangle
0,1_{B}\rrangle=\overline{p_{0}}^{c}$. By Lemma 5.3.(vii), we also have that
$\llangle 0,1_{B}\rrangle\overline{p_{0}}^{c}p_{1}=1_{B}$. Therefore, we have
that $\overline{p_{0}}^{c}$ splits, and similarly we can also show that
$\overline{p_{1}}^{c}$ splits.

$\Box$

###### Lemma 5.4

Let $\mathbb{X}$ be a classical restriction category with binary products.
Then $\mathbb{X}$ has finite restriction coproducts if and only if for every
pair of objects $A$ and $B$, the restriction idempotent
$\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$ splits. Explicitly:

  1. (i)

If the restriction coproduct $A\oplus B$ exists, then the restriction
idempotent $\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$ splits via the maps
$\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B$ and
$\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B$.

  2. (ii)

If the restriction idempotent $\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$
splits via maps $r:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B$ and ${s:A\oplus
B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B}$, then $A\oplus B$ is a
restriction product of $A$ and $B$ with injections
$\iota_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B$ and
$\iota_{1}:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B$ defined as
$\iota_{0}=\llangle 1_{A},0\rrangle r$ and $\iota_{1}=\llangle 0,1_{B}\rrangle
r$.

Proof:

  1. (i)

Suppose that $A\oplus B$ is the restriction coproduct of $A$ and $B$. We first
check that $\overline{p_{1}}^{c}p_{0}\iota_{0}$ and
$\overline{p_{0}}^{c}p_{1}\iota_{1}$ are indeed disjoint:

$\displaystyle\overline{\overline{p_{1}}^{c}p_{0}\iota_{0}}\overline{p_{0}}^{c}p_{1}\iota_{1}$
$\displaystyle=~{}\overline{\overline{p_{1}}^{c}p_{0}}\overline{p_{0}}^{c}p_{1}\iota_{1}$
Lemma 2.2.(ii) and $\iota_{0}$ total
$\displaystyle=~{}\overline{p_{1}}^{c}\overline{p_{0}}\overline{p_{0}}^{c}p_{1}\iota_{1}$
Lemma 2.2.(vi) and Lemma 4.9.(i) $\displaystyle=~{}0$ Lemma 4.9.(ii)

So
$\overline{p_{1}}^{c}p_{0}\iota_{0}\perp\overline{p_{0}}^{c}p_{1}\iota_{1}$,
thus we can indeed take their join
$\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}$.
Now we must show both equalities that
$\left(\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}\right)\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle=\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$
and
$\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle\left(\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}\right)=1_{A\oplus
B}$. So we compute:

$\displaystyle\left(\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}\right)\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle$
$\displaystyle=~{}\overline{p_{1}}^{c}p_{0}\iota_{0}\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle\vee\overline{p_{0}}^{c}p_{1}\iota_{1}\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle$
Lemma 4.3.(iii)
$\displaystyle=~{}\left\llangle\overline{p_{1}}^{c}p_{0}\iota_{0}\iota^{\circ}_{0},\overline{p_{1}}^{c}p_{0}\iota_{0}\iota^{\circ}_{1}\right\rrangle\vee\left\llangle\overline{p_{0}}^{c}p_{1}\iota_{1}\iota^{\circ}_{0},\overline{p_{0}}^{c}p_{1}\iota_{1}\iota^{\circ}_{1}\right\rrangle$
(5)
$\displaystyle=~{}\left\llangle\overline{p_{1}}^{c}p_{0},0\right\rrangle\vee\left\llangle
0,\overline{p_{0}}^{c}p_{1}\right\rrangle$ Lemma 3.6.(iii)
$\displaystyle=~{}\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$ Lemma 5.3.(vi)
$\displaystyle\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle\left(\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\overline{p_{0}}^{c}p_{1}\iota_{1}\right)$
$\displaystyle=~{}\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle\overline{p_{1}}^{c}p_{0}\iota_{0}\vee\llangle\iota^{\circ}_{0},\iota^{\circ}_{1}\rrangle\overline{p_{0}}^{c}p_{1}\iota_{1}$
[J.3]
$\displaystyle=~{}\overline{\iota^{\circ}_{1}}^{c}\iota^{\circ}_{0}\iota_{0}\vee\overline{\iota^{\circ}_{0}}^{c}\iota^{\circ}_{1}\iota_{1}$
Lemma 5.3.(ii)
$\displaystyle=~{}\overline{\iota^{\circ}_{1}}^{c}\vee\overline{\iota^{\circ}_{0}}^{c}$
Lemma 3.6.(iii)
$\displaystyle=~{}\left(\overline{\iota^{\circ}_{1}}~{}\overline{\iota^{\circ}_{0}}\right)^{c}$
Lemma 4.9.(iv) $\displaystyle=~{}0^{c}$ Lemma 3.6.(v)
$\displaystyle=~{}1_{A\oplus B}$ Lemma 4.9.(v)

So we conclude that $\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$ splits.

  2. (ii)

Suppose that $\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$ splits via
$r:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B$ and $s:A\oplus
B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$, so:

$\displaystyle rs=\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$ $\displaystyle
sr=1_{A\oplus B}$ (20)

We must first show that the suggested injections are total. First note again
that since $s$ is a section, $s$ is monic, and thus $s$ is total (Lemma
2.2.(iii)). Therefore it follows from Lemma 2.2.(ii) that:

$\displaystyle\overline{r}=\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$ (21)

We then compute that:

$\displaystyle\overline{\iota_{0}}$ $\displaystyle=~{}\overline{\llangle
1_{A},0\rrangle r}$ Def. of $\iota_{0}$ $\displaystyle=~{}\overline{\llangle
1_{A},0\rrangle\overline{r}}$ Lemma 2.2.(i)
$\displaystyle=~{}\overline{\llangle
1_{A},0\rrangle\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)}$
(21) $\displaystyle=~{}\overline{\llangle
1_{A},0\rrangle\overline{p_{0}}^{c}\vee\llangle
1_{A},0\rrangle\overline{p_{1}}^{c}}$ [J.3]
$\displaystyle=~{}\overline{0\vee\llangle 1_{A},0\rrangle}$ Lemma 5.3.(vii)
$\displaystyle=~{}\overline{\llangle 1_{A},0\rrangle}$ Lemma 4.3.(ii)
$\displaystyle=~{}\overline{\llangle 1_{A},\overline{1_{A}}0\rrangle}$ $1_{A}$
total $\displaystyle=~{}\overline{\llangle 1_{A},0\rrangle\overline{p_{0}}}$
Lemma 3.1.(ii) $\displaystyle=~{}\overline{\llangle 1_{A},0\rrangle p_{0}}$
Lemma 2.2.(i) $\displaystyle=~{}\overline{1_{A}}$ (4) $\displaystyle=~{}1_{A}$
$1_{A}$ total

So $\overline{\iota_{0}}=1_{A}$, and similarly we can show that
$\overline{\iota_{1}}=1_{B}$. So the injection maps are indeed total. Now for
a pair of maps $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ and
$g:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$, consider the composites
$\overline{p_{1}}^{c}p_{0}f$ and $\overline{p_{0}}^{c}p_{1}g$. We show these
are disjoint:

$\displaystyle\overline{\overline{p_{1}}^{c}p_{0}f}\overline{p_{0}}^{c}p_{1}g$
$\displaystyle=~{}\overline{p_{0}f}\overline{p_{1}}^{c}\overline{p_{0}}^{c}p_{1}g$
Lemma 2.2.(vi) and Lemma 4.9.(i) $\displaystyle=~{}0$ Lemma 5.3.(iv)

So $\overline{p_{1}}^{c}p_{0}f\perp\overline{p_{0}}^{c}p_{1}g$. Thus we can
take their join and define $[f,g]:A\oplus B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ as follows:

$\displaystyle[f,g]:=s\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$
(22)

Then we compute:

$\displaystyle\iota_{0}[f,g]$ $\displaystyle=~{}\llangle 1_{A},0\rrangle
rs\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$ Def.
of $\iota_{0}$ and $[f,g]$
$\displaystyle=~{}\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$
(20) $\displaystyle=~{}\left(\llangle
1_{A},0\rrangle\overline{p_{0}}^{c}\vee\llangle
1_{A},0\rrangle\overline{p_{1}}^{c}\right)\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$
[J.3] $\displaystyle=~{}\left(0\vee\llangle
1_{A},0\rrangle\right)\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$
Lemma 5.3.(vii) $\displaystyle=~{}\llangle
1_{A},0\rrangle\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$
Lemma 4.3.(ii) $\displaystyle=~{}\llangle
1_{A},0\rrangle\overline{p_{1}}^{c}p_{0}f\vee\llangle
1_{A},0\rrangle\overline{p_{0}}^{c}p_{1}g$ [J.3] $\displaystyle=~{}\llangle
1_{A},0\rrangle p_{0}f\vee 0$ Lemma 5.3.(vii) $\displaystyle=~{}\llangle
1_{A},0\rrangle p_{0}f$ Lemma 4.3.(ii) $\displaystyle=~{}f$ (4)

So $\iota_{0}[f,g]=f$, and similarly we can show that $\iota_{1}[f,g]=g$.
Lastly for uniqueness, suppose that there is a map $h:A\oplus
B\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}C$
such that $\iota_{0}h=f$ and $\iota_{1}h=g$. Now we first compute that:

$\displaystyle sp_{0}$ $\displaystyle=~{}srsp_{0}$ (20)
$\displaystyle=~{}s\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)p_{0}$
$\displaystyle=~{}s\left(\overline{p_{0}}^{c}p_{0}\vee\overline{p_{1}}^{c}p_{0}\right)$
Lemma 4.3.(iii)
$\displaystyle=~{}s\left(0\vee\overline{p_{1}}^{c}p_{0}\right)$ Lemma 4.9.(vi)
$\displaystyle=~{}s\overline{p_{1}}^{c}p_{0}$ Lemma 4.3.(ii)

So $sp_{0}=s\overline{p_{1}}^{c}p_{0}$, and similarly we can show that
$sp_{1}=s\overline{p_{0}}^{c}p_{1}$. Then we compute:

$\displaystyle h$ $\displaystyle=~{}srsrh$ (20)
$\displaystyle=~{}s\left(\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}\right)rh$
(20)
$\displaystyle=~{}s\left(\llangle\overline{p_{1}}^{c}p_{0},0\rrangle\vee\llangle
0,\overline{p_{0}}^{c}p_{1}\rrangle\right)rh$ Lemma 5.3.(vi)
$\displaystyle=~{}s\left(\llangle\overline{p_{1}}^{c}p_{0},0\rrangle
rh\vee\llangle 0,\overline{p_{0}}^{c}p_{1}\rrangle rh\right)$ Lemma 4.3.(iii)
$\displaystyle=~{}s\left(\overline{p_{1}}^{c}p_{0}\llangle 1_{A},0\rrangle
rh\vee\overline{p_{0}}^{c}p_{1}\llangle 0,1_{B}\rrangle rh\right)$ (5)
$\displaystyle=~{}s\left(\overline{p_{1}}^{c}p_{0}\iota_{0}h\vee\overline{p_{0}}^{c}p_{1}\iota_{1}h\right)$
Def. of $\iota_{j}$
$\displaystyle=~{}s\left(\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\right)$
Assump. on $h$ $\displaystyle=~{}[f,g]$ Def. of $[f,g]$

So $[f,g]$ is unique. Thus we conclude that $A\oplus B$ is a restriction
coproduct.

$\Box$

We will now explain how in a classical restriction category with both products
$\&$ and restriction products $\times$, it turns out that the product $A\&B$
is always the restriction coproduct of $A$, $B$, and $A\times B$, that is,
$A\&B=A\oplus B\oplus(A\times B)$. To do so, we will make use of the
following:

###### Lemma 5.5

[8, Lemma 7.7] Let $\mathbb{X}$ be a classical restriction category, and let
${e_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A}$,
$e_{1}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, and
$e_{2}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$ be split restriction idempotents,
with splittings $r_{i}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A_{i}$ and
$s_{i}:A_{i}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, that are pairwise disjoint and such
that $e_{0}\vee e_{1}\vee e_{2}=1_{A}$. Then $A$ is a restriction coproduct of
$A_{0}$, $A_{1}$, and $A_{2}$ where the injections are
$s_{i}:A_{i}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, and furthermore, for maps
$f_{0}:A_{0}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$,
$f_{1}:A_{1}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$, and
$f_{2}:A_{2}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$, their copairing
$[f_{0},f_{1},f_{2}]:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ is defined as
$[f_{0},f_{1},f_{2}]=r_{0}f_{0}\vee r_{1}f_{1}\vee r_{2}f_{2}$.

###### Proposition 5.6

Let $\mathbb{X}$ be a classical restriction category with binary products and
binary restriction products. Then for each object $A$ and $B$, their product
$A\&B$ is a restriction coproduct of $A$, $B$, and $A\times B$ with injection
maps ${\iota_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B}$,
$\iota_{1}:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\&B$, and $\iota_{2}:A\times
B\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A\&B$
respectively defined as follows:

$\displaystyle\iota_{0}=\llangle 1_{A},0\rrangle$
$\displaystyle\iota_{1}=\llangle 0,1_{B}\rrangle$
$\displaystyle\iota_{2}=\llangle\pi_{0},\pi_{1}\rrangle$

and furthermore, for maps $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$,
$g:B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$, and $h:A\times
B\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}C$,
their copairing $[f,g,h]:A\&B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}C$ is defined as follows:

$[f,g,h]=\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\vee\langle
p_{0},p_{1}\rangle h$

Moreover, the following equalities hold:

$\displaystyle p_{0}=[1_{A},0,\pi_{0}]$ $\displaystyle
p_{1}=[0,1_{B},\pi_{1}]$

Proof: We wish to make use of Lemma 5.5. To do so, we need to provide three
split restriction idempotents of type $A\&B$, that are pairwise disjoint, and
whose join is equal to the identity. So consider the restriction idempotents
$e_{0}:=\overline{p_{1}}^{c}$, $e_{1}:=\overline{p_{0}}^{c}$, and
$e_{2}:=\overline{p_{0}}~{}\overline{p_{1}}$. By Lemma 5.3.(viii),
$\overline{p_{1}}^{c}$ splits through $A$ via
$r_{0}:=\overline{p_{1}}^{c}p_{0}$ and $s_{0}:=\llangle 1_{A},0\rrangle$,
while $\overline{p_{0}}^{c}$ splits through $B$ via
$r_{1}:=\overline{p_{0}}^{c}p_{1}$ and $s_{1}:=\llangle 0,1_{B}\rrangle$. By
Lemma 5.2, we also know that $\overline{p_{0}}~{}\overline{p_{1}}$ splits
through $A\times B$ via $r_{2}:=\langle p_{0},p_{1}\rangle$ and
$s_{2}:=\left\llangle\pi_{0},\pi_{1}\right\rrangle$. Now by Lemma 5.3.(iv), we
have that $\overline{p_{0}}^{c}\perp\overline{p_{1}}^{c}$, and by Lemma
4.9.(ii), it follows that
$\overline{p_{0}}~{}\overline{p_{1}}\perp\overline{p_{j}}^{c}$ as well. So our
chosen restriction idempotents are pairwise disjoint. Taking their join, we
compute that:

$\displaystyle\overline{p_{1}}^{c}\vee\overline{p_{0}}^{c}\vee\overline{p_{0}}~{}\overline{p_{1}}$
$\displaystyle=~{}\overline{p_{0}}~{}\overline{p_{1}}\vee\overline{p_{0}}^{c}\vee\overline{p_{1}}^{c}$
$\displaystyle=~{}\overline{p_{0}}~{}\overline{p_{1}}\vee(\overline{p_{0}}~{}\overline{p_{1}})^{c}$
Lemma 4.9.(ii) $\displaystyle=~{}1_{A\&B}$ Lemma 4.9.(ii)

Thus
$\overline{p_{1}}^{c}\vee\overline{p_{0}}^{c}\vee\overline{p_{0}}~{}\overline{p_{1}}=1_{A\&B}$
as desired. Thus, we can apply Lemma 5.5 to obtain that $A\&B$ is the
restriction coproduct of $A$, $B$, and $A\times B$, with the injections given
by $\iota_{0}=\llangle 1_{A},0\rrangle$, $\iota_{1}=\llangle 0,1_{B}\rrangle$,
and $\iota_{2}=\llangle\pi_{0},\pi_{1}\rrangle$, and the copairing by
$[f,g,h]=\overline{p_{1}}^{c}p_{0}f\vee\overline{p_{0}}^{c}p_{1}g\vee\langle
p_{0},p_{1}\rangle h$, as desired. Now by definition, we also have that
$\iota_{0}p_{0}=1_{A}$, $\iota_{1}p_{0}=0$, and $\iota_{2}p_{0}=\pi_{0}$. Thus
by the couniversal of the coproduct, it follows that
$p_{0}=[1_{A},0,\pi_{0}]$. Similarly, we can also show that
$p_{1}=[0,1_{B},\pi_{1}]$. $\Box$

Thus if a distributive restriction category is classical and has finite
products, said product and projections must be the classical product and
classical projections.

##  6 Classical Distributive Restriction Categories

In this section we prove the main result of this paper that a distributive
restriction category is classical if and only if it has classical products.

We begin by showing that a classical distributive category (by which we simply
mean a distributive restriction category that is also classical, and no
further assumptions) has classical products. First, here is a useful lemma
about the restrictions of the projections and their complements.

###### Lemma 6.1

In a classic distributive restriction category $\mathbb{X}$,

  1. (i)

$\overline{p_{0}}=\iota^{\circ}_{0}\iota_{0}\vee\iota^{\circ}_{2}\iota_{2}$
and
$\overline{p_{0}}=\iota^{\circ}_{1}\iota_{1}\vee\iota^{\circ}_{2}\iota_{2}$;

  2. (ii)

$\overline{p_{0}}^{c}=\iota^{\circ}_{1}\iota_{1}$ and
$\overline{p_{1}}^{c}=\iota^{\circ}_{0}\iota_{0}$;

  3. (iii)

$\overline{p_{1}}^{c}p_{0}=\iota^{\circ}_{0}$ and
$\overline{p_{0}}^{c}p_{1}=\iota^{\circ}_{1}$

Proof:

  1. (i)

This follows from Lemma 3.13.(i) and Lemma 4.4.(i), so
$\overline{p_{0}}=1_{A}\oplus 0\oplus 1_{A\times
B}=\iota^{\circ}_{0}\iota_{0}\vee\iota^{\circ}_{2}\iota_{2}$ and
$\overline{p_{1}}=0\oplus 1_{B}\oplus 1_{A\times
B}=\iota^{\circ}_{1}\iota_{1}\vee\iota^{\circ}_{2}\iota_{2}$.

  2. (ii)

To show this, we make use of Lemma 4.9.(iii). Indeed, recall that by Lemma
3.6.(iv), $\iota^{\circ}_{1}\iota_{1}=\overline{\iota^{\circ}_{1}}$ is a
restriction idempotent. So we compute:

$\displaystyle\overline{p_{0}}\iota^{\circ}_{1}\iota_{1}$
$\displaystyle=~{}\left(1_{A}\oplus 0\oplus 1_{A\times B}\right)\left(0\oplus
1_{B}\oplus 0\right)$ Lemma 3.13.(i) and Lemma 3.6.(ii)
$\displaystyle=~{}0\oplus 0\oplus 0$ (7) $\displaystyle=~{}0$
$\displaystyle\overline{p_{0}}\vee\iota^{\circ}_{1}\iota_{1}$
$\displaystyle=~{}\iota^{\circ}_{0}\iota_{0}\vee\iota^{\circ}_{2}\iota_{2}\vee\iota^{\circ}_{1}\iota_{1}$
Lemma 6.1.(i)
$\displaystyle=~{}\iota^{\circ}_{0}\iota_{0}\vee\iota^{\circ}_{1}\iota_{1}\vee\iota^{\circ}_{2}\iota_{2}$
$\displaystyle=~{}1_{A\oplus B\oplus(A\times B)}$ Lemma 4.4.(ii)

Then by Lemma 4.9.(iii), it follows that
$\overline{p_{0}}^{c}=\iota^{\circ}_{1}\iota_{1}$. Similarly, we can show that
$\overline{p_{1}}^{c}=\iota^{\circ}_{0}\iota_{0}$.

  3. (iii)

By definition of the classical projections and (ii), it follows that
$\overline{p_{1}}^{c}p_{0}=\iota^{\circ}_{0}$ and
$\overline{p_{0}}^{c}p_{1}=\iota^{\circ}_{1}$ as desired.

$\Box$

###### Proposition 6.2

A classical distributive restriction category has classical products.

Proof: Let $\mathbb{X}$ be a classical distributive restriction category.
Since $\mathbb{X}$ has restriction zeroes by assumption, we need only show
that $A\oplus B\oplus(A\times B)$ is a product of $A$ and $B$. So let
$f:C\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}A$
and ${g:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B}$ be a given pair of maps. First
consider the parallel maps $\overline{g}^{c}f\iota_{0}$,
$\overline{f}^{c}g\iota_{1}$, and $\langle f,g\rangle\iota_{2}$. We first
check that:

$\displaystyle\overline{\overline{g}^{c}f\iota_{0}}\overline{f}^{c}g\iota_{1}$
$\displaystyle=~{}\overline{\overline{f}^{c}\overline{g}^{c}f\iota_{0}}g\iota_{1}$
Lemma 2.2.(vi)
$\displaystyle=~{}\overline{\overline{g}^{c}\overline{f}^{c}f\iota_{0}}g\iota_{1}$
Lemma 2.2.(v)
$\displaystyle=~{}\overline{\overline{g}^{c}0\iota_{0}}g\iota_{1}$ Lemma
4.9.(vi) $\displaystyle=~{}0$ Rest. zero map

So $\overline{g}^{c}f\iota_{0}\perp\overline{f}^{c}g\iota_{1}$. To show that
$\overline{g}^{c}f\iota_{0}$ and $\langle f,g\rangle\iota_{2}$ are disjoint,
recall that the restriction of a pair is given by the meet of the restrictions
[3, Prop 2.8]:

$\displaystyle\overline{\langle f,g\rangle}=\overline{f}~{}\overline{g}$ (23)

So we can compute:

$\displaystyle\overline{\langle
f,g\rangle\iota_{2}}\overline{g}^{c}f\iota_{0}$
$\displaystyle=~{}\overline{\langle f,g\rangle}\overline{g}^{c}f\iota_{0}$
Lemma 2.2.(ii) and $\iota_{2}$ total
$\displaystyle=~{}\overline{f}\overline{g}~{}\overline{g}^{c}f\iota_{0}$ (23)
$\displaystyle=~{}0$ Lemma 4.9.(ii)

So $\overline{g}^{c}f\iota_{0}\perp\langle f,g\rangle\iota_{2}$, and similarly
we can show that $\overline{f}^{c}g\iota_{1}\perp\langle f,g\rangle\iota_{2}$.
So $\overline{g}^{c}f\iota_{0}$, $\overline{f}^{c}g\iota_{1}$, and $\langle
f,g\rangle\iota_{2}$ are pair-wise disjoint (and thus compatible). Then define
the classical pairing $\llangle f,g\rrangle:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B\oplus(A\times B)$ as the join
of those three maps:

$\displaystyle\llangle
f,g\rrangle:=\overline{g}^{c}f\iota_{0}\vee\overline{f}^{c}g\iota_{1}\vee\langle
f,g\rangle\iota_{2}$ (24)

We now compute that:

$\displaystyle\llangle f,g\rrangle p_{0}$
$\displaystyle=~{}\left(\overline{g}^{c}f\iota_{0}\vee\overline{f}^{c}g\iota_{1}\vee\langle
f,g\rangle\iota_{2}\right)p_{0}$ (4)
$\displaystyle=~{}\overline{g}^{c}f\iota_{0}p_{0}\vee\overline{f}^{c}g\iota_{1}p_{0}\vee\langle
f,g\rangle\iota_{2}p_{0}$ Lemma 4.3.(iii)
$\displaystyle=~{}\overline{g}^{c}f\vee 0\vee\langle f,g\rangle\pi_{0}$ Def.
of $p_{0}$ $\displaystyle=~{}\overline{g}^{c}f\vee\overline{g}f$ Lemma
4.3.(ii) $\displaystyle=~{}(\overline{g}^{c}\vee\overline{g})f$ Lemma
4.3.(iii) $\displaystyle=~{}f$ Lemma 4.9.(ii)

So $\llangle f,g\rrangle p_{0}=f$, and similarly we can show that $\llangle
f,g\rrangle p_{1}=g$. Now we must show the uniqueness of $\llangle
f,g\rrangle$. So let $h:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus B\oplus(A\times B)$ be a map
such that $hp_{0}=f$ and $hp_{1}=g$. Then we first compute that:

$\displaystyle h\iota^{\circ}_{0}$
$\displaystyle=~{}h\overline{p_{1}}^{c}p_{0}$ Lemma 6.1.(iii)
$\displaystyle=~{}\overline{hp_{1}}^{c}hp_{0}$ Lemma 4.9.(ix)
$\displaystyle=~{}\overline{g}^{c}f$ Assump. on $h$

So $h\iota^{\circ}_{0}=\overline{g}^{c}f$ and similarly we can show that
$h\iota^{\circ}_{1}=\overline{f}^{c}g$. We also compute that:

$\displaystyle h\iota^{\circ}_{2}\pi_{0}$
$\displaystyle=~{}h\overline{p_{1}}p_{0}$ Lemma 3.13.(ii)
$\displaystyle=~{}\overline{hp_{1}}hp_{0}$ [R.4]
$\displaystyle=~{}\overline{g}f$ Assump. on $h$

So $h\iota^{\circ}_{2}\pi_{0}=\overline{g}f$ and similarly
$h\iota^{\circ}_{2}\pi_{1}=\overline{f}g$. Then by universal property of the
restriction product, we have that $h\iota^{\circ}_{2}=\langle f,g\rangle$. So
finally we compute that:

$\displaystyle h$
$\displaystyle=~{}h\left(\iota^{\circ}_{0}\iota_{0}\vee\iota^{\circ}_{1}\iota_{1}\vee\iota^{\circ}_{2}\iota_{2}\right)$
Lemma 4.4.(ii) $\displaystyle=~{}h\iota^{\circ}_{0}\iota_{0}\vee
h\iota^{\circ}_{1}\iota_{1}\vee h\iota^{\circ}_{2}\iota_{2}$ Lemma 4.3.(iii)
$\displaystyle=~{}\overline{g}^{c}f\iota_{0}\vee\overline{f}^{c}g\iota_{1}\vee\langle
f,g\rangle\iota_{2}$ Identities for $h$ $\displaystyle=~{}\llangle
f,g\rrangle$

Thus $A\oplus B\oplus(A\times B)$ is a product of $A$ and $B$ as desired. So
we conclude that $\mathbb{X}$ has classical products. $\Box$

We now wish to prove the converse, that if a distributive restriction category
has classical products then it is classical. To do so, we will need to make
use of _decisions_.

###### Definition 6.3

An extensive restriction category [7, Sec 3] is a coCartesian restriction
category $\mathbb{X}$ with restriction zeroes such that for every for every
map $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B_{0}\oplus\ldots\oplus B_{n}$ there
exists a (necessarily unique) map
${\mathsf{d}[f]:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\ldots\oplus A}$, called the
decision [7, Prop 2.11] of $f$, such that the following equalities hold:

  1. [D.1]

$\overline{f}=\mathsf{d}[f]\left[1_{A},\ldots,1_{A}\right]$

  2. [D.2]

$\mathsf{d}[f](f\oplus\ldots\oplus f)=f(\iota_{0}\oplus\ldots\oplus\iota_{n})$

Every distributive restriction category with restriction zeroes is extensive.
While for the proof of Prop 6.7, just knowing that decisions exist is
sufficient, it may be useful to record explicitly how decisions are
constructed and some examples.

###### Proposition 6.4

[7, Thm 5.8] A distributive restriction category with restriction zeroes is
extensive, where for a map of type $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B_{0}\oplus\ldots\oplus B_{n}$, its
decision ${\mathsf{d}[f]:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\ldots\oplus A}$ is defined as
the following composite:

$\begin{gathered}\begin{array}[c]{c}\mathsf{d}[f]\end{array}:=\begin{array}[c]{c}\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.375pt\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{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.3736pt\raise 8.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.5pt\hbox{$\scriptstyle{\left\langle\overline{f\iota^{\circ}_{0}},\ldots,\overline{f\iota^{\circ}_{n}}\right\rangle}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 54.375pt\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}}{\hbox{\kern
54.375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\times\ldots\times
A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
108.33276pt\raise 5.83499pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.575pt\hbox{$\scriptstyle{\iota_{0}\times\ldots\times\iota_{0}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 146.62506pt\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}}{\hbox{\kern
146.62506pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{(A\oplus\mathsf{1})\times\ldots\times(A\oplus\mathsf{1})}$}}}}}}}\ignorespaces}}}}\ignorespaces\\\
\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
42.86763pt\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{\cong\bigoplus\limits^{n+1}_{k=0}\left(A^{\times^{k}}\oplus\ldots\oplus
A^{\times^{k}}\right)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
61.85274pt\raise 5.33626pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.17625pt\hbox{$\scriptstyle{\iota^{\circ}_{1}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 90.86763pt\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}}{\hbox{\kern
90.86763pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\oplus\ldots\oplus
A}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{array}\end{gathered}$ (25)

###### Example 6.5

In $\mathsf{PAR}$, the decision of $f:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}Y_{0}\sqcup\ldots\sqcup Y_{n}$ is the
partial function ${\mathsf{d}[f]:X\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}X\sqcup\ldots\sqcup X}$ defined as
follows:

$\mathsf{d}[f](x)=\begin{cases}\iota_{0}(x)&\text{if }f(x)\downarrow\text{ and
}f(x)\in Y_{0}\\\ \vdots\\\ \iota_{n}(x)&\text{if }f(x)\downarrow\text{ and
}f(x)\in Y_{n}\\\ \uparrow&\text{o.w. }\end{cases}$

###### Example 6.6

In $k\text{-}\mathsf{CALG}_{\bullet}$, the codecision of
$f:A_{0}\times\ldots\times A_{n}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ is the non-unital $k$-algbera
morphism $\mathsf{d}[f]:B\times\ldots\times B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ defined as follows:

$\mathsf{d}[f](b_{0},\ldots,b_{n})=\sum^{n}_{k=0}f(0,\ldots,0,\underset{\begin{subarray}{c}k\text{-th}\\\
\text{term}\end{subarray}}{1},0,\ldots,0)b$

###### Proposition 6.7

A distributive restriction category with classical products is classical.

Proof: Let $\mathbb{X}$ be a distributive restriction category with classical
products. To prove that $\mathbb{X}$ is classical, we need to show that
$\mathbb{X}$ has joins and relative complements. Starting with the joins,
since $\mathbb{X}$ has restriction zeroes by assumption, to prove that
$\mathbb{X}$ has finite joins, it suffices to prove that $\mathbb{X}$ has
binary joins [8, Lemma 6.8]. So let $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ and
$g:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
be compatible maps, $f\smile g$. Define $f\vee
g:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
as follows:

$\begin{gathered}f\vee g:=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.375pt\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{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
23.46455pt\raise 5.8pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.57501pt\hbox{$\scriptstyle{\llangle
f,g\rrangle}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 66.375pt\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}}{\hbox{\kern
66.375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{B\oplus B\oplus(B\times
B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
156.23074pt\raise 6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.575pt\hbox{$\scriptstyle{[1_{B},1_{B},\pi_{0}]}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 201.48758pt\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}}{\hbox{\kern
201.48758pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{B}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$
(26)

We first observe that $f\vee g$ can also be expressed using the decision of
$\llangle f,g\rrangle$. So we compute the following:

$\displaystyle f\vee g$ $\displaystyle=~{}\llangle
f,g\rrangle[1_{B},1_{B},\pi_{0}]$ Def. of $f\vee g$ $\displaystyle=~{}\llangle
f,g\rrangle\left[\iota_{0}p_{0},\iota_{1}p_{1},\iota_{2}\iota^{\circ}_{2}\pi_{0}\right]$
Def. of $p_{i}$ and Lemma 3.6.(iii) $\displaystyle=~{}\llangle
f,g\rrangle\left(\iota_{0}\oplus\iota_{1}\oplus\iota_{2}\right)\left[p_{0},p_{1},\iota^{\circ}_{2}\pi_{0}\right]$
(7) $\displaystyle=~{}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right]\left(\llangle f,g\rrangle\oplus\llangle
f,g\rrangle\oplus\llangle
f,g\rrangle\right)\left[p_{0},p_{1},\iota^{\circ}_{2}\pi_{0}\right]$ [D.2]
$\displaystyle=~{}\mathsf{d}\\!\left[\llangle f,g\rrangle\right]\left[\llangle
f,g\rrangle p_{0},\llangle f,g\rrangle p_{1},\llangle
f,g\rrangle\iota^{\circ}_{2}\pi_{0}\right]$ (7)
$\displaystyle=~{}\mathsf{d}\\!\left[\llangle f,g\rrangle\right][f,g,\langle
f,g\rangle\pi_{0}]$ (4) and Lemma 3.13.(iii)
$\displaystyle=~{}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right][f,g,\overline{g}f]$ (2)

So we have that:

$\begin{gathered}f\vee g:=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.375pt\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{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
19.96455pt\raise 6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.575pt\hbox{$\scriptstyle{\mathsf{d}\left[\llangle
f,g\rrangle\right]}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern
66.375pt\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}}{\hbox{\kern
66.375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\oplus A\oplus
A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
130.42209pt\raise 6.62639pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.05139pt\hbox{$\scriptstyle{[f,g,\overline{g}f]}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 174.62506pt\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}}{\hbox{\kern
174.62506pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{B}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$
(27)

Of course, since $f\smile g$, we also have that $f\vee
g=\mathsf{d}\\!\left[\llangle f,g\rrangle\right][f,g,\overline{g}f]$. From
this, we then get that $f\vee g=\llangle f,g\rrangle[1_{B},1_{B},\pi_{1}]$ as
well. Next, we show that $f\vee g$ is an upper-bound of $f$ and $g$. So we
compute:

$\displaystyle\overline{f}(f\vee g)$ $\displaystyle=~{}\overline{f}\llangle
f,g\rrangle[1_{B},1_{B},\pi_{0}]$ (26)
$\displaystyle=~{}\llangle\overline{f}f,\overline{f}g\rrangle[1_{B},1_{B},\pi_{0}]$
(5) $\displaystyle=~{}\llangle
f,g\rrangle\overline{p_{0}}[1_{B},1_{B},\pi_{0}]$ [R.1] and Lemma 3.1.(ii)
$\displaystyle=~{}\llangle f,g\rrangle(1_{A}\oplus 0\oplus 1_{A\times
B})[1_{B},1_{B},\pi_{0}]$ Lemma 3.13.(i) $\displaystyle=~{}\llangle
f,g\rrangle[1_{B},0,\pi_{0}]$ (7) $\displaystyle=~{}\llangle f,g\rrangle
p_{0}$ Def. of $p_{0}$ $\displaystyle=~{}f$ (4)

So $f\leq f\vee g$ and similarly, we can show that $g\leq f\vee g$. Now
suppose that we have a map $h:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ such that $f\leq h$ and $g\leq h$.
Then we compute:

$\displaystyle\overline{f\vee g}h$ $\displaystyle=~{}\overline{\llangle
f,g\rrangle[1_{B},1_{B},\pi_{0}]}h$ Def. of $f\vee g$
$\displaystyle=~{}\overline{\overline{\llangle f,g\rrangle}\llangle
f,g\rrangle[1_{B},1_{B},\pi_{0}]}h$ [R.1] $\displaystyle=~{}\overline{\llangle
f,g\rrangle}~{}\overline{\llangle f,g\rrangle[1_{B},1_{B},\pi_{0}]}h$ [R.3]
$\displaystyle=~{}\overline{\llangle
f,g\rrangle[1_{B},1_{B},\pi_{0}]}~{}\overline{\llangle f,g\rrangle}h$ [R.2]
$\displaystyle=~{}\overline{\mathsf{d}\\!\left[\llangle
f,g\rrangle\right][f,g,\overline{g}f]}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right]\left[1_{A},1_{A},1_{A}\right]h$ (27) and [D.1]
$\displaystyle=~{}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right]\overline{[f,g,\overline{g}f]}\left[h,h,h\right]$ [R.4] and
(7) $\displaystyle=~{}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right]\left(\overline{f}\oplus\overline{g}\oplus\overline{\overline{g}f}\right)\left[h,h,h\right]$
(8) and [R.3] $\displaystyle=~{}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right]\left[\overline{f}h,\overline{g}h,\overline{g}\overline{f}h\right]$
(7) $\displaystyle=~{}\mathsf{d}\\!\left[\llangle
f,g\rrangle\right]\left[f,g,\overline{g}f\right]$ $f\leq h$ and $g\leq h$
$\displaystyle=~{}f\vee g$

So $f\vee g\leq h$. Thus we conclude that $f\vee g$ is indeed the join of $f$
and $g$. Next, for any map $k:A^{\prime}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A$, we compute:

$\displaystyle k(f\vee g)$ $\displaystyle=~{}k\llangle
f,g\rrangle[1_{B},1_{B},\pi_{0}]$ Def. of $f\vee g$ $\displaystyle=~{}\llangle
kf,kg\rrangle[1_{B},1_{B},0]$ (5) $\displaystyle=~{}kf\vee kg$ Def. of $kf\vee
kg$

So we conclude that $\mathbb{X}$ is indeed a join restriction category. Now
for relative complements, let $f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ and
${g:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B}$ be maps such that $f\leq g$. Define
$g\backslash f:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B$ as follows:

$\begin{gathered}g\backslash f:=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.375pt\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{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
23.46455pt\raise 5.8pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-1.57501pt\hbox{$\scriptstyle{\llangle
f,g\rrangle}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern 66.375pt\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}}{\hbox{\kern
66.375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{B\oplus B\oplus(B\times
B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
166.47269pt\raise 5.33626pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.17625pt\hbox{$\scriptstyle{\iota^{\circ}_{1}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 201.48758pt\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}}{\hbox{\kern
201.48758pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{B}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$
(28)

We first show that $g\backslash f$ and $f$ are disjoint:

$\displaystyle\overline{f}(g\backslash f)$
$\displaystyle=~{}\overline{f}\llangle f,g\rrangle\iota^{\circ}_{1}$ Def. of
$g\backslash f$
$\displaystyle=~{}\llangle\overline{f}f,\overline{f}g\rrangle\iota^{\circ}_{1}$
(5) $\displaystyle=~{}\llangle f,f\rrangle\iota^{\circ}_{1}$ [R.1] and $f\leq
g$ $\displaystyle=~{}\langle f,f\rangle\iota_{2}\iota^{\circ}_{1}$ Lemma
3.13.(v) $\displaystyle=~{}0$ Lemma 3.6.(iii)

So $g\backslash f\perp f$ as desired. To show that the join of $g\backslash f$
and $f$ is equal to $g$, we first have to compute a useful identity. So
consider the composite
$\llangle\iota^{\circ}_{1},\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$.
We will show that this composite is equal to $p_{1}$ by precomposing it with
the injection maps:

$\displaystyle\iota_{0}\llangle\iota^{\circ}_{1},\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$
$\displaystyle=~{}\llangle\iota_{0}\iota^{\circ}_{1},\iota_{0}\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$
(5) $\displaystyle=~{}\llangle 0,0\rrangle[1_{B},1_{B},\pi_{0}]$ Lemma
3.6.(iii) $\displaystyle=~{}0$ Lemma 3.13.(vi)
$\displaystyle\iota_{1}\llangle\iota^{\circ}_{1},\iota^{\circ}_{2}\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$
$\displaystyle=~{}\llangle\iota_{1}\iota^{\circ}_{1},\iota_{1}\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$
(5) $\displaystyle=~{}\llangle 1_{B},0\rrangle[1_{B},1_{B},\pi_{0}]$ Lemma
3.6.(iii) $\displaystyle=~{}\iota_{1}[1_{B},1_{B},\pi_{0}]$ Lemma 3.13.(iv)
$\displaystyle=~{}1_{B}$ Def. of $[-,-,-]$
$\displaystyle\iota_{2}\llangle\iota^{\circ}_{1},\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$
$\displaystyle=~{}\llangle\iota_{2}\iota^{\circ}_{1},\iota_{2}\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$
(5) $\displaystyle=~{}\llangle 0,\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]$ Lemma
3.6.(iii) $\displaystyle=~{}\pi_{1}\iota_{1}[1_{B},1_{B},\pi_{0}]$ Lemma
3.13.(iv) $\displaystyle=~{}\pi_{1}$ Def. of $[-,-,-]$

So by the couniversal property of the coproduct,
$\llangle\iota^{\circ}_{1},p_{1}\rrangle[1_{B},1_{B},\pi_{0}]=[0,1_{B},\pi_{1}]$.
In other words:

$\displaystyle\llangle\iota^{\circ}_{1},\iota^{\circ}_{2}\pi_{1}\rrangle[1_{B},1_{B},\pi_{0}]=p_{1}$
(29)

Using this identity, we then compute:

$\displaystyle g\backslash f\vee f$ $\displaystyle=~{}\llangle g\backslash
f,f\rrangle[1_{B},1_{B},\pi_{0}]$ Def. of $g\backslash f\vee f$
$\displaystyle=~{}\left\llangle\llangle
f,g\rrangle\iota^{\circ}_{1},\overline{f}g\right\rrangle[1_{B},1_{B},\pi_{0}]$
Def. of $g\backslash f$ and $f\leq g$ $\displaystyle=~{}\left\llangle\llangle
f,g\rrangle\iota^{\circ}_{1},\llangle f,\overline{f}g\rrangle
p_{1}\right\rrangle[1_{B},1_{B},\pi_{0}]$ (4)
$\displaystyle=~{}\left\llangle\llangle f,g\rrangle\iota^{\circ}_{1},\llangle
f,g\rrangle\overline{p_{0}}p_{1}\right\rrangle[1_{B},1_{B},\pi_{0}]$ Lemma
3.1.(ii) $\displaystyle=~{}\llangle
f,g\rrangle\left\llangle\iota^{\circ}_{1},\overline{p_{0}}p_{1}\right\rrangle[1_{B},1_{B},\pi_{0}]$
(5) $\displaystyle=~{}\llangle
f,g\rrangle\left\llangle\iota^{\circ}_{1},\iota^{\circ}_{2}\pi_{1}\right\rrangle[1_{B},1_{B},\pi_{0}]$
Lemma 3.13.(ii) $\displaystyle=~{}\llangle f,g\rrangle p_{1}$ (29)
$\displaystyle=~{}g$ (4)

So we have that $g\backslash f$ is the relative complement of $f$ with respect
to $g$. Thus we conclude that $\mathbb{X}$ is a classical restriction
category. $\Box$

So we conclude this section by stating the main result of this paper:

###### Theorem 6.8

A distributive restriction category is classical if and only if it has
classical products.

Recall that while a distributive restriction category always has $A\&B$ as a
tensor product, it may not be a classical product. An extreme example, already
alluded to in the introduction and discussed further below, is an ordinary
distributive category viewed as a trivial restriction category (i.e. with
$\overline{f}=1_{A}$ for all $f$). This is not a classical restriction
category unless it is essentially the final category.

A more subtle example of a distributive restriction category in which the
tensor $A\&B$ is not a classical product is the category of topological spaces
and partial continuous maps defined on open sets, $\mathsf{TOP}_{\bullet}$.
This is a distributive restriction category with joins, however, it is not
classical. Indeed, in $\mathsf{TOP}_{\bullet}$, the restriction idempotents of
a topological space $X$ correspond to its open subsets $U\subseteq X$. As
such, the composition of restriction idempotents corresponds to the
intersection of opens, while the join will correspond to the union. So if
$\mathsf{TOP}_{\bullet}$ was classical, then for each open subset $U\subseteq
X$, there would exist another open subset $U^{c}\subseteq X$ such that $U\perp
U^{c}$, which means that $U\cap U^{c}=\emptyset$, and $U\cup U^{c}=X$.
Clearly, this means that $U^{c}$ must be the set-theoretic complement of $U$.
However, the complement of an open subset is not necessarily open. Therefore,
not every restriction idempotent in $\mathsf{TOP}_{\bullet}$ has a complement,
and so $\mathsf{TOP}_{\bullet}$ is not classical. Thus, $\&$ is not a product
in $\mathsf{TOP}_{\bullet}$.

It is worth mentioning that if we instead consider
$\mathsf{TOP}^{clopen}_{\bullet}$, the subcategory of partial continuous
functions defined on _clopen_ sets, then $\mathsf{TOP}^{clopen}_{\bullet}$ is
a classical distributive restriction category, and so $\&$ is a product in
$\mathsf{TOP}^{clopen}_{\bullet}$. This leads to another interesting example
$\mathsf{STONE}^{clopen}_{\bullet}$, the category of Stone spaces (which
recall are totally disconnected compact Hausdorff topological spaces) and
partial continuous functions defined on clopen sets. Then
$\mathsf{STONE}^{clopen}_{\bullet}$ is also a classical distributive
restriction category and, thanks to Stone duality, we also have that the
opposite category of Boolean algebras and maps which preserves meets, joins,
and the bottom element (but not necessarily the top element) is also a
classical distributive restriction category.

##  7 Classical Classification

In this section, we show that classical distributive restriction categories
are in fact precisely the Kleisli categories of the exception monads of
distributive categories. For a more in-depth introduction to distributive
categories, we invite the reader to see [1, 2].

By distributive category [2, Sec 3], we mean a category $\mathbb{D}$ with
finite products and finite coproducts which distribute in the same sense as in
Def 2.5. From the point of view of restriction categories, a distributive
category is a distributive restriction category $\mathbb{D}$ with a trivial
restriction, so $\overline{f}=1_{A}$ and every map is total. As such, for a
distributive category $\mathbb{D}$, we will use $\times$ for the product and
$\mathsf{1}$ for the terminal object. As noted above, a distributive category
(seen as a trivial restriction category) does not have classical products
unless the category is trivial. The subcategory of total maps of a
distributive restriction category, on the other hand, is always a distributive
category:

###### Lemma 7.1

[7, Prop 5.7] For a distributive restriction category $\mathbb{X}$,
$\mathcal{T}[\mathbb{X}]$ is a distributive category.

For a distributive category $\mathbb{D}$, its exception monad (also sometimes
called the maybe monad) is the monad $\\_\oplus\mathsf{1}$, where the unit is
the injection $\iota_{0}:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\mathsf{1}$ and the
multiplication is
$[\iota_{0},\iota_{1},\iota_{1}]:A\oplus\mathsf{1}\oplus\mathsf{1}\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\mathsf{1}$. It is well
established that the Kleisli category of the exception monad
$\mathbb{D}_{\\_\oplus\mathsf{1}}$ is a restriction category, in fact, it is a
distributive restriction category with restriction zeroes. To help us
distinguish between maps in the base category and maps in the Kleisli
category, we will use interpretation brackets, which are functions on homsets
$\llbracket-\rrbracket:\mathbb{D}_{\\_\oplus\mathsf{1}}(A,B)\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}\mathbb{D}(A,B\oplus\mathsf{1})$. So a
Kleisli map from $A$ to $B$ will be written as $\llbracket
f\rrbracket:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$. To demonstrate how
these interpretation brackets are useful, here is how to express identity maps
and composition in the Kleisli category:

$\displaystyle\llbracket 1_{A}\rrbracket=\iota_{0}$ $\displaystyle\llbracket
fg\rrbracket=\llbracket f\rrbracket\left[\llbracket
g\rrbracket,1_{\mathsf{1}}\right]$ (30)

Let us now describe how the Kleisli category of the exception monad is a
distributive restriction category with restriction zeroes.

###### Proposition 7.2

[7, Ex 5.4] Let $\mathbb{D}$ be a distributive category. Then
$\mathbb{D}_{\\_\oplus\mathsf{1}}$ is a distributive restriction category with
restriction zeroes where:

  1. (i)

For a Kleisli map $\llbracket f\rrbracket:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$, its restriction
$\left\llbracket~{}\overline{f}~{}\right\rrbracket:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\mathsf{1}$ is defined as the
following composite:

$\begin{gathered}\begin{array}[c]{c}\left\llbracket~{}\overline{f}~{}\right\rrbracket\end{array}:=\begin{array}[c]{c}\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.375pt\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{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.07985pt\raise 8.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\left\langle
1_{A},\llbracket f\rrbracket\right\rangle}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 54.375pt\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}}{\hbox{\kern
54.375pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{A\times(B\oplus\mathsf{1})\cong(A\times
B)\oplus(A\times\mathsf{1})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
201.09026pt\raise 5.41751pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.2575pt\hbox{$\scriptstyle{\pi_{0}\oplus\pi_{1}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 235.93143pt\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}}{\hbox{\kern
235.93143pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{A\oplus\mathsf{1}}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{array}\end{gathered}$
(31)

  2. (ii)

A Kleisli map $\llbracket f\rrbracket:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$ is total if and only
if $\llbracket f\rrbracket=g\iota_{0}$ for some (necessarily unique) map
$g:A\allowbreak\mathrel{\mathop{\hbox to10.79999pt{\rightarrowfill}}\limits}B$
in $\mathbb{D}$. Therefore, we have an isomorphism
$\mathcal{T}[\mathbb{D}_{\\_\oplus\mathsf{1}}]\cong\mathbb{D}$.

  3. (iii)

The restriction terminal object is the terminal object $\mathsf{1}$, and
$\llbracket t_{A}\rrbracket:A\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}\mathsf{1}\oplus\mathsf{1}$ is defined
as the composite $\llbracket t_{A}\rrbracket=t_{A}\iota_{0}$.

  4. (iv)

The restriction product is the product $A\times B$ where the projections
$\llbracket\pi_{0}\rrbracket:A\times B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\mathsf{1}$ and
$\llbracket\pi_{1}\rrbracket:A\times B\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$ are defined as the
composites $\llbracket\pi_{j}\rrbracket=\pi_{j}\iota_{0}$, and where the
pairing of Kleisli maps $\llbracket
f\rrbracket:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}A\oplus\mathsf{1}$ and $\llbracket
g\rrbracket:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}B\oplus\mathsf{1}$ is the Kleisli map
$\llbracket\langle f,g\rangle\rrbracket:C\allowbreak\mathrel{\mathop{\hbox
to10.79999pt{\rightarrowfill}}\limits}(A\times B)\oplus\mathsf{1}$ defined as
follows:

$\begin{gathered}\begin{array}[c]{c}\llbracket\langle
f,g\rangle\rrbracket\end{array}:=\begin{array}[c]{c}\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.53812pt\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{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
15.82751pt\raise 8.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.5pt\hbox{$\scriptstyle{\left\langle\llbracket
f\rrbracket,\llbracket g\rrbracket\right\rangle}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 66.53812pt\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}}{\hbox{\kern
66.53812pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise