In many engineering applications it is useful to reason about “negative information”.
For example, in planning problems, providing an optimal solution is the same as giving a feasible solution (the “positive” information) together with a proof of the fact that there cannot be feasible solutions better than the one given (the “negative” information).
We model negative information by introducing the concept of “norphisms”, as opposed to the positive information of morphisms.
A “nategory” is a category that has “nom”-sets in addition to hom-sets, and specifies the interaction between norphisms and morphisms.

In particular, we have composition rules of the form $\text{morphism} + \text{norphism} \to \text{norphism}$.
Norphisms do not compose by themselves; rather, they use morphisms as catalysts.
After providing several applied examples, we connect nategories to enriched categtory theory.
Specifically, we prove that categories enriched in de Paiva's dialectica categories $\GC$, in the case $\CatC = \Set$ and equipped with a modified monoidal product, define nategories which satisfy additional regularity properties.
This formalizes negative information categorically in a way that makes negative and positive morphisms equal citizens.

§ INTRODUCTION

§.§ Manipulation of negative information is important in applications of category theory

Our research group's background is in robotics and systems theory.
In these fields, we have found that category theory can describe well many of the structures in our problems, but something is often missing: we find ourselves in the position of reasoning and writing algorithms that manipulate “negative information”, but we do not know what is an appropriate categorical concept for it.
We give some examples.

Robot motion planning can be formalized as the problem of finding a trajectory through an environment, respecting some constraint (e.g., avoiding obstacles).
One can think of the robot configuration manifold $\manifold$ as a category where the objects are elements of the tangent bundle and the morphisms are the feasible paths according to the problem constraints.
The output of planning problems has an intuitive representation in category theory, if the problem is feasible.
A path planning algorithm is given two objects and must compute a morphism as a solution.
A motion planning algorithm would compute a trajectory, which could be seen as a functor $F$ from the manifold $[0,T]$ to $M$ with $F(0)=A$ and $F(T)=B$.
However, if the problem is infeasible–if no morphisms between two points can be found—if the algorithm must present a certificate of infeasibility–what is the equivalent concept in category theory?

In many cases, the problems are not binary (either a solution exists or not, either a proposition is true or not) but we care about the performance of solutions.
For example, consider the case of the weighted shortest path problem in dynamic programming.
The problem is to find a path through a graph that minimizes the sum of the weights of the edges on the path.
In robotics, this can be used for planning problems, where the weights could represent the time, the distance, or the energy required by a robot to traverse an edge, and the nodes are either regions of space or, more generally, joint states of the world and environment.
Proving that a path is optimal means producing the path together with a proof that there are no shorter paths.
This is called a “certificate of optimality” and, like certificates of infeasibility, is negative information as it consists in negating the existence of a certain class of paths.
Interestingly, one can see algorithms such as Dijkstra's algorithm as constructing both positive and negative information at the same time, such that when a path is finally found, we are sure that there are no shorter ones [5].

In some cases, the negative information is a first-class citizen which is critical to the efficiency.
Algorithms such as A* require the definition of heuristic functions, which is negative information: they provide a lower bound on the cost of a path between two points.
And better heuristics make the algorithm faster.
Again, we ask, what could be the categorical counterpart of heuristics?

In co-design [6, 2], a morphism $\funsp \mto \ressp$ describes what functionality can be achieved with which resources.
They are characterized as boolean profunctors, that is, monotone functions $\funsp\op \cartprod \ressp \to \Bool$.
The negative information would be a “nesign” problem that characterizes an impossibility.
For example, if $\funsp=\ressp=\text{Energy}$, we expect that in this universe we cannot find a realizable morphism $\adp$ that satisfies $\adp(2 J, 1 J)$ (obtaining 2 Joules from 1 Joule).

Can this be expressed as some sort of morphism? In which category does it live?

§.§ Our approach: “Categorification” of negative information

We briefly describe our thought process in finding a formalization for dealing with negative information.

One approach could have been to build structure on top of a category, at a higher level, using logic.
We eschew this approach because of the belief that we should find a duality between positive and negative information that puts them “at the same level”.

Our approach has been one in the spirit of “categorification”: representing the negative information with a concrete structure for which to find axioms and inference rules.

An early influence in our thinking was the paper of Shulman about “proofs and refutations” [8].
What follows is a simplified explanation of one of the concepts of the paper.
Consider a category where objects are propositions and morphisms $\Obja \to \Objb$ are propositions $\Obja\Rightarrow \Objb$
(with the particular case of $\Obja \simeq (\top \to \Obja$)).
We can then consider the type $\proofs(\Obja\to \Objb)$ of proofs and the type $\refutations(\Obja\to \Objb)$ of refutations, which correspond to positive and negative information.
According to intuitionist logic, $\proofs(\Obja\to \Objb) = (\proofs(\Obja)\to \proofs(\Objb)) \times (\refutations(\Objb)\to \refutations(\Obja))$: a proof of $\Obja\Rightarrow \Objb$ is a way to convert a proof of $\Obja$ into a proof of $\Objb$ together with a way to convert a refutation of $\Objb$ into a refutation of $\Obja$.

In that paper, proofs and refutations, positive and negative information, are treated at the same level but not symmetrically—proof and refutations have different semantics, and $\proofs$ and $\refutations$ map products and coproducts ($\vee$, $\wedge$) to different linear logic operators.

This led to the idea that negative information should be at the same level of positive information: if positive information is represented by morphisms, then also the negative information should be described as “negative arrows” between objects, which we called norphisms (for negative morphisms).

We also realized that the positive/negative information duality we are looking for is richer than the structure of proofs/refutations in logic.
In (classical/intuitionistic) logic, one expects the existence of either a proof of a proposition $A$, a refutation of $A$, or neither, but not both.
Instead, in our formalization, norphisms are a more general notion, which can coexist with morphisms and give complementary information, as in the planning examples in the introduction.

An initial idea was to consider for each category a “twin” category, whose morphisms would be the norphisms we were looking for to represent the negative information; however, this idea failed.
In the course of the paper, it will be clear that positive/negative information cannot be decoupled, because negative information cannot be composed independently of positive information. In the end, we unite them by viewing them as part of a single enrichement structure.

§.§ Plan of the paper

This paper follows an inductive exposition and is divided in two parts.

In the first part we provide the motivation and several examples of representing negative information with “norphism” structure.

In Section <ref> we consider the case of a thin category.
In this simple setting we can already see that norphisms compose differently than morphisms, and that we need two composition rules for them.

In Section <ref> we state our main definition, that of a “nategory”, and in Section <ref> we show some canonical ways to build a nategory out of a category.

In Sections <ref> and <ref> we discuss two examples, and , which have norphism structures in which norphisms and morphisms are not mutually exclusive.

In the second part our goal is to provide an elegant way to think of norphisms and their composition by using enriched category theory.
By doing so, we show that the additional structure of norphisms and their composition, rules which might initially appear “funky”, is not an arbitrary structure, but rather it is as “natural” as the positive information of morphisms. In Section <ref> we introduce the dialectica category $\GSet$ [3, 1] and define a monoidal product for it which is slightly different than the ones usually used as linear logic connectives. Then, in  Section <ref>, we prove that $\GSet$-enriched categories encode nategories which satisfy some additional compatibilities between morphisms and norphisms. These additional compatibilities are not satisfied in certain examples of interest to us, therefore we have refrained from including them directly in our definition of nategory.

§ BUILDING INTUITION: THE CASE OF THIN CATEGORIES

To build an intuition about norphisms, we look at the case of “thin” categories, in which each hom-set contains at most one morphism.

Thin categories are essentially pre-orders.
To aid the interpretation, one can think of a pre-order as defining a reachability relation, in which a morphism $\Obja \mto \Objb$ represents “I can reach $\Objb$ from $\Obja$”.
Or, we can think of morphisms as (proof-irrelevant) implications: $\Obja \mto \Objb$ represents “I can prove $\Objb$ from $\Obja$”.
In a thin category, negative information is limited to indicate the refutation of positive information.
Therefore, a norphism $\nora \colon \Obja \norto \Objb$ is equivalent to “There are no morphisms from $\Obja$ to $\Objb$”.
Particularly, this means “I cannot reach $\Objb$ from $\Obja$” or “I cannot prove $\Objb$ from $\Obja$”.

We will later see that, in general, norphisms need not necessarily be mutually exclusive with morphisms. Still, this example is sufficient to get us started in appreciating how morphisms and norphisms compose differently.
The composition rule for morphisms reads:

\begin{equation}
\label{eq:composition-mor}
\prfperiod{\mora\colon \Obja \mto \Objb}{\morb\colon \Objb \mto \Objc}
{(\mora \mthen \morb)\colon \Obja \mto \Objc}
\end{equation}

Mimicking this, one could start with two norphisms $\nora\colon \Obja \norto \Objb$ and $\norb\colon \Objb \norto \Objc$ and expect to be able to say something about a norphism $\Obja \norto \Objc$, with a composition rule of the form:

\begin{equation}\label{eq:composition-nor-2}
\prfperiod{\nora\colon \Obja \norto \Objb}{\norb\colon \Objb \norto \Objc}
{\textcolor{norcolor}{???} \colon \Obja \norto \Objc}
\end{equation}

However, norphisms do not compose this way.
In fact, one can derive the following rule:

\begin{equation}
\label{eq:nor-composition}
\prfperiod{\norc \colon \Obja \norto \Objc}{\quad}{\Objb \colon \Ob_\CatC}{(\nora\colon \Obja \norto \Objb) \boolor (\norb\colon \Objb \norto \Objc)}
\end{equation}

This rule is “the dual” of (<ref>) in the same sense as these two axioms are dual:

\begin{equation}\label{eq:nor-duality}
\prfcomma{\true}{\Obja \mto \Obja} \qquad \prfcomma{\Obja \norto \Obja}{\false}
\end{equation}

that is, in the sense of flipping vertically and negating the propositions.

We read (<ref>) as saying that if there is no morphism $\Obja \mto \Objc$, it is because, for every possible intermediate $\Objb$, there cannot be a morphism $\Obja \mto \Objb$ or $\Objb\mto \Objc$.
Note that composition goes in the “opposite” direction meaning that from one norphism, we get some information about the existence of one or two in a pair.

The composition (<ref>) is not constructive: from the “$\boolor$”, we do not know which side we can create.
Indeed, this composition highlights the asymmetry between morphisms and norphisms:

morphisms compose constructively by themselves (i.e., without taking into account norphisms);

norphisms, instead, do not “compose”, but rather “decompose” by themselves.

To construct norphisms, we need to start from a norphism and a morphism that acts as a “catalyst”.

When interpreting a thin category as a graph, if there is a norphism $\nora \colon \Obja \norto \Objb$, it means that for any $\Objb$, the path $\Obja \mto \Objb \mto \Objc$ must be interrupted in one part or the other, because otherwise we would have a contradiction.

Indeed, if we know that morphisms $\mora\colon \Obja \mto \Objb$ and $\morb\colon \Objb \mto \Objc$ exist, then their composition $\mora\mthen \morb\colon \Obja \mto \Objc$ must exist, and therefore no norphism $\nora\colon \Obja \norto \Objc$ can exist.

This observation can be turned around in a constructive way.
Starting from a morphism $\mora\colon \Obja \mto \Objb$ and a norphism $\nora\colon \Obja \norto \Objc$ (i.e., morphisms and norphisms with the same source), we can infer a norphism $\northenb{\mora}{\nora}\colon \Objb\norto \Objc$ (i.e., there cannot be a morphism $\Objb\mto \Objc$):
[inline]Check norphism symbol, as in the pic it has to be done differently.

\begin{equation}
\label{eq:rule-same-source}
\begin{tabular}{cc}
\includesag{nor-compose-const-a}\qquad \qquad &
\begin{tikzpicture}
\node at (0,2){\prfperiod{\Objb \overset{\mora}{\stylemorph{\leftarrow}} \Obja \overset{\nora}{\norto}\Objc}{\Objb \overset{\northenb{\mora}{\nora}}{\norto} \Objc}
\end{tikzpicture}
\end{tabular}
\end{equation}

Symmetrically, starting from a morphism $\morb\colon \Objb \mto \Objc$ and a norphism $\nora\colon \Obja \norto \Objc$ (i.e., morphisms and norphisms with the same target), we can infer a norphism $\northena{\nora}{\mora} \colon \Obja\norto \Objb$:
[inline]check symbol in pic if changing macro

\begin{equation}
\label{eq:rule-same-target}
\begin{tabular}{cc}
\includesag{nor-compose-const-b}\qquad \qquad &
\begin{tikzpicture}
\node at(0,2){\prfperiod{\Obja \overset{\nora}{\norto} \Objc \overset{\morb}{\stylemorph{\leftarrow}}\Objb}{\Obja \overset{\northena{\nora}{\morb}}{\norto} \Objb}};
\end{tikzpicture}
\end{tabular}
\end{equation}

\begin{equation}\label{eq:norcomp1}
\prf{
\Objb \overset{\mora}{\stylemorph{\leftarrow}} \Obja \overset{\nora}{\norto}\Objc
\Objb \overset{\mora \,\northenbsymb\, \nora}{\norto} \Objc
\end{equation}

\begin{equation}\label{eq:norcomp2}
\prf{
\Obja \overset{\nora}{\norto} \Objc \overset{\morb}{\stylemorph{\leftarrow}}\Objb
\Obja \overset{\nora \,\northenasymb\, \morb}{\norto} \Objb
\end{equation}

Note that the new norphism is pointing in the “same direction” as the starting one, meaning that either source or target are preserved.

§ DESCRIBING NEGATIVE INFORMATION: NATEGORIES

In this section we make the notion of norphisms more precise, by defining the additional structure which a category must have in order to encode negative information.

A locally small nategory is a locally small category with the following additional structure.
For each pair of objects $\Obja,\Objb \setin \Ob_{\CatC}$, in addition to the set of morphisms $\HomSet{\CatC}{\Obja}{\Objb}$, we also specify:

* A set of norphisms $\NomSet{\CatC}{\Obja}{\Objb}$.

* An incompatibility relation, which we write as a binary function

\begin{equation} \label{eq:010-nategory-incompat}
\nmincompat{\Obja}{\Objb}\colon\NomSet{\CatC}{\Obja}{\Objb} \cartprod \HomSet{\CatC}{\Obja}{\Objb}   \to \makeset{\false, \true}.
\end{equation}

For all triples $\Obja,\Objb,\Objc$, in addition
to the morphism composition function

\begin{equation} \label{eq:011-nategory-comp}
\mthen_{\Obja\Objb\Objc} \colon \HomSet{\CatC}{\Obja}{\Objb} \cartprod \HomSet{\CatC}{\Objb}{\Objc} \to \HomSet{\CatC}{\Obja}{\Objc},
\end{equation}

we require the existence of two norphism composition functions

\begin{equation}\label{eq:012-nategory-norcomp}
\begin{aligned}
\northenbsymb_{\Obja\Objb\Objc} & \colon \HomSet{\CatC}{\Obja}{\Objb} \cartprod \NomSet{\CatC}{\Obja}{\Objc} \to \NomSet{\CatC}{\Objb}{\Objc},
\\
\northenasymb_{\Obja\Objb\Objc} & \colon \NomSet{\CatC}{\Obja}{\Objc} \cartprod \HomSet{\CatC}{\Objb}{\Objc} \to \NomSet{\CatC}{\Obja}{\Objb},
\end{aligned}
\end{equation}

and we ask that they satisfy two “equivariance” conditions:

\begin{align}
\nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb)
& \Rightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab )\label{eq:cond1}\tag{equiv-1}, \\
\nmincompat{\Obja}{\Objb} (\northena{\nora}{\morb}, \mora)
& \Rightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab )\tag{equiv-2}\label{eq:cond2}.
\end{align}

We write $\nora : \Obja \norto \Objb$ to say that $\nora \in \NomSet{\CatC}{\Obja}{\Objb}$.

If the two conditions (<ref>) and (<ref>) are satisfied with “$\Leftrightarrow$” instead of just “$\Rightarrow$”, we say that the nategory is exact.

Condition (<ref>) says that the norphism $\northenb{\mora}{\nora}$ can exclude the morphism $\morb$ only if $\morab$ is excluded by $\nora$.
The idea is that such a $\morb$ should not be excluded for any “additional reasons”, but only on the grounds that $\morab$ is excluded by $\nora$.

Starting situation.

Find incompatibility with $\nora$.

Pulling back incompatible morphisms.

\subseteq
\precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objc}(\nora))$.

We draw some figures to develop further intuition (Fig. <ref>).
Let $\nomtohom{\Obja}{\Objb}$ denote the function which maps a norphism to the set of morphisms with which it is incompatible:

\begin{equation}
\label{eq:nom-to-hom}
\defmapperiod{
\nomtohom{\Obja}{\Objb}
\NomSet{\CatC}{\Obja}{\Objb}
\to
\powerset(\HomSet{\CatC}{\Obja}{\Objb})
\nora
\makeset{
\mora \setin \HomSet{\CatC}{\Obja}{\Objb}\colon \nmincompat{\Obja}{\Objb}(\nora, \mora)
\end{equation}

We start in Fig. <ref> with a norphism $\nora: \Obja \norto \Objc$ and
a morphism $\mora: \Obja \mto \Objb$.
In Fig. <ref> we apply $\nomtohom{\Obja}{\Objc}$ to find the set of incompatible morphisms $\nomtohom{\Obja}{\Objc}(\nora)$.
In Fig. <ref> we use the precomposition map

\begin{equation}\label{eq:020-precomp-map}
\defmapcomma{
\precomp{\mora}
\HomSet{\CatC}{\Objb}{\Objc}
\to
\HomSet{\CatC}{\Obja}{\Objc}
\morb
\mora \mthen \morb
\end{equation}

to obtain the set of morphisms

\begin{equation}
\precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objc}(\nora)).
\end{equation}

These are to be prohibited because when pre-composed with $\mora$
they give a morphism that is forbidden by $\nora$.
Now, in principle, it could be that our norphism inference is so powerful that
$\northenb{\mora}{\nora}$ manages to exclude all of these:

\begin{equation}
\nomtohom{\Objb}{\Objc}(\northenb{\mora}{\nora}) = \precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objc}(\nora)).
\end{equation}

In general, we are happy with the composition operation if it excludes part of those (but not more):

\begin{equation}\label{eq:inclusion-condition1}
\nomtohom{\Objb}{\Objc}(\northenb{\mora}{\nora})
\subseteq
\precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objc}(\nora)).
\end{equation}

It can readily be checked that (<ref>) is equivalent to (<ref>).
Similarly, (<ref>) is equivalent to requiring

\begin{equation}\label{eq:inclusion-condition2}
\nomtohom{\Objb}{\Objc}(\northena{\nora}{\morb})
\subseteq
\postcomp{\morb}^{-1}(\nomtohom{\Obja}{\Objc}(\nora)),
\end{equation}

where $\postcomp{\morb}$ is the map “post-composition with $\morb$”.

It is an inclusion of two sets $S_1 \subseteq S_2$.
Call the generic element of the two sets $\morb$.
Then inclusion means that the indicator function of the first implies the indicator function of the second: $S_1(\morb) \Rightarrow S_2(\morb)$.
The indicator function of the first set is:

\begin{equation}
S_1(\morb) = \morb \in \nomtohom{\Objb}{\Objc}(\northenb{\mora}{\nora})
= \nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb).
\end{equation}

For the second set it is:

\begin{equation}
S_2(\morb) = \morb \in \precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objc}(\nora))
= \nmincompat{\Obja}{\Objc} ( \nora, \morab ).
\end{equation}

\begin{align}\label{eq:cond12bis}
\nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb)
& \Rightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab ), \\
\nmincompat{\Obja}{\Objb} (\nora \northenasymb \morb, \mora)
& \Rightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab ).
\end{align}

\begin{align}\label{eq:cond12ter}
\nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb)
& \Leftrightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab ), \\
\nmincompat{\Obja}{\Objb} (\nora \northenasymb \morb, \mora)
& \Leftrightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab ).
\end{align}

§ CANONICAL NATEGORY CONSTRUCTIONS

Here are three canonical constructions that allow us to get a nategory out of a category in a more or less straightforward way:

* Setting the norphism sets to be empty (Example <ref>);

* Setting the norphism sets to be singletons that negate the entire respective hom-sets (Example <ref>);

* Setting the norphism sets to be the powerset of the respective hom-sets (Example <ref>).

[A nategory with no norphisms]

For any category , let

\begin{equation}\label{eq:010-nonorph}
\NomSet{\CatC}{\Obja}{\Objb}\definedas\emptyset.
\end{equation}

For all pairs $\Obja,\Objb$ the
function $\nmincompat{\Obja}{\Objb}$ is uniquely defined as it has an empty domain.
The functions $\northenbsymb, \northenasymb$ also have empty domains.
The conditions (<ref>) and (<ref>) are trivially verified.
A nategory with no norphisms is just a category.

[Singleton norphism sets negating all morphisms]

In this construction, we turn a category into a nategory by making the choice that a norphism is a witness for the fact that the corresponding hom-set is empty.
For any category , let

\begin{equation}\label{eq:020-one}
\NomSet{\CatC}{\Obja}{\Objb}\definedas\makeset{\theonlynor},
\end{equation}

for any pair $\Obja,\Objb$ and any $\mora\colon\Obja\mto\Objb$ let

\begin{equation}\label{eq:021-one-true}
\nmincompat{\Obja}{\Objb} ( \theonlynor, \mora) = \true.
\end{equation}

In this case, the element $\theonlynor$ is a witness for “$\HomSet{\CatC}{\Obja}{\Objb}$ is empty”.

Next, we need to define the two maps:

\begin{align}
\northenbsymb & \colon \HomSet{\CatC}{\Obja}{\Objb} \cartprod \NomSet{\CatC}{\Obja}{\Objc} \to \NomSet{\CatC}{\Objb}{\Objc},
\\
\northenasymb & \colon \NomSet{\CatC}{\Obja}{\Objc} \cartprod \HomSet{\CatC}{\Objb}{\Objc} \to \NomSet{\CatC}{\Obja}{\Objb}.
\end{align}

The choice is forced, as there is only one norphism in the codomains.
We obtain:

\begin{align}\label{eq:022-one-compose}
\northenb{\mora}{\theonlynor} & = \theonlynor, \\
\northena{\theonlynor}{\morb} & = \theonlynor.
\end{align}

The conditions (<ref>) and (<ref>) are easily verified because $\nmincompat{\Obja}{\Objb}$ always evaluates to $\true$.

[Norphism sets are subsets of hom-sets]

For any category , let

\begin{equation}\label{eq:030-powerset}
\NomSet{\CatC}{\Obja}{\Objb}=\powerset(\HomSet{\CatC}{\Obja}{\Objb}).
\end{equation}

Set the incompatibility relation as

\begin{equation}\label{eq:030-powerset-incomp}
\nmincompat{\Obja}{\Objb}(\nora, \mora) = \mora \in \nora.
\end{equation}

Define the composition operations as

\begin{align}\label{eq:030-powerset-compose}
\northenb{\mora}{\nora} & = \precomp{\mora}^{-1}(\nora), \\
\northena{\nora}{\morb} & = \postcomp{\morb}^{-1}(\nora),
\end{align}

where $\precomp{\mora}$ and $\postcomp{\morb}$ are the pre- and post-composition maps

\begin{equation}\label{eq:030-powerset-precomp}
\defmapcomma{
\precomp{\mora}
\HomSet{\CatC}{\Objb}{\Objc}
\to
\HomSet{\CatC}{\Obja}{\Objc}
\morb
\mora \mthen \morb
\end{equation}

\begin{equation}\label{eq:030-powerset-postcomp}
\defmapperiod{
\postcomp{\morb}
\HomSet{\CatC}{\Obja}{\Objb}
\to
\HomSet{\CatC}{\Obja}{\Objc}
\mora
\mora \mthen \morb
\end{equation}

Let's check the condition (<ref>): $  \nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb)
\Rightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab )$.
Using our definitions, we get

\begin{equation}
\morb \in \northenb{\mora}{\nora}
\quad
\Rightarrow
\quad
\morab \in \nora.
\end{equation}

Expanding the left-hand side we find

\begin{align}
\morb \in \precomp{\mora}^{-1}(\nora)
& \quad
\Rightarrow
\quad
\morab \in \nora.
\end{align}

Another expansion shows that both sides are the same:

\begin{align}
\morab \in \nora
& \quad
\Rightarrow
\quad
\morab \in \nora .
\end{align}

Checking condition (<ref>) is analogous.
Note that this nategory is exact.

Finally, we provide an example of a nategory that we will use later as a counter-example.

[Very weak composition operations]

For any category , as in the previous example, use subsets of morphisms as the norphisms

\begin{equation}
\NomSet{\CatC}{\Obja}{\Objb}=\powerset(\HomSet{\CatC}{\Obja}{\Objb}),
\end{equation}

and set the incompatibility relation as

\begin{equation}
\nmincompat{\Obja}{\Objb}(\nora, \mora) = \mora \in \nora.
\end{equation}

However, define the composition operations as

\begin{align}\label{eq:composition-weak}
\northenb{\mora}{\nora} & = \emptyset, \\
\northena{\nora}{\morb} & = \emptyset.
\end{align}

The equivariance conditions are still satisfied.
For example condition (<ref>),

\begin{equation}
\nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb)
\Rightarrow
\nmincompat{\Obja}{\Objc} ( \nora, \morab ),
\end{equation}

\begin{equation}
\morb \in \emptyset
\ \Rightarrow \
\morab \in \emptyset,
\end{equation}

which is vacuously satisfied, because the premise is always false.

§ EXAMPLE: HIKING ON THE SWISS MOUNTAINS

In this section we present an example of planning, giving a more concrete description of the path planning problems mentioned in the introduction.
We describe $\Berg$, a category whose morphisms are hiking paths of various difficulty on a mountain.
We then consider the problem of finding paths of minimum length.

Let $\mapelevation \colon \reals^2\to \reals$ be a $C^1$ function, describing the elevation of a mountain.
The set with elements $\tup{\setAel, \setBel, \mapelevation(\setAel,\setBel)}$ is a manifold $\manifold$ that is embedded in $\reals^3$.
Let $\steepness=\interv{\steepnessL}{\steepnessU}\setsubset \reals$ be a closed interval of real numbers.
The category $\Berg_{\mapelevation,\steepness}$ is specified as follows:

* An object $\Obja$ is a pair $\tup{\pos,\vel}\setin \tangbundle \manifold$, where $\pos = \tupp{\pos_x,\pos_y,\pos_z}$ is the position, $\vel$ is the velocity, and $\tangbundle\manifold$ is the tangent bundle of the manifold.

* Morphisms are $C^1$ paths $\mora \colon [0, \tau] \to \manifold$ on the manifold satisfying evident boundary conditions (here $\tau \in \reals$ may vary). We also define, formally by decree, that for each $\tup{\pos,\vel}$ there is a trivial path “$[0,0] \to \manifold$” which is $C^1$, has trace $\pos$, and velocity $\vel$.

At each point $\pos = \mora(t)$ of a path we define the steepness via the formula

\begin{equation}\label{eq:Berg-steepness}
\steepfun(\tup{\pos,\vel}) \definedas \vel_z/\sqrt{\vel_x^2+\vel_y^2},
\end{equation}

where $\vel = \tfrac{d}{dt}\mora(t)$.
We choose as morphisms only the paths that have the steepness values contained in the interval $\steepness$:

\begin{equation}\label{eq:Berg-Hom}
\HomSet{\Berg_{\mapelevation,\steepness}}{\Obja}{\Objb}=\{\mora \text{ is a } C^1 \text{ path from }\Obja \text{ to }\Objb \text{ and } \steepfun(\mora)\setsubseteq \steepness\},
\end{equation}

* Morphism composition is given by concatenation of paths.

* Identity morphisms are given by trivial paths.

at (0,0) ;

at (2,0.1) $\manifold$;
at (-2.3,1.3)$\tangbundle\manifold$;
at (-1.6,-0.5)$\Obja$;
at (-0.3,1.6)$\Objb$;
[thick, -Triangle] (0,1.45)–node[pos=0.4,above]$\vel$ (0.7,1.6);

proceedingsFor the complete proof that $\Berg$ is a category, we refer the reader to Lemma <ref>.

The steepness interval $\steepness$ allows considering different categories on the same mountain, with possible hikes varying in difficulty, measured via minimum/maximum steepness.
For example, a good hiker can handle $\steepness=\interv{-0.57}{0.57}$ (positive/negative $30^\circ$ slope).

If $\steepness=\interv{-0.57}{0}$, we are only allowed to climb down.
If $\steepness=\interv{0}{0}$, we can only walk along isoclines.

Interpretation of norphisms in $\Berg$
What might a norphism be in this case?

One possibility is to let a norphism $\nora\colon \Obja \norto \Objb$ mean “there exists no path from $\Obja$ to $\Objb$”.
This is a simple choice that is similar to Example <ref> and that makes morphisms and norphisms mutually exclusive.

We can obtain a more useful theory by letting norphisms carry information that is complementary to morphisms
by interpreting them as lower bounds on distances.
To see how this can work, let the set of norphisms be the real numbers completed by positive infinity:

\begin{equation}\label{eq:nom-nonneg}
\NomSet{\Berg}{\Obja}{\Objb} \ \definedas \ \nonNegReals \setunion \makeset{+\infty}.
\end{equation}

Let $\lengthfun(\mora)$ be the length of the path (according to the manifold metric).
Then we interpret a norphism $\nora\colon \Obja \norto \Objb$ as a witness of “for all paths $\mora\colon \Obja \mto \Objb$, we have $\lengthfun(\mora)\geq \nora$”.

The case $\nora = \infty$ negates any path from $\Obja$ to $\Objb$.

The incompatibility relation $\nmincompat{\Obja}{\Objb}$ can be written as follows:

\begin{equation}\label{eq:nom-nonneg-incompat}
\nmincompat{\Obja}{\Objb}(\nora, \mora) = \lengthfun(\mora) < \nora.
\end{equation}

To say that a path $\mora$ is optimal means saying that $\mora$ is feasible and that $\lengthfun(\mora)$ is a norphism:

\begin{equation}\label{eq:nom-nonneg-optimal}
\prfdoubleperiod{\mora\colon \Obja \mto \Objb}{\stylenorph{\lengthfunnor(\mora)}\colon \Obja \norto \Objb}{\mora \text{\ is optimal}}
\end{equation}

Composition rules for norphisms
Next, we define the following two composition rules

\begin{equation}
\label{eq:berg-compose}
\begin{aligned}
\northenb{\mora}{\nora} & = \max\{\nora - \lengthfun(\mora), 0\}, \\
\northena{\nora}{\morb} & = \max\{\nora - \lengthfun(\morb), 0\},
\end{aligned}
\end{equation}

which are the equivalent of (<ref>) and (<ref>). See  Fig. <ref>.
Our reasoning is as follows. If for example $\mora$ is a path from $\Obja$ to $\Objb$, and we know that going from $\Obja$ to $\Objc$ has a distance of at least $\nora$, then any path from $\Objb$ to $\Objc$ must be at least $\nora - \lengthfun(\mora)$ long.

In this case,

\begin{equation}
\begin{aligned}
\nomtohom{\Obja}{\Objc}(\northenb{\mora}{\nora}) & =\{\morb\colon \lengthfun(\morb) < \max\{\nora-\lengthfun(\mora),0\}\}.
\end{aligned}
\end{equation}

If $\nora < \lengthfun(\mora)$, then $\nomtohom{\Obja}{\Objc}(\northenb{\mora}{\nora})$ is empty, which differs from

\begin{equation}
\precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objb}(\nora))=\{\morb\colon \lengthfun(\morb)+\lengthfun(\mora)< \nora\}.
\end{equation}

The nategory is not exact.
However, since

\begin{equation}
\{\morb\colon \lengthfun(\morb) < \max\{\nora-\lengthfun(\mora),0\}\}\subseteq \{\morb\colon \lengthfun(\morb)+\lengthfun(\mora)< \nora\},
\end{equation}

the nategory satisfies (<ref>).
The check for (<ref>) is analogous.

Composition of morphisms and norphisms in the case of paths and lengths.

As a variant of the above, if we set

\begin{equation}\label{eq:nom-reals}
\NomSet{\Berg}{\Obja}{\Objb} \ \definedas \ \reals \setunion \makeset{+\infty},
\end{equation}

and define the composition operations as

\begin{equation}\label{eq:nom-reals-compose}
\begin{aligned}
\northenb{\mora}{\nora} & = \nora - \lengthfun(\mora), \\
\northena{\nora}{\morb} & = \nora - \lengthfun(\morb),
\end{aligned}
\end{equation}

then the nategory is exact.
Indeed, for this case one has

\begin{equation}
\begin{aligned}
\nomtohom{\Obja}{\Objc}(\northenb{\mora}{\nora}) & =\{\morb\colon \lengthfun(\morb) < \nora-\lengthfun(\mora)\}, \\
& =\{\morb\colon \lengthfun(\morb)+\lengthfun(\mora)< \nora\} \\
& =\precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objb}(\nora)).
\end{aligned}
\end{equation}

We may also think of a variation in which the norphisms are integers:

\begin{equation}\label{eq:nom-integers}
\NomSet{\Berg}{\Obja}{\Objb} \ \definedas \ \mathbb{Z} \setunion \makeset{+\infty}.
\end{equation}

In this case we are limited to express constraints of the type

\begin{align}
\lengthfun(\mora) \geq 0, \ \lengthfun(\mora) \geq 1, \ \lengthfun(\mora) \geq 2, \dots
\end{align}

We then define the composition rules as

\begin{equation}
\begin{aligned}
\label{eq:berg-comp-bis}
\northenb{\mora}{\nora} & = \thefloor{\nora - \lengthfun(\mora)}, \\
\northena{\nora}{\morb} & = \thefloor{\nora - \lengthfun(\morb)}.
\end{aligned}
\end{equation}

\begin{equation}
\begin{aligned}
\label{eq:berg-comp-round}
\northenb{\mora}{\nora} & = \theround{\nora - \lengthfun(\mora)} \\
\northena{\nora}{\morb} & = \theround{\nora - \lengthfun(\morb)}
\end{aligned}
\end{equation}

In this case, (<ref>) is satisfied, however our nategory is not exact, because in general

\begin{equation}
\begin{aligned}
\nomtohom{\Obja}{\Objc}(\northenb{\mora}{\nora}) & =\{\morb\colon \lengthfun(\morb) < \thefloor{\nora-\lengthfun(\mora)}\} \\
& \subsetneq \{\morb \colon \lengthfun(\morb)< \nora -\lengthfun(\mora)\} \\
& =\precomp{\mora}^{-1}(\nomtohom{\Obja}{\Objb}(\nora)),
\end{aligned}
\end{equation}

since $\thefloor{\nora-\lengthfun(\mora)} +\lengthfun(\mora) \leq \nora$.
An analogous reasoning applies to (<ref>). We note that using $\theround{-}$ or $\theceil{-}$ in (<ref>) would violate (<ref>) and (<ref>).

Norphism schemas

So far, we have not discussed heuristics for actually choosing a set $\Nom$ for each pair of objects in $\Berg$. Here are some different ways.

* Non-negativity of lenths. Since path lengths cannot be negative, for all pair of objects $\Obja, \Objb$ we can say that we have a norphism

\begin{equation}\label{eq:nor-schema-zero}
\stylenorph{0}\colon \Obja \norto \Objb.
\end{equation}

If these are our only norphisms, we are providing no new information about paths.

* Bound based on distance in $\reals^3$.
Any path along the mountain cannot be shorter than the distance of a straight line (“as the crow flies”).
Therefore, for two objects $\tupp{\pos^1, \vel^1}$, $\tupp{\pos^2, \vel^2}$, we might
choose the distance $\| \pos^1 - \pos^2 \| $ in $\reals^3$

\begin{equation}\label{eq:nor-schema-distance-R3}
\| \pos^1 - \pos^2 \| \colon \tupp{\pos^1, \vel^1} \norto \tupp{\pos^2, \vel^2}.
\end{equation}

as a norphism.

* Bound based on geodesic distance.
More accurate bounds are given by taking geodesic distance as our norphisms.
This is defined using the metric $d_\manifold$ of the manifold:

\begin{equation}\label{eq:nor-schema-distance-geodesic}
d_\manifold(\pos^1, \pos^2) \colon \tupp{\pos^1, \vel^1} \norto \tupp{\pos^2, \vel^2}.
\end{equation}

* Bound based on steepness interval.
A different kind of norphism is to encode steepness information, and relate it to the steepness of paths, instead of their length.
Given two objects $\tupp{\pos^1, \vel^1}$, $\tupp{\pos^2, \vel^2}$, we can use one of the following bounds

\begin{equation}\label{eq:nor-schema-altitudeU}
\prfcomma{\pos^1_z - \pos^2_z<0}{
|\pos^1_z - \pos^2_z| /\steepnessU\colon \tupp{\pos^1, \vel^1} \norto \tupp{\pos^2, \vel^2}
\end{equation}

\begin{equation}\label{eq:nor-schema-altitudeL}
\prfperiod{\pos^1_z - \pos^2_z>0}{
|\pos^1_z - \pos^2_z| /\steepnessL\colon \tupp{\pos^1, \vel^1} \norto \tupp{\pos^2, \vel^2}
\end{equation}

§ EXAMPLE: CO-DESIGN

The next example revolves around the construction of norphisms for the category of design problems  [2, 6]; this is called $\textbf{Feas}_{\Bool}$ in [6].

The objects of are posets.
The morphisms are design problems (also referred to as feasibility relations or boolean profunctors).
A design problem (DP) $\adpa \colon \funposA \profto \resposB$ is a monotone map of the form $\adp \colon \funposA\op \Ptimes \resposB \toinPos \Bool,$ where $\funposA, \resposB$ are arbitrary posets and $\Bool$ denotes the poset with elements $\makeset{\false, \true}$, with $\false \leq \true$.

The semantics for a DP is that it describes a process which provides a certain functionality, by requiring certain resources.
A design problem $\adp$ is a monotone map, since lowering the requested functionalities will not require more resources, and increasing the available resources will not provide less functionalities.

Morphism composition is defined as follows.
Given DPs $\adpa \colon \funposA \profto \resposB$ and $\adpb \colon \funposB \profto \resposC$, their composite is

\begin{equation}
\defmapperiod{
(\adpa\functhen \adpb)
\funposA\posop \Ptimes \resposC
\toinPos
\Bool
\tup{\funposAopel, \resposCel}
\bigvee_{\posBel \setin \funposB}
\adpa(\funposAopel,\resposBel)
\booland
\adpb(\funposBopel,\resposCel)
\end{equation}

For any poset , the identity DP $\catidof\posA \colon \funposA \profto \resposA$ is the monotone map

\begin{equation}
\label{eq:identity}
\defmapperiod{
\catid_\funposA
\funposA\posop \Ptimes \resposA
\toinPos
\Bool
\tupp{\funposAel_\F{1}\F{\opel},\resposAel_\R{2}}
\funposAel_\F{1} \posleqof{\funposA} \resposAel_\R{2}
\end{equation}

*Interpretation of norphisms in
Given that the morphisms of are feasibility relations, we expect that the norphisms of (“nesign problems” NP), should be infeasibility relations.
We define a nesign problem

$\andpa\colon \funsp \nprofto \ressp$

to be a monotone map $\andpa\colon \funsp \Ptimes \ressp\op \to \Bool$, and we interpret $\andpa(f,r\opel)=\true$ to mean that it is not possible to produce $f$ from $r$.

The idea is that if $\tup{f_1, r_1}$ is infeasible, then $f_1 \posleqof{} f_2$ implies that $\tup{f_2, r_1}$ is also infeasible and $r_2 \posleqof{} r_1$ implies that $\tup{f_1, r_2}$ is also infeasible. Note that the source poset of a nesign problem is the $\op$ of the source poset for a design problem.

*Compatibility of morphisms and norphisms
Consider a DP $\adp\colon \funsp \profto \ressp$ and a NP $\andpa\colon \funsp \nprofto \ressp$.
The compatibility relation between DP and NP should ensure that there are no contradictions.
We ask that, for any pair of functionality/resources $\tup{f,r}$, it cannot happen that they are declared feasible by the DP ($\adpa(f\opel,r)$) and declared infeasible by the NP ($\andpa(f,r\opel)$):

\begin{equation}
\nmincompat{\funsp}{\ressp} (\andpa, \adp) = \exists f\setin \funsp, r\setin \ressp \colon \adpa(f\opel,r)\wedge \andpa(f,r\opel).
\end{equation}

*Composition rules for norphisms
Given a NP $\andpa\colon \posA \nprofto \posB$ and a DP $\adpa\colon \posC \profto \posB$, one can compose them to get a NP $\northena{\andpa}{\adpa}\colon \posA \nprofto \posC$:

\begin{equation}
(\northena{\andpa}{\adpa})(\posAel,\posCel\opel)=\bigvee_{\posBel \setin \posB}\andpa(\posAel, \posBel\opel) \booland \adp(\posCel\opel, \posBel).
\end{equation}

And given a DP $\adpa\colon \posB\profto \posA$ and a NP $\andpa\colon \posB \nprofto \posC$, one can compose them to get a NP $\adpa \northenbsymb \andpa\colon \posA \nprofto \posC$:

\begin{equation}
(\northenb{\adpa}{\andpa})(\posAel,\posCel\opel)=\bigvee_{\posBel \setin \posB}\adp(\posBel\opel, \posAel)\booland \andpa(\posBel, \posCel\opel).
\end{equation}

The composition rules satisfy (<ref>) and (<ref>) and are exact, as may easily be checked.

Consider the posets $\posA=\tup{\natnumbers_{[\mathrm{kg \ pears}]},\leq}$, $\posB=\tup{\mathbb{R}_{\geq 0,[\mathrm{CHF}]},\leq }$, and $\posC=\tup{\natnumbers_{[\mathrm{kg \ raisins}]},\leq}$.
Consider the design problem $\adp\colon \posC \profto \posB$ and the nesign problem $\andpa\colon \posA \nprofto \posB$ given, respectively, by the (in)feasibility relations

\begin{equation*}
\prfdoublecomma{\adpa(\F{r}\opel,\R{q})}{\F{r}\cdot 10 \leq \R{q}}\qquad
\prfdoubleperiod{\andpa(\F{p},\R{q}\opel)}{\F{p}\cdot 5 > \R{q}}
\end{equation*}

These say that it is possible to buy raisins at [10]CHF/kg or more, and never possible to buy pears at less than [5]CHF/kg.
We can evaluate the composition $(\northena{\andpa}{\adpa})\colon \posA \nprofto \posC$ in a particular point to understand its meaning. For instance:

\begin{equation*}
\begin{aligned}
(\northena{\andpa}{\adpa})(\F{10},\R{4}\opel) & =\bigvee_{\posBel \setin \posB}\andpa(10, \posBel\opel) \booland \adp(4\opel, \posBel) \\
& =\bigvee_{\posBel \setin \posB} (40\leq q < 50)=\true.
\end{aligned}
\end{equation*}

This equation is saying that we cannot get 10 kilos of pears from 4 kilos of raisins. The rationale is that, if I could, then I would be able to start with $40$ CHF and use $\adpa$ to get  $4$ kilos of raisins, which I could then use to obtain $10$ kilos of pears. But this would contradict the norphism $\andpa$, because $\andpa(10,40) = \true$ holds and this means that it is infeasible to exchange $40$ CHF for 10 kilos of pears.

Let $\posA=\posB=\posC=\tup{\reals_{[\mathrm{J}]},\leq}$, with $\posB$ representing potential energy, and $\posA$, $\posC$ representing kinetic energy. We will consider two machines which each convert potential energy into kinetic energy. Let $\adp\colon \posC \profto \posB$ be a design problem that describes “machine 1”, and $\andpa\colon \posA \nprofto \posB$ a nesign problem describing “machine 2” .
Let the (in)feasibility relations be

\begin{equation*}
\prfdoublecomma{\adpa(\F{r}\opel,\R{q})}{\F{r}\cdot 1.1 \leq \R{q}}\qquad
\prfdoubleperiod{\andpa(\F{p},\R{q}\opel)}{\F{p}\cdot 1.2 > \R{q}}
\end{equation*}

These say that for machine 1, energy losses during conversion occur with at least factor 1.1 and for machine 2, losses are always more than a factor 1.2.
We can evaluate the composition $(\northena{\andpa}{\adpa})\colon \posA \nprofto \posC$ in a particular point to understand its meaning.
For instance:

\begin{equation*}
\begin{aligned}
(\northena{\andpa}{\adpa})(\F{10},\R{9}\opel) & =\bigvee_{\posBel \setin \posB}\andpa(10, \posBel\opel) \booland \adp(9\opel, \posBel) \\
& =\bigvee_{\posBel \setin \posB} (9.9\leq q < 12)=\true.
\end{aligned}
\end{equation*}

This equation is saying that we cannot get 10 J of kinetic energy out of 9 J kinetic energy. The rationale in this example (beyond the laws of physics) is that if I could, then I would be able to start with $q = 9.9$ J of potential energy and use machine 1 to obtain $r = 9$ J kinetic energy, which I could then convert to $p = 10$ J kinetic energy. But this would contradict the norphism $\andpa$ related to machine 2, since $\andpa(10,9.9) = \true$ means that it is infeasible to convert 9.9 J potential energy into 10 J kinetic energy.

[inline]JL: The above example still doesn't make sense because if we relate $n$ specifically to machine 2, then we don't get a contradicition... we only get a contradicition if $n$ is a general statement about any morphisms from the given source to the given target. But if we take this interpretation, its a bit weird to have $P$ and $R$ as seperate posets... but if they are the same, then the (in)feasability relations given contradict each other! Another way to see that something is maybe amiss is to note that the “identity” DP between P and R would be infeasible in this example, essentially because the (in)feasibility relations that are given are not mutually compatible.

*Norphism schemas
Considerations about how to define norphisms might follow from specific knowledge about particular designs that we know are (in)feasible, as well as from more general principles of physics or information theory. One very general rule that is arguably valid across all fields: in this universe, physically realizable designs can never produce strictly more of the same resource than one started with. This rule can be encoded as a norphism.
For each object $\posA$, we postulate a NP

\begin{equation}\label{eq:postulate-NP}
\andpa_\posA \colon \posA\nprofto \posA,
\end{equation}

such that

\begin{equation}\label{eq:postulate-NP-val}
\andpa_\posA(\posBel,\posAel\opel) = \posAel \posprecof{\posA} \posBel,
\end{equation}

where $\posAel \posprecof{\posA} \posBel = (\posAel \posleqof{\posA} \posBel ) \wedge (\posAel \neq \posBel )$.

Interestingly, starting from any morphism

\begin{equation}\label{eq:adp}
\adp\colon \funsp \profto \ressp,
\end{equation}

one can directly obtain two NPs that go in the opposite direction, $\ressp \nprofto \funsp$.
These are

\begin{equation}\label{eq:inverse1}
(\northena{\andpa_\ressp}{\adp})(r,f\opel)=\bigvee_{r'\setin \ressp}\andpa_\ressp(r,{r'}\opel)\wedge \adp(f\opel,r'),
\end{equation}

\begin{equation}\label{eq:inverse2}
(\northenb{\adp}{\andpa_\funsp})(r,f\opel)=\bigvee_{f'\setin \funsp} \adp(f{'}\opel,r)\wedge \andpa_\funsp(f',f\opel).
\end{equation}

which gives two impossibility results.
The first states infeasibility because, while it is possible to get $f$ from $r'$ via $\adp$ for a certain $r'$, it is not possible to obtain $r$ from $r'$.
The second states infeasibility because, while it is possible to get $f'$ from $r$ via $\adp$ for a certain $f'$, it is not possible to obtain $f'$ from $f$.
In this nategory, we see that positive information induces negative information in the other direction.

Given any poset $\funposA$ the identity nesign problem is given by:

\begin{equation*}
\begin{aligned}
\ndpid\colon \funposA\Ptimes \resposA\op & \toinPos \Bool \\
\tup{\posAnel{1},\posAnel{2}\opel}       & \mapsto \posAnel{2}\possuccof{\posA} \posAnel{1}.
\end{aligned}
\end{equation*}

[inline]Collage interpretation, with choice of assumptions, but composition general

§ THE CATEGORY $\GSET$

The dialectica construction $\GC$ is due to De Paiva [3, 4], and its instantiation in the case $\CatC = \Set$ has been studied from a “questions and answers” perspective, for example in [1].
We will focus on , however our discussion is also interesting for other cases of the $\GC$ construction.

Recently, the $\GG(\CatC)$ construction and polynomial functors have been related to each other via a common generalization  <cit.>.

An object of is a tuple

\begin{equation}
\tup{\gcQ, \gcA, \gcR},
\end{equation}

where $\gcQ$ and $\gcA$ are sets, and $\gcR : \gcQ \toinRel \gcA$ is a relation.

A morphism
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcR_1}
\mtoin\GC
\tupp{\gcQ_2, \gcA_2, \gcR_2}
is a pair of maps

\begin{align}
\gcma = & \,\tupp{\gcmab, \gcmaf}, \\
& \ \gcmab: \gcQ_1 \mfromin\Set \gcQ_2, \\
& \ \gcmaf: \gcA_1 \mtoin\Set \gcA_2,
\end{align}

that satisfy the property

\begin{equation}\label{eq:010-gset-mor-cond}
\forall \gcq_2: \gcQ_2 \quad \forall \gca_1: \gcA_1 \quad
\inrel{\gcmab(\gcq_2)}{\gcR_1}{\gca_1}
\ \Imp\
\inrel{\gcq_2}{\gcR_2}{\gcmaf(\gca_1)}.
\end{equation}

Morphism composition is defined component-wise

\begin{align}
\gcmB{\theseries} = \gcmbb \functhen \gcmab, \\
\gcmF{\theseries} = \gcmaf \functhen \gcmbf,
\end{align}

and satisfies (<ref>) via composition of implications.

The identity at $\tup{\gcQ, \gcA, \gcR}$ is
\catidat{\tup{\gcQ, \gcA, \gcR}} =
\tup{
\catidat{\gcQ}, \catidat{\gcA}

Our notation was chosen to facilitate a “questions and answers” interpretation [1].
In this perspective, an object of is a “problem”: a relation $\gcR$ between
a set of questions $\gcQ$ and a set of answers $\gcA$.
For a particular question $\gcq\in\gcQ$
and answer $\gca\in\gcA$, $\inrel{\gcq}{\gcR}{\gca}$ means that the answer is correct for the question.
A morphism $
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcR_1}
\mtoin\GC
\tupp{\gcQ_2, \gcA_2, \gcR_2}
$ is a reduction of problem 2 to problem 1, in the sense that we can use a solution to problem 1 to solve problem 2.
The idea is that we start from a question $\gcq_2$ and transform it to a question $\gcq_1 = \gcmab(\gcq_2)$ of the first problem. Assuming we can find an answer $\gca_1$ to $\gcq_1$, we can then transform it in an answer of the second problem $\gca_2 = \gcmaf(\gca_1)$. The condition (<ref>) ensures that the answer so produced is correct for the second problem.

We now rewrite the objects of in a slightly different way.
Instead of

\begin{equation}
\gcR : \gcQ \toinRel \gcA,
\end{equation}

we can write this relation as a boolean function

\begin{equation}
\label{eq:gcc-bool}
\gcC \colon \gcQ \cartprod \gcA \to \makeset{\false, \true}.
\end{equation}

Letting $\Bool$ denote the category with two objects “$\false$” and “$\true$” and a single non-identity morphism $\Imp\colon \false \mto_{\Bool} \true$, we can rewrite (<ref>) again as

\begin{equation}\label{eq:dependent-implications}
\gcC \colon \gcQ \cartprod \gcA \to \Obof \Bool.
\end{equation}

And then condition (<ref>) can be rewriten as a dependent function

\begin{equation}\label{eq:depfun-implication}
\gcmae : \{\gcq_2: \gcQ_2, \gca_1: \gcA_1 \}
\to \gcC_1 (\gcmab(\gcq_2), \gca_1)
\mtoin\Bool \gcC_2 ( \gcq_2, \gcmaf(\gca_1) ).
\end{equation}

The value $\gcmae(\gcq_2, \gca_1)$ is a morphism in $\Bool$ that witnesses an implication.

One idea that we find interesting is to replace $\Bool$ with some other category (on which we may wish to place suitable assumptions) and can consider maps of the form

\begin{equation}
\gcC \colon \gcQ \cartprod \gcA \to \Obof \CatB.
\end{equation}

If $\CatB$ is some category whose morphisms are “proofs”, the analogue of (<ref>)
chooses a proof which is just one among many possible proofs (and such proofs might themselves be ordered by relevance or other criteria).

Let be any category.
An object of the category $\GSetB$ is a tuple

\begin{equation}
\tup{\gcQ, \gcA, \gcC},
\end{equation}

where $\gcQ$ is a set; $\gcA$ is a set, $\gcC$ is a function

\begin{equation}
\gcC \colon \gcQ \cartprod \gcA \to \Obof\CatB.
\end{equation}

A morphism
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcC_1}
\mto%
\tupp{\gcQ_2, \gcA_2, \gcC_2}
is a tuple of three functions

\begin{align}
\gcma = & \,\tupp{\gcmab, \gcmaf, \gcmae}, \\
& \ \gcmab: \gcQ_1 \mfromin\Set \gcQ_2, \\
& \ \gcmaf: \gcA_1 \mtoin\Set \gcA_2, \\
& \gcmae : \{\gcq_2: \gcQ_2, \gca_1: \gcA_1 \} \label{eq:depfun}
\to \gcC_1 (\gcmab(\gcq_2), \gca_1)
\mtoin\CatB \gcC_2 ( \gcq_2, \gcmaf(\gca_1) ).
\end{align}

The composition of the above morphism $\gcma$ with

\gcmb \colon \tupp{\gcQ_2, \gcA_2, \gcC_2}
\mto %
\tupp{\gcQ_3, \gcA_3, \gcC_3}
is defined as follows:

\begin{align}
\gcmB{\theseries} & = \gcmbb \functhen \gcmab, \\
\gcmF{\theseries} & = \gcmaf \functhen \gcmbf, \\
\gcmE{\theseries} & \colon
\tupp{\gcq_3, \gca_1}
\mapsto
\gcmae (\gcmbb(\gcq_3) , \gca_1)
\mthenof\CatB
\gcmbe (\gcq_3 , \gcmaf(\gca_1) ).
\end{align}

More explicitly,

\begin{equation}
\begin{aligned}
\gcmE{\theseries}
\colon
\tupp{\gcq_3, \gca_1}
\mapsto \\
& \gcC_1( (\gcmbb \functhen \gcmab)(\gcq_3), \gca_1)
\xrightarrow{\mbox{$\gcmae (\gcmbb(\gcq_3) , \gca_1 )$}}
\gcC_2( \gcmbb(\gcq_3), \gcmaf(\gca_1))
\xrightarrow{\mbox{$\gcmbe (\gcq_3 , \gcmaf(\gca_1) )$}}%
\gcC_3(\gcq_3, (\gcmaf \functhen \gcmbf) (\gca_1)).
\end{aligned}
\end{equation}

The identity at $\tupp{\gcQ, \gcA, \gcC}$ is given by $\tupp{\catidat{\gcQ}, \catidat{\gcA},
\tupp{\gcq, \gca} \mapsto \catidat{\gcC(\gcq,\gca)}}$.

For completeness, we give the further generalization, in which we have instead of and $\gcmae$ becomes a natural transformation.

Given a category $\gcE$,
an object of $\GG(\Category, \gcE)$ is a tuple

\begin{equation}
\tup{\gcQ, \gcA, \gcC },
\end{equation}

where $\gcQ$ is a category, $\gcA$ is a category, $\gcC$ is a functor

\begin{equation}
\gcC \colon \gcQ \op \times \gcA \to \gcE.
\end{equation}

A morphism
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcC_1}
\mtoin\GCat
\tupp{\gcQ_2, \gcA_2, \gcC_2}
is a tuple

\begin{equation}
\gcma = \tupp{\gcmab, \gcmaf, \gcmae},
\end{equation}

* $\gcmab: \gcQ_2 \mtoin{\Category} \gcQ_1$ is a functor,

* $\gcmaf: \gcA_1 \mtoin{\Category} \gcA_2$ is a functor,

* $\gcmae$ is a natural transformation between two functors

\begin{equation}
\funa, \funb: \gcQ_2\op \times \gcA_1 \to \gcE,
\end{equation}

defined as

\begin{align}
\funa & = (\gcmab \times \funidat{\gcA_1}) \fthen \gcC_1, \\
\funb & = (\funidat{\gcQ_2\op} \times \gcmaf) \fthen \gcC_2 .
\end{align}

[inline]Need to finish with composition

Linear logic binary-operators

connective     unit

multiplicatives     $\lltimes$     $\llone$

$\llpar$       $\llbot$

additives           $\llplus$      $\llzero$

$\llwith$      $\lltop$

§.§ Monoidal product $\gcMeh$

Assume has finite products.
The action on the objects is defined as follows:

\begin{equation}
\tupp{\gcQ_1, \gcA_1, \gcC_1}
\gcMehob
\tupp{\gcQ_2, \gcA_2, \gcC_2}
= \tupp{
\gcQ_1 \cartprod \gcQ_2,
\gcA_1 \cartprod \gcA_2,
\gcC_1 \gcCmeh \gcC_2
\end{equation}

\begin{equation}
\gcC_1 \gcCmeh \gcC_2 : \tupp{\tupp{\gcq_1, \gcq_2}, \tupp{\gca_1, \gca_2}}
\mapsto \gcC_1(\gcq_1, \gca_1) \cprodob\CatB \gcC_2(\gcq_2, \gca_2 ),
\end{equation}

where $\cprodob\CatB$ is the product of two objects in $\CatB$.
The monoidal unit is

\begin{equation}
1_{\gcMeh} = \tupp{\makeset{\theonlyQ}, \makeset{\theonlyA}, \gctrue},
\qquad \gctrue \colon \tupp{\theonlyQ, \theonlyA} \mapsto \termobof\CatB.
\end{equation}

The product of
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcC_1}
\mto
\tupp{\gcQ_3, \gcA_3, \gcC_3} $ and $
\gcmb \colon \tupp{\gcQ_2, \gcA_2, \gcC_2}
\mto
\tupp{\gcQ_4, \gcA_4, \gcC_4}
$ is

\begin{equation}
\gcma \gcMehmor \gcmb \colon
\tupp{
\gcQ_1 \cartprod \gcQ_2 ,
\gcA_1 \cartprod \gcA_2,
\gcC_1 \gcCmeh \gcC_2
\mto
\tupp{
\gcQ_3 \cartprod \gcQ_4,
\gcA_3 \cartprod \gcA_4,
\gcC_3 \gcCmeh \gcC_4
\end{equation}

\begin{align}
\gcmB{\themeh} & = \gcmab \funcprod \gcmbb, \\
\gcmF{\themeh} & = \gcmaf \funcprod \gcmbf, \\
\gcmE{\themeh} & \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto
\gcmae ( \gcq_3, \gca_1)
\cprodmor\CatB
\gcmbe (\gcq_4, \gca_2).
\label{eq:meh-m}
\end{align}

§.§ Monoidal product $\lltimes$

Assume has finite products.
The action on the objects is defined as follows:

\begin{equation}
\tupp{\gcQ_1, \gcA_1, \gcC_1}
\lltimesob
\tupp{\gcQ_2, \gcA_2, \gcC_2}
= \tupp{
\gcQ_1 ^ {\gcA_2} \cartprod \gcQ_2 ^ {\gcA_1},
\gcA_1 \cartprod \gcA_2,
\gcC_1 \gcCtimes \gcC_2
\end{equation}

\begin{equation}
\gcC_1 \gcCtimes \gcC_2 : \tupp{\tupp{\gcq_1, \gcq_2}, \tupp{\gca_1, \gca_2}}
\mapsto \gcC_1(\gcq_1(\gca_2), \gca_1) \cprodob\CatB \gcC_2(\gcq_2 (\gca_1), \gca_2 ),
\end{equation}

where $\cprodob\CatB$ is the product of two objects in $\CatB$.
The monoidal unit is

\begin{equation}
1_{\otimes} = \tupp{\makeset{\theonlyQ}, \makeset{\theonlyA}, \gctrue},
\qquad \gctrue \colon \tupp{\theonlyQ, \theonlyA} \mapsto \termobof\CatB.
\end{equation}

The product of
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcC_1}
\mto
\tupp{\gcQ_3, \gcA_3, \gcC_3} $ and $
\gcmb \colon \tupp{\gcQ_2, \gcA_2, \gcC_2}
\mto
\tupp{\gcQ_4, \gcA_4, \gcC_4}
$ is

\begin{equation}
\gcma \lltimesmor \gcmb \colon
\tupp{
\gcQ_1 ^ {\gcA_2} \cartprod \gcQ_2 ^ {\gcA_1},
\gcA_1 \cartprod \gcA_2,
\gcC_1 \gcCtimes \gcC_2
\mto
\tupp{
\gcQ_3 ^ {\gcA_4} \cartprod \gcQ_4 ^ {\gcA_3},
\gcA_3 \cartprod \gcA_4,
\gcC_3 \gcCtimes \gcC_4
\end{equation}

\begin{align}
\gcmB{\theprod} & =
\tupp{
\gcmbf \functhen - \functhen \gcmab,
\gcmaf \functhen - \functhen \gcmbb
}, \\
\gcmF{\theprod} & = \gcmaf \funcprod \gcmbf, \\
\gcmE{\theprod} & \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto
\gcmae ( (\gcmbf\functhen\gcq_3)(\gca_2), \gca_1)
\cprodmor\CatB
\gcmbe ( (\gcmaf\functhen\gcq_3)(\gca_1), \gca_2).
\label{eq:otimes-m}
\end{align}

The “$\cprodmor\CatB$” in (<ref>) is the product of the two morphisms in $\CatB$.

§.§.§ Derivation of (<ref>)

The function $\gcmE{\theprod}$ needs to have type

\begin{align}
\gcmE{\theprod} : & \{\tupp{\gcq_3, \gcq_4} : \gcQ_3 ^ {\gcA_4} \cartprod \gcQ_4 ^ {\gcA_3},
\tupp{\gca_1, \gca_2}: \gcA_1 \cartprod \gcA_2 \}
\to \\
& \gcC_1 \gcCtimes \gcC_2 \pars{\gcmB{\theprod}(\tupp{\gcq_3, \gcq_4}) , \tupp{\gca_1, \gca_2}}
\mtoin\CatB \\
& \gcC_3 \gcCtimes \gcC_4 \pars {\tupp{\gcq_3, \gcq_4}, \gcmaf \funcprod \gcmbf(\tupp{\gca_1, \gca_2}) }
\end{align}

Simplifying, we get that we should find a map

\begin{align}
\gcmE{\theprod} & \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto \\
& \gcC_1 \gcCtimes \gcC_2 \pars{\tupp{\gcmbf \functhen \gcq_3 \functhen \gcmab, \gcmaf \functhen \gcq_4 \functhen \gcmbb} , \tupp{\gca_1, \gca_2}}
\mtoin\CatB \\
& \gcC_3 \gcCtimes \gcC_4 \pars {\tupp{\gcq_3, \gcq_4}, \tupp{\gcmaf(\gca_1), \gcmbf(\gca_2)} }
\end{align}

Expanding $\gcC_1 \gcCtimes \gcC_2$ and $\gcC_3 \gcCtimes \gcC_4$ we have

\begin{align}
\gcmE{\theprod} & \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto \\
& \gcC_1(\gcmab(\gcmbf \functhen \gcq_3 (\gca_2)), \gca_1) \cprodob\CatB
\gcC_2(\gcmbb(\gcmaf \functhen \gcq_4 (\gca_1)), \gca_2 )
\mtoin\CatB \\
& \gcC_3(\gcmbf \functhen \gcq_3(\gca_2), \gcmaf(\gca_1))
\cprodob\CatB
\gcC_4(\gcmaf \functhen \gcq_4(\gca_1), \gcmbf(\gca_2) )
\end{align}

Now notice that we can use $\gcmae$ and $\gcmbe$ to obtain the two morphisms

\begin{align}
\gcmae ( (\gcmbf\functhen\gcq_3)(\gca_2), \gca_1): \gcC_1(\gcmab(\gcmbf \functhen \gcq_3 (\gca_2)), \gca_1)
\mtoin\CatB \gcC_3(\gcmbf \functhen \gcq_3(\gca_2), \gcmaf(\gca_1))
\\
\gcmbe ( (\gcmaf\functhen\gcq_3)(\gca_1), \gca_2): \gcC_2(\gcmbb(\gcmaf \functhen \gcq_4 (\gca_1)), \gca_2 )
\mtoin\CatB \gcC_4(\gcmaf \functhen \gcq_4(\gca_1), \gcmbf(\gca_2) )
\end{align}

Therefore, we can take the product of the two morphisms and obtain a morphism of the right type:

\begin{equation}
\gcmE{\theprod} \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto
\gcmae ( (\gcmbf\functhen\gcq_3)(\gca_2), \gca_1)
\funcprod
\gcmbe ( (\gcmaf\functhen\gcq_3)(\gca_1), \gca_2).
\end{equation}

§.§ Monoidal product $\llpar$

Assume has finite coproducts.
The action on the objects is defined as follows:

\begin{equation}
\tupp{\gcQ_1, \gcA_1, \gcC_1}
\llparob
\tupp{\gcQ_2, \gcA_2, \gcC_2}
= \tupp{
\gcQ_1 \cartprod \gcQ_2,
\gcA_1 ^ {\gcQ_2} \cartprod \gcA_2 ^ {\gcQ_1},
\gcC_1 \gcCpar \gcC_2
\end{equation}

\begin{equation}
\gcC_1 \gcCpar \gcC_2 : \tupp{\tupp{\gcq_1, \gcq_2}, \tupp{\gca_1, \gca_2}}
\mapsto \gcC_1(\gcq_1(\gca_2), \gca_1) \csumob\CatB \gcC_2(\gcq_2(\gca_1), \gca_2 ),
\end{equation}

where $\csumob\CatB$ is the coproduct of two objects in $\CatB$.

The monoidal unit is

\begin{equation}
1_{\llpar} = \tupp{\makeset{\theonlyQ}, \makeset{\theonlyA}, \gcfalse}, \qquad \gcfalse \colon \tupp{\theonlyQ, \theonlyA} \mapsto \initobof\CatB.
\end{equation}

The product of
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcC_1}
\mto
\tupp{\gcQ_3, \gcA_3, \gcC_3}$, $
\gcmb \colon \tupp{\gcQ_2, \gcA_2, \gcC_2}
\mto
\tupp{\gcQ_4, \gcA_4, \gcC_4}

\begin{equation}
\gcma \llparmor \gcmb \colon
\tupp{
\gcQ_1 \cartprod \gcQ_2,
\gcA_1 ^ {\gcQ_2} \cartprod \gcA_2 ^ {\gcQ_1},
\gcC_1 \gcCpar \gcC_2
\mto
\tupp{
\gcQ_3 \cartprod \gcQ_4,
\gcA_3 ^ {\gcQ_4} \cartprod \gcA_4 ^ {\gcQ_3},
\gcC_3 \gcCpar \gcC_4
\end{equation}

\begin{align}
\gcmB{\thepar} & = \gcmab \funcprod \gcmbb, \\
\gcmF{\thepar} & =
\tupp{
\gcmbb \functhen - \functhen \gcmaf,
\gcmab \functhen - \functhen \gcmbf
}, \\
\gcmE{\thepar} & \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto
\gcmae ( \dots, \gca_1)
\csummor\CatB
\gcmbe (\dots, \gca_2).
\label{eq:par-m}
\end{align}

where $\csummor\CatB$ is the coproduct of two morphisms in $\CatB$.

[inline]Finish formula above

§.§ A monoidal product for $\GSet$

The categories $\GC$ have a very rich structure.
In particular they provide models of linear logic with four distinct monoidal products $\lltimes$, $\llpar$, $\llplus$, and $\llwith$.
We define here a monoidal product $\gcPlus$ for $\GSet$ which one might say is “in between” the the multiplicative connectives $\lltimes$ and $\llpar$ (which are denoted $\oslash$ and $\square$, respectively, in [3, 4]).

On objects,

\begin{equation}
\tupp{\gcQ_1, \gcA_1, \gcC_1}
\gcPlusob
\tupp{\gcQ_2, \gcA_2, \gcC_2}
= \tupp{
\gcQ_1 ^ {\gcA_2} \cartprod \gcQ_2 ^ {\gcA_1},
\gcA_1 \cartprod \gcA_2,
\gcC_1 \gcCplus \gcC_2
\end{equation}

\begin{equation}
\gcC_1 \gcCplus \gcC_2: \tupp{\tupp{\gcq_1, \gcq_2}, \tupp{\gca_1, \gca_2}}
\mapsto \gcC_1(\gcq_1(\gca_2), \gca_1) \vee \gcC_2(\gcq_2(\gca_1), \gca_2 ).
\end{equation}

The product of morphisms
\gcma \colon \tupp{\gcQ_1, \gcA_1, \gcC_1}
\mto
\tupp{\gcQ_3, \gcA_3, \gcC_3}$ and $
\gcmb \colon \tupp{\gcQ_2, \gcA_2, \gcC_2}
\mto
\tupp{\gcQ_4, \gcA_4, \gcC_4}
$ is

\begin{equation}
\gcma \gcPlusmor \gcmb \colon
\tupp{
\gcQ_1 ^ {\gcA_2} \cartprod \gcQ_2 ^ {\gcA_1},
\gcA_1 \cartprod \gcA_2,
\gcC_1 \gcCplus \gcC_2
\mto
\tupp{
\gcQ_3 ^ {\gcA_4} \cartprod \gcQ_4 ^ {\gcA_3},
\gcA_3 \cartprod \gcA_4,
\gcC_3 \gcCplus \gcC_4
\end{equation}

\begin{align}
\gcmB{\thesum} & = %
\tupp{
\gcmbf \functhen - \functhen \gcmab,
\gcmaf \functhen - \functhen \gcmbb
}, \\
\gcmF{\thesum} & = \gcmaf \funcprod \gcmbf, \\
\gcmE{\thesum} & \colon \tupp{\tupp{\gcq_3, \gcq_4}, \tupp{\gca_1, \gca_2}}
\mapsto
\gcmae ( \gcmbf\functhen\gcq_3(\gca_2), \gca_1)
\vee
\gcmbe ( \gcmaf\functhen\gcq_3(\gca_1), \gca_2).
\label{eq:oplus-sum}
\end{align}

The monoidal unit is

\begin{equation}
1_{\gcPlus} = \tupp{\makeset{\theonlyQ}, \makeset{\theonlyA}, \gcfalse},
\qquad
\gcfalse \colon \tupp{\theonlyQ, \theonlyA} \mapsto \false.
\end{equation}

For the associator and unitors we make the canonical choices, which are easily inferred from their signatures.
We refrain from writing them out explicitly here.
For reasons of space we also omit the the proof that $\tupp{\GSet,\gcPlus}$ is indeed a monoidal category.

In the generalization where we replace $\Bool$ with some category $\CatB$, the operation $\vee$ and the object $\false$ in $\Bool$ which are used in the above definition would be replaced by suitable substitutes in $\CatB$.

§ DESCRIBING NATEGORIES USING ENRICHMENT

We recall the following standard definition of enriched category [7], for easy reference and to fix notation.

Let $\tup{\CatV, \mtimescat, \idmoncat, \associator, \leftunitor,\rightunitor}$ be a monoidal category.

A -enriched category is a tuple
\tupp{\Ob_\CatE, \homobjectset{}, \enm, \enid_{}},

* $\Ob_\CatE$ is a collection of objects.

* $\homobjectset{}$ is a function such that, for all pairs of objects $\Obja,\Objb\setin \Ob_\CatE$, its value $\homobject{}{\Obja}{\Objb}$ is an object of $\CatV$, called a hom-object.

* $\enm$ is a function such that, for all $\Obja, \Objb, \Objc\setin \Ob_\CatE$, there exists a morphism $\enmof{}{\Obja}{\Objb}{\Objc}$ of
\begin{equation}
\enmof{}{\Obja}{\Objb}{\Objc}\colon\homobject{}{\Obja}{\Objb} \mtimescatob \homobject{}{\Objb}{\Objc} \mtoin\CatV \homobject{}{\Obja}{\Objc},
\end{equation}

called a composition morphism.

* $\enid_{}$ is a function such that, for each $\Obja\setin \ObE$, there exists a morphism of
\begin{equation}
\enidof{}{\Obja} \colon \idmoncat \mtoin{\CatV} \homobject{}{\Obja}{\Obja},
\end{equation}

called an identity-choosing morphism.

Moreover, for any $\Obja,\Objb,\Objc,\Objd\setin \ObE$, the following diagrams must commute.

\begin{equation}
\label{eq:enrichment-assoc2-act}
\includesag{enrichment_assoc}
\end{equation}

\begin{equation}
\label{eq:enrichment-unital2}
\includesag{enrichment_unital}
\end{equation}

Recall that specifying the data of an ordinary (locally small) category is equivalent to specifying a category enriched in the monoidal category $\prcatp=\tup{\Set, \cartprod, \singleton}$.
In this case, both the enriched category and the ordinary category have the same objects, the hom-objects of the enriched category correspond to the hom-sets of the ordinary category, the composition morphisms encode the composition operations, and the identity-choosing morphisms select an element of each of the hom-sets of the type $\homobject{}{\Obja}{\Obja}$, corresponding to identity morphisms.
The diagrams (<ref>) and (<ref>) encode the associativity of the composition operations, and that the identity morphisms act neutrally for composition.

We show one direction.
Suppose that we are given a $\prcatp$-enriched category as a tuple
$\tupp{\Ob, \homobjectset{}, \enm, \enid_{}}.
We can define a small category $\CatC$  as follows:

* Set $\ObC \definedas \ObE$.

* For each $\Obja,\Objb\setin\ObC$, let $\HomSet{\CatC}{\Obja}{\Objb} \definedas \homobject{}{\Obja}{\Objb}$.

* For each $\Obja,\Objb,\Objc \setin \ObC$, we know a function

\begin{equation}
\enmof{}{\Obja}{\Objb}{\Objc}:\HomSet{\CatC}{\Obja}{\Objb}\mtimescat \HomSet{\CatC}{\Objb}{\Objc}\mtoin{\Set} \HomSet{\CatC}{\Obja}{\Objc}.
\end{equation}

The diagrams constraints imply that this function is associative.

Therefore, we use it to define morphism composition in $\CatC$, setting $\mthen_{\Obja,\Objb,\Objc}\definedas \enmof{}{\Obja}{\Objb}{\Objc}$.

* For each $\Obja\setin\ObC$ we know a function $\enidof{}{\Obja}\colon\singleton\mtoin{\Set} \HomSet{\CatC}{\Obja}{\Obja}$ that selects a morphism.

The diagrams constraints imply that such morphism satisfies unitality
with respect to $\mthen_{\Obja,\Objb,\Objc}$.
Therefore, we can use it to define the identity at each object:

\begin{equation}
\label{eq:ja-hom}
\catidat{\Obja} \definedas \enidof{}{\Obja}(\singletonel).
\end{equation}

The commutative diagrams are clearly satisfied, by choosing the obvious associator and left/right unitors.

The proof of our main result below follows a similar pattern – we show that to specify a nategory which satisfies some additional conditions it is sufficient to specify a category enriched in the monoidal category $\tup{\GSet, \gcPlus}$.
We will denote $\tup{\GSet, \gcPlus}$ by , which stands for “positive” and “negative”.

A -enriched category provides the data necessary to specify a nategory.
However, not all nategories can be specified by the data of a -enriched category,
because the nategory produced has the following additional properties, which encode a covariant and a contravariant “action” of morphisms on norphisms.

Identities act neutrally:

\begin{align}
\northenb{\catidat{}}{\nora}  = \nora \tag{neut-1} \label{eq:neutrality1}, \\
\northena{\nora}{\catidat{}} = \nora \tag{neut-2}\label{eq:neutrality2}.
\end{align}

Compatibility with composition:

\begin{align}
\northenb{(\morab)}{\nora}            & =\northenb{\morb}{  (\northenb{\mora}{\nora})}, \tag{covar}\label{eq:compat-comp1} \\
\northena{\nora}{ (\morb\mthen\morc)} & =\northena{(\northena{\nora}{\morc})}{\morb}. \tag{contravar}\label{eq:compat-comp2}
\end{align}

The actions commute:

\begin{align}
\northenb{\mora}{ (\northena{\nora}{\morc})} & =\northena{(\northenb{\mora}{\nora}) }{ \morc}.\tag{comm}
\end{align}

These conditions are not satisfied by all nategories.

Suppose somebody has provided us with a -enriched category $\CatE = \tupp{\ObE, \homobjectset{}, \enm, \enid_{}}$.
Using this data we will describe a nategory $\CatC$ with the above-stated properties.

For the objects of , we set $\ObC \definedas \ObE$.

For every pair of objects $\Obja,\Objb \setin \ObC$, we have an object $\homobject{}{\Obja}{\Objb}$ of .
This is a tuple

\begin{equation}\label{eq:tup}
\homobject{}{\Obja}{\Objb} = \tupp{\gcQ, \gcA, \gcC},
\end{equation}

which we interpret as

\begin{equation}\label{eq:tup-interpret}
\homobject{}{\Obja}{\Objb} =\tupp{\NomSet{\CatC}{\Obja}{\Objb}, \HomSet{\CatC}{\Obja}{\Objb}, \nmincompat{\Obja}{\Objb}},
\end{equation}

thereby setting $\NomSet{\CatC}{\Obja}{\Objb} \definedas \gcQ$, $\HomSet{\CatC}{\Obja}{\Objb}\definedas \gcA$, and $\nmincompat{\Obja}{\Objb} \definedas \gcC$.

Next, for each $\Obja \setin \Ob$ we have an identity-choosing morphism

\begin{equation}\label{eq:provided}
\enidof{}{\Obja} \colon \idmoncat_\prcat \mtoin{\prcat} \homobject{}{\Obja}{\Obja}.
\end{equation}

Because $\idmoncat_\prcat=\tupp{\makeset{\theonlyQ}, \makeset{\theonlyA}, \gcfalse}$, this is a morphism

\begin{equation}\label{eq:provided-unroll}
\enidof{}{\Obja}
\colon
\tupp{\makeset{\theonlyQ}, \makeset{\theonlyA}, \gcfalse}
\mtoin{\prcat}
\tupp{
\NomSet{\CatC}{\Obja}{\Obja},
\HomSet{\CatC}{\Obja}{\Obja},
\nmincompat{\Obja}{\Obja}
\end{equation}

which consists of three functions $\tupp{\gcmab, \gcmaf ,\gcmae}$.
The forward map $\gcmaf: \makeset{\theonlyA} \mto \HomSet{\CatC}{\Obja}{\Obja}$ chooses our (candidate) identity morphism, so we set $ \idname_\Obja \definedas \gcmaf(\theonlyA)$.
The backward map $\gcmab
\colon
\NomSet{\CatC}{\Obja}{\Obja}
\to
\makeset{\theonlyQ}$
is uniquely determined and does not carry any information.
As for $\gcmae$, it is a dependent function of the type

\begin{equation}
\gcmae : \{\gcq_2: \NomSet{\CatC}{\Obja}{\Obja}, \gca_1: \makeset{\theonlyA} \}
\to \gcfalse (\gcmab(\gcq_2), \gca_1)
\mtoin\Bool \nmincompat{\Obja}{\Obja} ( \gcq_2, \gcmaf(\gca_1) ).
\end{equation}

Evaluated at $\gcq_2 = \nora$ and $\gca_1 = \theonlyA$, we have

\begin{equation}
\gcmae(\nora,\theonlyA) : \false \mtoin\Bool
\nmincompat{\Obja}{\Obja} ( \nora, \catid_{\Obja} ).
\end{equation}

Because $\false$ is an initial object in $\Bool$, such a morphism always exists,
no matter what the right-hand side is.
Therefore, this condition does not carry any additional information.

Now let us fix three objects $\Obja,\Objb,\Objc$ and consider the composition morphism

\begin{equation}\label{eq:beta}
\enmof{}{\Obja}{\Objb}{\Objc}
\colon \homobject{}{\Obja}{\Objb}
\mtimescatob_\prcat \homobject{}{\Objb}{\Objc}
\mtoin\prcat \homobject{}{\Obja}{\Objc}.
\end{equation}

Rewriting the hom-objects as tuples and using abbreviated notation we have

\begin{equation}\label{eq:beta-ours2}
\enmof{}{\Obja}{\Objb}{\Objc} \colon \tupp{
\Nab,
\Hab,
\nmincompat{\Obja}{\Objb}
\mtimescat_\prcat
\tupp{
\Nbc,
\Hbc,
\nmincompat{\Objb}{\Objc}
\mtoin\prcat \\
\tupp{
\Nac,
\Hac,
\nmincompat{\Obja}{\Objc}
\end{equation}

Expanding using the definition of $\mtimescat_\prcat$ we find

\begin{equation}\label{eq:themorph}
\enmof{}{\Obja}{\Objb}{\Objc} \colon
\tupp{
\Nab^{\Hbc} \cartprod \Nbc^{\Hab},
\Hab \cartprod \Hbc,
\nmincompat{\Obja}{\Objb} \gcCplus \nmincompat{\Objb}{\Objc}
\mtoin\prcat
\tupp{
\Nac,
\Hac,
\nmincompat{\Obja}{\Objc}
\end{equation}

Such a morphism corresponds to three maps $\tupp{\gcmbb, \gcmbf ,\gcmbe}$.
The forward map $\gcmbf $ has type

\begin{equation}\label{eq:morcomp}
\gcmbf \colon \HomSet{\CatC}{\Obja}{\Objb}\cartprod \HomSet{\CatC}{\Objb}{\Objc}
\to \HomSet{\CatC}{\Obja}{\Objc},
\end{equation}

and we use it to define morphism composition “ $\mthenof\CatC$” in our nategory.
The backward map $\gcmbb$ has type

\begin{equation}\label{eq:con-back}
\gcmbb \colon \Nac \to \Nab^{\Hbc} \cartprod \Nbc^{\Hab},
\end{equation}

which, after splitting into two maps (using the universal property of the product) and currying, specifies two maps

\begin{align} \label{eq:con-back2}
\northenasymb & \colon \Nac \cartprod \Hbc \to \Nab,
\\
\northenbsymb & \colon \Hab \cartprod \Nac \to \Nbc.
\end{align}

As for the dependent function $\gcmbe$, given $\nora: \Nac$, $\mora: \Hab$, $\morb: \Hbc$ we have

\begin{equation}\label{eq:proc1}
\gcmbe(\nora,\tup{\mora,\morb})
\colon
(\nmincompat{\Obja}{\Objb} \gcCplus \nmincompat{\Objb}{\Objc}) ( \tupp{ (\nora \northenasymb -), (- \northenbsymb \nora)}, \tup{\mora,\morb})
\mtoin\Bool \nmincompat{\Obja}{\Objc} ( \nora, \morab ).
\end{equation}

Expanding more,

\begin{equation}\label{eq:proc2}
\gcmbe(\nora,\tup{\mora,\morb})
\colon
\nmincompat{\Obja}{\Objb} (\nora \northenasymb \morb, \mora)
\vee
\nmincompat{\Objb}{\Objc} (\mora \northenbsymb \nora, \morb)
\mtoin\Bool
\nmincompat{\Obja}{\Objc} ( \nora, \morab ),
\end{equation}

which is equivalent to having two maps

\begin{align}
\gcmbe_1(\nora,\tup{\mora,\morb})\label{eq:proc3-maps}
\colon
\nmincompat{\Obja}{\Objb} (\northena{\nora}{\morb} , \mora)
\mtoin\Bool
\nmincompat{\Obja}{\Objc} ( \nora, \morab ), \\
\gcmbe_2(\nora,\tup{\mora,\morb})\label{eq:proc4-maps}
\colon
\nmincompat{\Objb}{\Objc}(\northenb{\mora}{\nora}, \morb)
\mtoin\Bool
\nmincompat{\Obja}{\Objc} ( \nora, \morab ).
\end{align}

These witness the implications which give us (<ref>) and (<ref>).

Next we move to the commutative diagrams in the definition of enriched category.
As a general observation, we note that for diagrams in $\GSet$ we only need to consider commutativity on the level of “forward maps” and “backward maps” respectively.
We do not need to worry about the conditions (<ref>), because for any two parallel morphisms this condition is the same, and hence “commutativity” is trivially satisfied.

*Conditions from the associativity diagram for enriched categories
We now consider the diagram (<ref>), in the case of .

On the level of “forward” maps, this commutative diagram encodes that morphism composition must be associative.
One the level of “backward” maps, it implies that the following diagram must commute:

Let us look at the two different routes through this diagram.
For the left-hand route, note that

\begin{equation}
\begin{aligned}
\gcmBdec{(\enmof{}{\Obja}{\Objb}{\Objc}\gcPlus \catid_{\Objc\Objd})} & =\tupp{\gcmF{\catid_{\Objd}}\functhen(-)\functhen \gcmBdec{\enmof{}{\Obja}{\Objb}{\Objc}},\gcmFdec{\enmof{}{\Obja}{\Objb}{\Objc}}\functhen (-)\functhen \gcmB{\catid_{\Objc\Objd}}} \\
& =\tupp{(-)\functhen \gcmBdec{\enmof{}{\Obja}{\Objb}{\Objc}}, \gcmFdec{\enmof{}{\Obja}{\Objb}{\Objc}}\functhen (-)},
\end{aligned}
\end{equation}

and so

\begin{equation}\label{eq:left-hand-route-assoc}
\begin{aligned}
\gcmBdec{\enmof{}{\Objb}{\Objc}{\Objd}}\functhen \gcmBdec{(\enmof{}{\Obja}{\Objb}{\Objc}\gcPlus \catid_{\Objc\Objd})} & \colon
\gcQ_{\Obja\Objd}\to \gcQ_{\Obja\Objc}^{\gcA_{\Objc\Objd}}\times \gcQ_{\Objc\Objd}^{\gcA_{\Obja\Objc}} \to \left(\gcQ_{\Obja\Objb}^{\gcA_{\Objb\Objc}}\times \gcQ_{\Objb\Objc}^{\gcA_{\Obja\Objb}}\right)^{\gcA_{\Objc\Objd}}\times \gcQ_{\Objc\Objd}^{\gcA_{\Obja\Objb}\times \gcA_{\Objb\Objc}} \\
\gcq                                                                                & \mapsto \tupp{\northena{\gcq}{(-)}, \northenb{(-)}{\gcq}}\mapsto \tupp{\northena{\gcq}{(-)}\functhen \gcmBdec{\enmof{}{\Obja}{\Objb}{\Objc}}, \gcmFdec{\enmof{}{\Obja}{\Objb}{\Objc}}\functhen \northenb{(-)}{\gcq}}.
\end{aligned}
\end{equation}

For the right-hand route, note that

\begin{equation}
\begin{aligned}
\gcmBdec{(\catid_{\Obja\Objb}\gcPlus \enmof{}{\Objb}{\Objc}{\Objd})} & =\tupp{\gcmFdec{\enmof{}{\Objb}{\Objc}{\Objd}}\functhen (-)\functhen \gcmB{\catid_{\Obja\Objb}}, \gcmF{\catid_{\Obja\Objb}}\functhen (-)\functhen \gcmBdec{\enmof{}{\Objb}{\Objc}{\Objd}}} \\
& =\tupp{\gcmFdec{\enmof{}{\Objb}{\Objc}{\Objd}}\functhen (-), (-)\functhen \gcmBdec{\enmof{}{\Objb}{\Objc}{\Objd}}},
\end{aligned}
\end{equation}

and so

\begin{equation}\label{eq:right-hand-route-assoc}
\begin{aligned}
\gcmBdec{\enmof{}{\Obja}{\Objb}{\Objd}}\functhen \gcmBdec{(\catid_{\Obja\Objb}\gcPlus \enmof{}{\Objb}{\Objc}{\Objd})} & \colon
\gcQ_{\Obja\Objd}\to \gcQ_{\Obja\Objb}^{\gcA_{\Objb\Objd}}\times \gcQ_{\Objb\Objd}^{\gcA_{\Obja\Objb}}
\to \gcQ_{\Obja\Objb}^{\gcA_{\Objb\Objc}\times \gcA_{\Objc\Objd}}\times \left( \gcQ_{\Objb\Objc}^{\gcA_{\Objc\Objd}}\times \gcQ_{\Objc\Objd}^{\gcA_{\Objb\Objc}}\right)^{\gcA_{\Obja\Objb}} \\
\gcq                                                                                & \mapsto \tupp{\northena{\gcq}{(-)},\northenb{(-)}{\gcq}}\mapsto \tupp{\gcmFdec{\enmof{}{\Objb}{\Objc}{\Objd}}\functhen \northena{\gcq}{(-)}, \northenb{(-)}{\gcq}\functhen \gcmBdec{\enmof{}{\Objb}{\Objc}{\Objd}} }.
\end{aligned}
\end{equation}

Instead of now applying $\gcmB{\associator}$ directly, which is an obvious map but messy to write down, we evaluate the functions we obtained from our calculations for the left- and right-hand routes.
Given $\tupp{\mora,\morb,\morc}\in \gcA_{\Obja\Objb}\times \gcA_{\Objb\Objc}\times \gcA_{\Objc\Objd}$, evaluating the two components of (<ref>) we find

\begin{equation}
(\gcq \northenasymb (-) \functhen \gcmBdec{\enmof{}{\Obja}{\Objb}{\Objc}})(\morc)=
\gcmBdec{\enmof{}{\Obja}{\Objb}{\Objc}}(\northena{\gcq}{\morc})\colon \tupp{\morb,\mora}\mapsto \tupp{\northena{(\northena{\gcq}{\morc})}{\morb}, \northenb{\mora}{(\northena{\gcq}{\morc})}},
\end{equation}

\begin{equation}
(\gcmFdec{\enmof{}{\Obja}{\Objb}{\Objc}}\functhen \northenb{(-)}{\gcq})(\tupp{\mora,\morb})=\northenb{(\mora\functhen \morb)}{\gcq},
\end{equation}

For the right-hand route, evaluating (<ref>) gives

\begin{equation}
(\gcmFdec{\enmof{}{\Objb}{\Objc}{\Objd}}\functhen \northena{\gcq}{(-)})(\tupp{\morb,\morc})=\northena{\gcq}{(\morb\functhen \morc)},
\end{equation}

\begin{equation}
(\northenb{(-)}{\gcq} \functhen \gcmBdec{\enmof{}{\Objb}{\Objc}{\Objd}})(\mora)=\gcmBdec{\enmof{}{\Objb}{\Objc}{\Objd}}(\northenb{\mora}{\gcq}) \colon \tupp{\morc,\morb}\mapsto \tupp{\northena{(\northenb{\morb}{\gcq})}{\mora}, \northenb{\morb}{(\northenb{\mora}{\gcq})}}.
\end{equation}

By comparing the two routes, we obtain the conditions

\begin{equation}
\begin{aligned}
\northenb{(\mora\functhen \morb)}{\gcq}    & = \northenb{\morb}{(\mora \northenbsymb \gcq)}, \\
\northena{\gcq}{(\morb\functhen \morc)}    & =\northena{(\northena{\gcq}{\morc})}{\morb}, \\
\northenb{\mora}{(\northena{\gcq}{\morc})} & =\northena{(\northenb{\mora}{\gcq})}{\morc}.
\end{aligned}
\end{equation}

*Conditions from the unitality diagrams for enriched categories
Consider the right-hand portion of the diagram (<ref>), now for the case of .

On the level of forward maps, this diagram encodes the condition that $\catid_\Obja\functhen \gca=\gca$ for any morphism $\gca \colon \Obja \mto \Objb$.
On the level of backward maps, it amounts to the commutative diagram

Computing the right-hand route, we have

\begin{equation}
\begin{aligned}
\gcmBdec{(\enidof{}{\Obja} \gcPlus \catid_{\homobject{}{\Obja}{\Objb}})}\colon \gcQ_{\Obja\Obja}^{\gcA_{\Obja\Objb}}\times \gcQ_{\Obja\Objb}^{\gcA_{\Obja\Obja}} & \to \singletonQ^{\gcA_{\Obja\Objb}}\times \gcQ_{\Obja\Objb}^{\singletonA} \\
\tupp{\varphi_{\Obja\Obja},\varphi_{\Obja\Objb}}                                                                                & \mapsto \tupp{!, \gcmF{\enidof{}{\Obja}}\functhen \varphi_{\Obja\Objb}\functhen \gcmB{\catid_{\homobject{}{\Obja}{\Objb}}}}=\tupp{!, \theonlyA \mapsto \varphi_{\Obja\Obja}(\catid_\Obja)},
\end{aligned}
\end{equation}

\begin{equation}
\begin{aligned}
\gcmBdec{((\enidof{}{\Obja} \gcPlus \catid_{\homobject{}{\Obja}{\Objb}})\functhen \enmof{}{\Obja}{\Obja}{\Objb})}\colon
\gcQ_{\Obja\Objb} & \to \gcQ_{\Obja\Obja}^{\gcA_{\Obja\Objb}}\times\gcQ_{\Obja\Objb}^{\gcA_{\Obja\Obja}}\to \singletonQ^{\gcA_{\Obja\Objb}}\times \gcQ_{\Obja\Objb}^{\singletonA} \\
\gcq              & \mapsto \gcmF{\enmof{}{\Obja}{\Obja}{\Objb}}(\gcq)=\tupp{\northena{\gcq}{(-)},\northenb{(-)}{\gcq}} \\
& \mapsto \tupp{\gcmF{\catid_{\homobject{}{\Obja}{\Objb}}}\functhen \northena{\gcq}{(-)} \functhen \gcmB{\enidof{}{\Obja}}, \gcmF{\enidof{}{\Obja}}\functhen \northenb{(-)}{\gcq}\functhen \gcmB{\catid_{\homobject{}{\Obja}{\Objb}}}} \\
& =\tupp{!,\theonlyA \mapsto (\northenb{\catid_\Obja}{\gcq})},
\end{aligned}
\end{equation}

which, when compared with $\gcmB{\leftunitor} \colon \gcq \mapsto \tupp{!, \theonlyA \mapsto \gcq} $, gives the condition

\begin{equation}
\northenb{\catid}{\gcq}=\gcq.
\end{equation}

The left-hand portion of the diagram (<ref>) may be treated analogously and gives rise the to the conditions

\begin{equation}
\gca\functhen \catid_\Objb=\gca
\qquad \text{and} \qquad
\northena{\gcq}{ \catid}=\gcq.
\end{equation}

Exact nategories are those in which the implications in (<ref>) and (<ref>) are in fact equivalences. In the above proof, this corresponds to the morphisms (<ref>) and (<ref>) in being identities.

(<ref>) begs the question as to why we don't include the additional properties stated there as part of our definition of what a nategory is. Our reason is that these properties fail for examples of interest to us.

For example, in applications it is normal that physical measurements and numerical representations on a computer are given only to a certain accuracy. This motivates (<ref>), where we only allow integer values for norphisms. However, in that example, the properties (<ref>) and (<ref>) are not satisfied. To see this, consider (<ref>)and consider morphisms $\morb$ and $\morc$ in $\Berg$ with $\lengthfun(\morb)=\lengthfun(\morc)=1.5$. For a norphism $\gcq$ of the appropriate signature we have

\begin{equation}
\northena{\gcq}{(\morb\functhen \morc)}=\thefloor{\gcq - \lengthfun(\morb \mthen \mora)}=\thefloor{\gcq-3}
\end{equation}

on the one hand, and

\begin{equation}
\northena{(\northena{\gcq}{\morc})}{\morb}=\thefloor{\thefloor{\gcq-1.5}-1.5}
\end{equation}

on the other. If we choose $\gcq=10$, for instance, the previous expressions evaluate to 7 and 6, respectively.

As a different example, the properties (<ref>) and (<ref>) fail in Example <ref>. Indeed, there $\northenb{\catid_\Obja}{\nora}=\emptyset$ and $\northena{\nora}{\catid_\Objb}=\emptyset$, even though, in general, we would have $\nora \neq \emptyset$.

§ CONCLUSIONS

This work showed that we can encode negative information in a categorical manner such that  norphisms (negative arrows) and morphisms (positive arrows) are equal citizens in the theory. Norphisms and morphisms are, in general, not mutually exclusive; they give complementary information.

We have seen how, in the category , norphisms can represent negative results such as lower bounds on distances between two locations.
A path planning algorithm must construct a morphism (a path) and construct a norphism (a bound) to prove that the path is optimal.
We have also seen how, in the category , norphisms can represent design impossibility results.

After defining nategories as categories with extra structure, we showed a way to encode this new concept using categories enriched in the dialecta category $\GSet$. This approach, however, introduces some compatibility properties for norphism composition that we do not wish to include in our general notion of nategory. Future work includes exploring if nategories might be recovered, on the nose, via a different enrichment, as well as studying various typical categorical concepts in the context of nategories. We would also be very happy to discover further interesting examples.

Future work includes:

* Surveying known categories for natural norphism structures.

* As suggested by a reviewer, defining the relation between $\prcat$ and $\CatSymbol{Poly}$.

* Understanding how the norphism structure generalizes to higher-level construction.
For example, what is the natural definition of a “nunctor” (a “negative” functor)?

§ ACKNOWLEDGMENTS

The authors would like to thank David I.
Spivak for fruitful discussions.
We also thank Valeria de Paiva, Brendan Fong, and David Yetter for helpful comments.
Gioele Zardini was supported by the Swiss National Science Foundation, under NCCR Automation, grant agreement 51NF40_180545.

[1]
authorAndreas Blass
(year1995): titleQuestions and answers—a
category arising in linear logic, complexity theory, and set theory.
journalAdvances in linear logic
volume222, pp. pages61–81,

[2]
authorAndrea Censi,
authorJonathan Lorand &
authorGioele Zardini
(year2022): titleApplied Compositional Thinking
for Engineers.
noteWork in progress book.

[3]
authorValeria De Paiva
(year1989): titleThe dialectica categories.
journalCategories in Computer Science and Logic
volume92, pp. pages47–62, 10.48456/tr-213.

[4]
authorValeria De Paiva
(year1989): titleA dialectica-like model of
linear logic.
In: booktitleCategory Theory and Computer Science,
organizationSpringer, pp. pages341–356, 10.1007/BFb0018360.

[5]
authorDaniel Delling,
authorPeter Sanders,
authorDominik Schultes &
authorDorothea Wagner
(year2009): titleEngineering route planning
In: booktitleAlgorithmics of large and complex
networks, publisherSpringer, pp. pages117–139,

[6]
authorBrendan Fong &
authorDavid I Spivak
(year2018): titleSeven sketches in
compositionality: An invitation to applied category theory.
journalarXiv preprint arXiv:1803.05316,

[7]
authorGregory Maxwell Kelly
(year1982): titleBasic concepts of enriched
category theory.
volume64, publisherCUP Archive.

[8]
authorMichael Shulman
(year2022): titleAffine logic for constructive
journalThe Bulletin of Symbolic Logic, pp.
pages1–51, 10.1017/bsl.2022.28.