# ChatFDA: Medical Records Risk Assessment

Minh Tran
Robotics Institute
Carnegie Mellon University
<EMAIL_ADDRESS>
&Charlie Sun
Language Technologies Institute
Carnegie Mellon University
<EMAIL_ADDRESS>

###### Abstract

In healthcare, the emphasis on patient safety and the minimization of medical
errors cannot be overstated. Despite concerted efforts, many healthcare
systems, especially in low-resource regions, still grapple with preventing
these errors effectively. This study explores a pioneering application aimed
at addressing this challenge by assisting caregivers in gauging potential
risks derived from medical notes. The application leverages data from openFDA,
delivering real-time, actionable insights regarding prescriptions. Preliminary
analyses conducted on the MIMIC-III [2] dataset affirm a proof of concept
highlighting a reduction in medical errors and an amplification in patient
safety. This tool holds promise for drastically enhancing healthcare outcomes
in settings with limited resources. To bolster reproducibility and foster
further research, the entire codebase underpinning our methodology is
accessible on Github.

##  1 Introduction

Every year in the United States alone, there are 250,000 deaths due to medical
errors. These can stem from diagnostic errors, surgeries, patient care
infections, and largely (44%) [3] from medications. This situation persists
even in a country with a well-developed healthcare system boasting advanced
medical facilities, meticulously organized and digitalized records. In low-
resource regions, especially in rural areas of developing countries, the
challenge of ensuring patient safety intensifies. There are regions where a
single nurse may be responsible for an entire village, and they might not have
access to standardized medical records. Sometimes, the records are merely
handwritten notes or even recollections from the patients themselves.

Knowing that eliminating medical records could save millions live per year, we
are motivated to create a tool to leverage the power of LLMs to assure the
safety for patients, especially for areas where ressources are limited. We
built an application that takes multimodalities medical records input from
text, voice, to image then extract/correct any mistake made by human. Based on
the medical history and prescription, we also provided risk assessment for
each case.

##  2 Related Works

###  2.1 Medical Records Correction

Medical record correction has been a focal point in healthcare informatics for
several years. Various studies have delved into the use of Electronic Health
Records (EHRs) to bolster the accuracy and reliability of medical data. In the
past, probabilistic models have been employed to identify and rectify
inconsistencies in medical records, especially in the realm of medication
prescriptions. Recently, large language models (like GPT-4 and PaLM) [4, 1]
have found applications in general error correction. However, benchmarks
specific to medical data remain nonexistent. These studies underscore the
paramount importance of precise medical record-keeping, an area our research
aspires to further by assessing risks based on these records.

###  2.2 Language Models for Medical Data

The infusion of language models into the medical domain is an emerging trend,
further propelled by the inception of advanced models such as Med-PaLM 2 and
Med-BERT [6, 5]. Such models have been harnessed for diverse tasks including
medical text summarization, diagnosis prediction, and drug interaction
identification. Yet, there’s a noticeable research gap on the efficacy of
leveraging LLMs to bolster patient safety, especially in multilingual contexts
with limited information. Our study seeks to fill this void by incorporating
language models to interpret and authenticate medical notes, especially in
environments where expert intervention is scarce. This section offers a
snapshot of potential research trajectories and applications of LLMs in
medical contexts.

Both of these domains—medical records correction and language models for
medical data—shed light on invaluable insights and foundational principles
that shape and bolster the ambitions of our research. By marrying elements
from these two realms, we endeavor to design an application with the potential
to markedly enhance patient safety and curtail medical errors in resource-
constrained settings.

##  3 Proposed Approach

###  3.1 Pipeline Design

Our application’s architecture is structured as a pipeline comprising several
interlinked modules:

  1. 1.

Data Collection Module: This initial module gathers and processes various
forms of medical data. While our inputs can range from text to voice and
images, we’ve specifically honed in on medical notes for this experiment due
to their reliability as a primary information source for caregivers.

  2. 2.

Data Standardization Module: Using the MIMIC-III dataset as a foundation, this
module standardizes the amassed data, ensuring its consistency and
compatibility for further analysis.

  3. 3.

Medical Records Processing Module with GPT-4: From the standardized data, this
module employs the GPT-4 model to segregate the medical records into two
distinct sections: prescriptions and medical history. This vital step not only
mitigates potential human errors during note-taking but also precisely
identifies each patient’s prescribed treatments.

  4. 4.

Prescription Analysis Module with openFDA: The prescription data is relayed to
openFDA, which subsequently offers actionable insights. This encompasses
potential medication interactions and pertinent treatment guidelines.

  5. 5.

Risk Evaluation and Record Storage Module: This concluding block synthesizes
the insights derived from openFDA with the patient’s medical history to
generate a comprehensive risk evaluation. Concurrently, it ensures the updated
medical records are safely stored in the database, facilitating future
retrievals and analyses.

Figure 1: Pipeline Diagram

###  3.2 Prompt Design

Designing a useful prompt for a language model is critical, especially in
high-stakes situations like medical evaluations. In this study, we introduce
two separate prompts:

  1. 1.

The first is to extract relevant medical information from a doctor’s notes.
This information pertains to a patient’s pre-existing conditions, symptoms,
and prescribed medications.

  2. 2.

The second prompt aims to assess the potential risks related to the extracted
medical information. In this section, we elaborate on our approach to
designing this risk-assessment prompt.

Prompt Structure: The risk assessment prompt comprises three primary sections:

  * •

Parsed Notes: This section integrates the parsed information from the doctor’s
notes.

  * •

Drug Information: Here, we incorporate drug interactions and warnings
retrieved from the FDA database.

  * •

Answer Section: The language model is tasked to analyze the prescribed
treatment, identifying potential drug interactions and assessing potential
patient reactions based on their pre-existing conditions. The culmination of
this analysis is the evaluation of the treatment’s dangerousness on a scale:
LOW, MEDIUM, or HIGH. An answer template is also provided to ensure
consistency in responses.

Actual Prompt:

    "I am a doctor, and I need you to evaluate my prescription:
    {parsed_notes}

    Drug contexts:
    {drug_info_string}

    Please answer the following in a concise point format, considering the provided drug context:
    - Possible interactions between the prescribed drugs?
    - Specific adverse effects of the drugs that relate to the patient’s pre-existing conditions
    and symptoms?

    Conclude your response by assessing the treatment’s dangerousness based on interactions and
    adverse effects specific to the patient. Categorize dangerousness as: LOW, MEDIUM, HIGH.

    Your answer should adhere to this format:
    * INTERACTIONS:
    - <interaction 1>
    - <interaction 2>
    - ...

    * ADVERSE EFFECTS:
    - <adverse effect 1>
    - <adverse effect 2>
    - ...

    * DANGEROUSNESS: <LOW / MEDIUM / HIGH>

    Include only necessary interactions or adverse effects in your response."

###  3.3 User Interface

The user interface of the application is intentionally designed to be
intuitive and user-friendly. It features a series of prompts that guide
healthcare workers through the verification process. Initially, users are
prompted to select their preferred method of input—image, voice, or text.
Based on this selection, the application provides an interface for capturing
the image, recording the voice, or typing the text. Once the data is processed
and analyzed, a summary report is displayed, and users are prompted to confirm
its accuracy. They are also prompted to review the actionable insights
generated from openFDA data, allowing for more informed decision-making.

By synergizing an efficient pipeline with user-friendly prompts, our proposed
approach aims to offer a robust and accessible application capable of
significantly reducing medical errors and improving patient safety,
particularly in low-resource settings.

##  4 Results Analsysis

We tested our application on a public sample of the MIMIC-III dataset that
contains de-identified health data associated with over 40,000 patients who
stayed in critical care units of the Beth Israel Deaconess Medical Center. For
this scope of this project, we only test on a small public sample, and focused
on medical notes only.

Figure 2: Processed Medical Notes

The results indicate that the our application is effective in verifying
medical notes, integrating real-time data for informed decision-making, and
improving the user experience for healthcare workers. Most importantly, the
application shows promise in its primary objective—reducing medical errors and
enhancing patient safety.

##  5 Limitation and Future directions

In this project, we introduce an application aimed at reducing medical errors
and enhancing patient safety, particularly in low-resource settings. We
demonstrate the app’s capability to verify medical notes and leverage openFDA
data for informed decision-making.

However, our work has limitations. The application’s effectiveness is
currently tested on a limited dataset, questioning its generalizability.
Additionally, the reliance on real-time data integration could pose challenges
in regions with poor internet connectivity. As well, the FDA drug info might
be too long for the LLM model due to the input token limit, which suggests
that a summary may be required when the list of drugs is long.

Future directions should focus on expanding the dataset for more robust
testing and exploring offline capabilities to make the application more
versatile. As well, there are models more specialized to medical texts, such
as Google’s Med-PaLM2, which is worth exploring once it becomes available.
Additionally, reinforcement learning with human feedback (RLHF) can be added,
in order to allow for model improvement based on doctor feedback, in the same
fashion as ChatGPT. This work serves as a stepping stone for leveraging
technology to reduce oversight in the judgement of healthcare professionals,
this would especially improve healthcare outcomes in resource-poor settings.

## References

  * [1] A. Chowdhery, S. Narang, J. Devlin, M. Bosma, G. Mishra, A. Roberts, P. Barham, H. W. Chung, C. Sutton, S. Gehrmann, P. Schuh, K. Shi, S. Tsvyashchenko, J. Maynez, A. Rao, P. Barnes, Y. Tay, N. Shazeer, V. Prabhakaran, E. Reif, N. Du, B. Hutchinson, R. Pope, J. Bradbury, J. Austin, M. Isard, G. Gur-Ari, P. Yin, T. Duke, A. Levskaya, S. Ghemawat, S. Dev, H. Michalewski, X. Garcia, V. Misra, K. Robinson, L. Fedus, D. Zhou, D. Ippolito, D. Luan, H. Lim, B. Zoph, A. Spiridonov, R. Sepassi, D. Dohan, S. Agrawal, M. Omernick, A. M. Dai, T. S. Pillai, M. Pellat, A. Lewkowycz, E. Moreira, R. Child, O. Polozov, K. Lee, Z. Zhou, X. Wang, B. Saeta, M. Diaz, O. Firat, M. Catasta, J. Wei, K. Meier-Hellstern, D. Eck, J. Dean, S. Petrov, and N. Fiedel.  Palm: Scaling language modeling with pathways, 2022.
  * [2] A. Johnson et al.  Mimic-iii clinical database, 2016.
  * [3] O. of Inspector General.  Adverse events in hospitals: A quarter of medicare patients experienced harm in october 2018, 2022.
  * [4] OpenAI.  Gpt-4 technical report, 2023.
  * [5] L. Rasmy, Y. Xiang, Z. Xie, C. Tao, and D. Zhi.  Med-bert: pre-trained contextualized embeddings on large-scale structured electronic health records for disease prediction, 2020.
  * [6] K. Singhal, T. Tu, J. Gottweis, R. Sayres, E. Wulczyn, L. Hou, K. Clark, S. Pfohl, H. Cole-Lewis, D. Neal, M. Schaekermann, A. Wang, M. Amin, S. Lachgar, P. Mansfield, S. Prakash, B. Green, E. Dominowska, B. A. y Arcas, N. Tomasev, Y. Liu, R. Wong, C. Semturs, S. S. Mahdavi, J. Barral, D. Webster, G. S. Corrado, Y. Matias, S. Azizi, A. Karthikesalingam, and V. Natarajan.  Towards expert-level medical question answering with large language models, 2023.


11institutetext: School of Informatics, University of Edinburgh, United
Kingdom,
11email: {chris.heunen<EMAIL_ADDRESS>
# Duoidally enriched Freyd categories††thanks: Jesse Sigal is partly funded by
Huawei.

Chris Heunen  0000-0001-7393-2640 Jesse Sigal  0000-0002-5117-8752

###### Abstract

Freyd categories provide a semantics for first-order effectful programming
languages by capturing the two different orders of evaluation for products. We
enrich Freyd categories in a duoidal category, which provides a new, third
choice of parallel composition. Duoidal categories have two monoidal
structures which account for the sequential and parallel compositions. The
traditional setting is recovered as a full coreflective subcategory for a
judicious choice of duoidal category. We give several worked examples of this
uniform framework, including the parameterised state monad, basic separation
semantics for resources, and interesting cases of change of enrichment.

###### Keywords:

Freyd category duoidal category Kleisli category Lawvere theory monad

##  1 Introduction

Computational effects encapsulate interactions of a computer program with its
environment in a modular way, and are a staple of modern programming languages
[17]. Originally captured by strong monads [15], they have been extended to
Arrows to deal with input as well as output [12], to Lawvere theories to
better combine effects algebraically [20], to PROs and PROPs to deal with non-
cartesian settings [13], and to Freyd categories to deal with effects that are
not higher-order [14].

Freyd categories let one compose effectful computations both in sequence and,
to some extent, in parallel, and reason about such compositions rigorously.
For an effectful computation $f\colon a\to b$, we may embed it, the domain,
and the codomain into a larger context by extending with $-\otimes c$ for any
object $c$ and monoidal-like operation $\otimes$, which we write as
$f\otimes\mathrm{id}\colon a\otimes c\to b\otimes c$. Intuitively,
$f\otimes\mathrm{id}$ does not interact with $c$. Effectful computations need
not commute as they may alter the environment:
$(f\otimes\mathrm{id}).(\mathrm{id}\otimes g)\neq(\mathrm{id}\otimes
g).(f\otimes\mathrm{id})$ in general.

But what if we want to track more data about computations than just types and
effects? For example, suppose we want to annotate every computation with its
resource needs: there could e.g. be a set $R$ of resources, and every
computation $f$ requires a certain subset $P\subseteq R$ of resources for it
to execute. Sequencing two computations needs all resources to execute both,
so if $f\colon a\to b$ and $g\colon b\to c$ require resources $P$ and $Q$
respectively, then $g.f$ requires $P\cup Q$. The same is true for parallel
composition: if $f_{1}\colon a_{1}\to b_{1}$ and $f_{2}\colon a_{2}\to b_{2}$
require $P_{1}$ and $P_{2}$ respectively, then $f_{1}\otimes f_{2}\colon
a_{1}\otimes a_{2}\to b_{1}\otimes b_{2}$ requires $P_{1}\cup P_{2}$. However,
it is often desirable to restrict $P_{1}$ and $P_{2}$ by requiring $P_{1}\cap
P_{2}=\emptyset$ so that morphisms composed in parallel use different
resources. If we have an identity map $\mathrm{id}\colon a\to a$ for all $a$
which requires $\emptyset\subseteq R$, then we can always form
$f\otimes\mathrm{id}$ for any $f$, but what of the general case?

This article proposes a solution that achieves just this: enrich Freyd
categories in duoidal categories. Duoidal categories carry two interacting
monoidal structures that will account for the sequential and parallel
composition of both the effectful computations and the extra data we want to
track, such as the resources above. We provide a concrete example for
resources in Section 3.1.

Section 2 introduces duoidally enriched Freyd categories. Section 3 shows the
breadth of such categories by treating disparate examples: separation
semantics for resources as above, indexed state monads, and Kleisli categories
of Lawvere theories. Section 4 shows that a judicious choice of duoidal
enriching category recovers traditional Freyd categories as a full
coreflective subcategory, and Section 5 gives an abstract characterisation of
duoidally enriched Freyd categories in purely algebraic terms. Section 6
considers changing the enriching duoidal category, accounting for e.g.
changing the underlying permission model in the example above. Section 7
concludes and suggests directions for future work.

##### Related work

Morrison and Penneys define a $\mathbf{V}$-monoidal category [16] for braided
monoidal $\mathbf{V}$ as a $\mathbf{V}$-category with parallel composition
that interacts well with the braid. In the case $\mathbf{V}$ is braided (and
thus duoidal), our definition of a $\mathbf{V}$-Freyd category is similar.
However, we also require bifunctorality of the hom objects, an important
difference for some of our constructions.

The abstract characterisation in Section 5 is inspired by Fujii’s
characterisation of PROs and PROPs [7] as monoids in
$\mathbf{MonCat_{lax}}\big{(}\mathbf{N}^{\mathrm{op}}\times\mathbf{N},\mathbf{Set}\big{)}$
and
$\mathbf{MonCat_{lax}}\big{(}\mathbf{P}^{\mathrm{op}}\times\mathbf{P},\mathbf{Set}\big{)}$
respectively, where $\mathbf{N}$ and $\mathbf{P}$ have natural numbers as
objects and equalities respectively bijections as morphisms.

Garner and López Franco describe a general framework for commutativity using
categories enriched in the sequential product of a duoidal category [8]. Their
framework requires the duoidal category to be _normal_ , meaning that the two
units are isomorphic. Only with this requirement and others do they define a
monoidal structure on their category of enriched categories, and do not define
a monoidal enriched category. We do not require normality.

Finally, Forcey [6], and Batanin and Markl [4] enrich over duoidal categories,
but using the parallel product instead. We choose to enrich over the
sequential product in order to define examples in which this is the
appropriate choice.

##  2 Duoidally enriched Freyd categories

This section introduces duoidally enriched Freyd categories (in Section 2.3),
but first we discuss Freyd categories (in Section 2.1) and duoidal categories
(in Section 2.2).

###  2.1 Freyd categories

Freyd categories provide semantics for first-order call-by-value programming
languages with effects [20]. We will generalise the definition of a Freyd
category slightly so that the effect free fragment need not have products,
beginning with the following preliminary definitions [14, 18].

###### Definition 1

A category $\mathbf{C}$ is _binoidal_ when it comes with endofunctors
$(-)\ltimes x$ and $x\rtimes(-)$ for each object $x$ such that $x\ltimes
y=x\rtimes y$ for all $y$; write $x\otimes y$ for this object. A morphism
$f\colon x\to y$ is _central_ if for any morphism $g\colon x^{\prime}\to
y^{\prime}$ the two maps $(y\rtimes g).(f\ltimes x^{\prime})$ and $(f\ltimes
y^{\prime}).(x\rtimes g)$ of type $x\otimes x^{\prime}\to y\otimes y^{\prime}$
are equal, as are the two maps $(y^{\prime}\rtimes f).(g\ltimes x)$ and
$(g\ltimes y).(x^{\prime}\rtimes f)$ of type $x^{\prime}\otimes x\to
y^{\prime}\otimes y$. Central morphisms form a wide subcategory
$Z(\mathbf{C})$ called the _centre_.

###### Definition 2

A binoidal category $\mathbf{C}$ is _premonoidal_ when equipped with an object
$e$ and families of central isomorphisms $\alpha\colon(x\otimes y)\otimes z\to
x\otimes(y\otimes z)$, $\lambda\colon e\otimes x\to x$, and $\rho\colon
x\otimes e\to x$ that are natural in each component and satisfy triangle and
pentagon equations.

###### Definition 3

A functor $F\colon\mathbf{C}\to\mathbf{D}$ between premonoidal categories is a
_premonoidal functor_ when equipped with central morphisms $\eta\colon
e_{\mathbf{D}}\to F\left(e_{\mathbf{C}}\right)$ and $\mu\colon
F(x)\otimes_{\mathbf{D}}F(y)\to F\left(x\otimes_{\mathbf{C}}y\right)$ such
that $\mu$ is natural in each component, and the following diagrams commute:

${{(F(x)\otimes_{\mathbf{D}}F(y))\otimes_{\mathbf{D}}F(z)}}$${{F(x)\otimes_{\mathbf{D}}(F(y)\otimes_{\mathbf{D}}F(z))}}$${{F(x\otimes_{\mathbf{C}}y)\otimes_{\mathbf{D}}F(z)}}$${{F(x)\otimes_{\mathbf{D}}F(y\otimes_{\mathbf{C}}z)}}$${{F((x\otimes_{\mathbf{C}}y)\otimes_{\mathbf{C}}z)}}$${{F(x\otimes_{\mathbf{C}}(y\otimes_{\mathbf{C}}z))}}$$\scriptstyle{\mu\otimes\mathrm{id}}$$\scriptstyle{\mu}$$\scriptstyle{F\alpha_{\mathbf{C}}}$$\scriptstyle{\alpha_{\mathbf{D}}}$$\scriptstyle{\mathrm{id}\otimes\mu}$$\scriptstyle{\mu}$
${{e_{\mathbf{D}}\otimes_{\mathbf{D}}F(x)}}$${{F(e_{\mathbf{C}})\otimes_{\mathbf{D}}F(x)}}$${{F(x)}}$${{F(e_{\mathbf{C}}\otimes_{\mathbf{C}}x)}}$${{F(x)\otimes_{\mathbf{D}}e_{\mathbf{D}}}}$${{F(x)\otimes_{\mathbf{D}}F(e_{\mathbf{C}})}}$${{F(x)}}$${{F(x\otimes_{\mathbf{C}}e_{\mathbf{C}})}}$$\scriptstyle{\lambda_{\mathbf{D}}}$$\scriptstyle{\eta\otimes\mathrm{id}}$$\scriptstyle{\mu}$$\scriptstyle{F\lambda_{\mathbf{C}}}$$\scriptstyle{\rho_{\mathbf{D}}}$$\scriptstyle{\mathrm{id}\otimes\eta}$$\scriptstyle{\mu}$$\scriptstyle{F\rho_{\mathbf{C}}}$

A premonoidal functor is _strong (strict)_ when $\eta$ and $\mu$ are
isomorphisms (identities).

Note that a strict premonoidal functor $F$ preserves associators and unitors
on the nose. Recall that a functor $F\colon\mathbf{C}\to\mathbf{D}$ between
monoidal categories is _lax monoidal_ when it comes with a morphism
$\eta\colon I\to F(I)$ and a natural transformation $\mu\colon F(X)\otimes
F(Y)\to F(X\otimes Y)$ satisfying coherence conditions. It is _strong
monoidal_ when $\eta$ and $\mu$ are invertible. Lax/strong monoidal functors
are closed under composition. Here now is our definition of a Freyd category.

###### Definition 4

A _Freyd category_ consists of a monoidal category $\mathbf{M}$ and a
premonoidal category $\mathbf{C}$ with the same objects, and an identity-on-
objects strict premonoidal functor $J\colon\mathbf{M}\to\mathbf{C}$ whose
image lies in $Z(\mathbf{C})$. A morphism $J\to J^{\prime}$ of Freyd
categories consists of a strong monoidal functor
$F_{0}\colon\mathbf{M}\to\mathbf{M}^{\prime}$ and a strong premonoidal functor
$F_{1}\colon\mathbf{C}\to\mathbf{C}^{\prime}$ such that
$F_{1}J=J^{\prime}F_{0}$. Freyd categories and their morphisms form a category
$\mathbf{Freyd}$.

###  2.2 Duoidal categories

A duoidal category carries two interacting monoidal structures, that one may
intuitively think of as sequential and parallel composition, but let us give
the definition [2, Definition 6.1] before examples.

###### Definition 5

A category $\mathbf{V}$ is _duoidal_ when it comes with two monoidal
structures $(\mathbf{V},*,J)$ and $(\mathbf{V},\circ,I)$, a natural
transformation $\zeta_{A,B,C,D}\colon(A\circ B)*(C\circ D)\to(A*C)\circ(B*D)$,
and three morphisms $\Delta\colon J\to J\circ J$, $\nabla\colon I*I\to I$, and
$\epsilon\colon J\to I$ such that $(I,\nabla,\epsilon)$ is a monoid in
$(\mathbf{V},*,J)$ and $(J,\Delta,\epsilon)$ is a comonoid in
$(\mathbf{V},\circ,I)$, and the following diagrams commute:

${{((A\circ B)*(C\circ D))*(E\circ F)}}$${{(A\circ B)*((C\circ D)*(E\circ
F))}}$${{((A*C)\circ(B*D))*(E\circ F)}}$${{(A\circ
B)*((C*E)\circ(D*F))}}$${{((A*C)*E)\circ((B*D)*F)}}$${{(A*(C*E))\circ(B*(D*F))}}$$\scriptstyle{\zeta*\mathrm{id}}$$\scriptstyle{\zeta}$$\scriptstyle{\alpha}$$\scriptstyle{\mathrm{id}*\zeta}$$\scriptstyle{\zeta}$$\scriptstyle{\alpha\circ\alpha}$${{J*(A\circ
B)}}$${{(J\circ J)*(A\circ B)}}$${{A\circ B}}$${{(J*A)\circ(J*B)}}$${{(A\circ
B)*J}}$${{(A\circ B)*(J\circ J)}}$${{A\circ
B}}$${{(A*J)\circ(B*J)}}$$\scriptstyle{\lambda}$$\scriptstyle{\Delta*\mathrm{id}}$$\scriptstyle{\zeta}$$\scriptstyle{\lambda\circ\lambda}$$\scriptstyle{\rho}$$\scriptstyle{\mathrm{id}*\Delta}$$\scriptstyle{\zeta}$$\scriptstyle{\rho\circ\rho}$
${{((A\circ B)\circ C)*((D\circ E)\circ F)}}$${{(A\circ(B\circ
C))*(D\circ(E\circ F))}}$${{((A\circ B)*(D\circ
E))\circ(C*F)}}$${{(A*D)\circ((B\circ C)*(E\circ
F))}}$${{((A*D)\circ(B*E))\circ(C*F)}}$${{(A*D)\circ((B*E)\circ(C*F))}}$$\scriptstyle{\zeta}$$\scriptstyle{\zeta\circ\mathrm{id}}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha*\alpha}$$\scriptstyle{\zeta}$$\scriptstyle{\mathrm{id}\circ\zeta}$${{I\circ(A*B)}}$${{(I*I)\circ(A*B)}}$${{A*B}}$${{(I\circ
A)*(I\circ B)}}$${{(A*B)\circ I}}$${{(A*B)\circ(I*I)}}$${{A*B}}$${{(A\circ
I)*(B\circ
I)}}$$\scriptstyle{\lambda}$$\scriptstyle{\nabla\circ\mathrm{id}}$$\scriptstyle{\zeta}$$\scriptstyle{\lambda*\lambda}$$\scriptstyle{\rho}$$\scriptstyle{\mathrm{id}\circ\nabla}$$\scriptstyle{\zeta}$$\scriptstyle{\rho*\rho}$

We may write $\left(\mathbf{V},*,J,\circ,I\right)$ or
$\left(\mathbf{V},*,\circ\right)$ to be explicit about the role of each
monoidal structure.

###### Example 1

Any braided monoidal category becomes duoidal by letting both monoidal
structures coincide and $\zeta$ be the middle-four interchange $x\otimes
y\otimes z\otimes w\allowbreak\to x\otimes z\otimes y\otimes w$ up to
associativity. In particular, any symmetric or cartesian monoidal category is
duoidal [2, Proposition 6.10, Example 6.19].

###### Example 2

If $\left(\mathbf{V},*,J,\circ,I\right)$ is duoidal, so is
$\left(\mathbf{V}^{\mathrm{op}},\circ,I,*,J\right)$, with opposite structure
maps [2, Section 6.1.2].

###### Example 3

If $\left(\mathbf{V},\otimes,I\right)$ is a monoidal category with products,
$\left(\mathbf{V},\otimes,I,\times,1\right)$ is duoidal with
$\zeta=\left\langle\pi_{1}\otimes\pi_{1},\pi_{2}\otimes\pi_{2}\right\rangle$,
$\Delta=\left\langle\mathrm{id},\mathrm{id}\right\rangle$, and $\nabla$ and
$\epsilon$ terminal maps. Similarly, if a monoidal category $\mathbf{V}$ has
coproducts, $\left(\mathbf{V},+,0,\otimes,I\right)$ is duoidal [2, Example
6.19].

###### Example 4

If $\left(\mathbf{V},*,J,\circ,I\right)$ is small and duoidal, straightforward
calculation shows Day convolution [5] of each monoidal structure makes the
category of presheaves
$([\mathbf{V}^{\mathrm{op}},\mathbf{Set}],*_{\mathrm{Day}},\mathbf{V}(-,J),\circ_{\mathrm{Day}},\mathbf{V}(-,I))$
again duoidal where

$\left(F*_{\mathrm{Day}}G\right)\left(A\right)=\int^{B,C}\mathbf{V}\left(A,B*C\right)\times
F\left(B\right)\times G\left(C\right)$

and likewise for $\circ_{\mathrm{Day}}$. An analogous construction holds for
$\left[\mathbf{V},\mathbf{Set}\right]$ by starting with
$\mathbf{V}^{\mathrm{op}}$.

###### Example 5

An endofunctor on $\mathbf{Set}$ is finitary when it preserves filtered
colimits and is therefore determined on finite sets. Finitary endofunctors are
closed under functor composition, $\circ$, with unit $\mathrm{Id}$; closed
under Day convolution with products, $\times_{\mathrm{Day}}$, with unit
$\mathbf{Set}\left(1,-\right)\cong\mathrm{Id}$; making
$\big{(}[\mathbf{Set},\mathbf{Set}]_{f},\times_{\mathrm{Day}},\mathrm{Id},\circ,\mathrm{Id}\big{)}$
a duoidal category. [8]

###### Example 6

For a small monoidal category $(\mathbf{M},\oplus,e)$, the category of
$\mathbf{Set}$-valued endoprofunctors
$\mathbf{Prof}(\mathbf{M})\coloneqq\left[\mathbf{M}^{\mathrm{op}}\\!\times\\!\mathbf{M},\mathbf{Set}\right]$
is duoidal $(\mathbf{Prof}(\mathbf{M}),\oplus_{\mathrm{Day}},\\!\diamond)$
with profunctor composition $(P\diamond Q)(a,c)\coloneqq\int^{b}P(a,b)\times
Q(b,c)$ (having unit $\mathbf{M}(-,-)$) and Day convolution of $\oplus$ on
both sides
$(P\oplus_{\mathrm{Day}}Q)(a,b)\coloneqq\int^{a_{1},a_{2},b_{2},b_{2}}\mathbf{M}(a,a_{1}\oplus
a_{2})\times\mathbf{M}(b_{1}\oplus b_{2},b)\times P(a_{1},b_{1})\times
Q(a_{2},b_{2})$ (having unit $\mathbf{M}(-,e)\times\mathbf{M}(e,-)$). [8]

###### Example 7

An important example for us is the category $\mathbf{Subset}$ of
_distinguished subsets_. Objects are pairs of sets $\left(X,A\right)$ such
that $X\subseteq A$ and morphisms $f\colon(X,A)\to(Y,B)$ are functions
$f\colon A\to B$ with $f(X)\subseteq Y$. We call $X$ the _distinguished
subset_. Composition and identities are as in $\mathbf{Set}$. We may suppress
the distinguished subset $X$ by writing $a\inplus A$ when $a\in X$. Next, we
give two monoidal structures on $\mathbf{Subset}$.

The first is the cartesian product: $(X,A)\times(Y,B)\coloneqq(X\times
Y,A\times B)$ on objects, and $f\times g$ as in $\mathbf{Set}$ on morphisms,
with unit $(1,1)$. Associators and unitors are as in $\mathbf{Set}$. This is
also a categorical product.

The second is the _disjunctive product_ : on objects $(X,A)\otimes(Y,B)$ is
defined as $\big{(}X\times Y,(A\times Y)\cup(X\times B)\big{)}$ with unit
$(1,1)$. We again have $f\times g$ on morphisms, which is well-defined.
Finally, the coherence maps are restricted versions of those for the cartesian
product.

Now $\big{(}\mathbf{Subset},\otimes,(1,1),\times,(1,1)\big{)}$ is duoidal by
Example 3: $\Delta$ and $\nabla$ are unitors, $\epsilon$ is the identity, and
$\zeta\colon\big{(}(X,A)\times(Y,B)\big{)}\otimes\big{(}(Z,C)\times(W,D)\big{)}\to\big{(}(X,A)\otimes(Z,C)\big{)}\times\big{(}(Y,B)\otimes(W,D)\big{)}$
is the restricted middle-four interchange; all axioms are inherited from
$(\mathbf{Set},\times,1)$ via Example 1.

The important difference between
$\big{(}\mathbf{Subset},\otimes,\times\big{)}$ and
$(\mathbf{Set},\times,\times)$ is that $\zeta$ is not invertible in the former
(as it is not surjective as a $\mathbf{Set}$ map). This allows Freyd
categories enriched in $\mathbf{Subset}$ a premonoidal-like structure.

###  2.3 Concrete definition

We are now ready for the titular notion of this paper. We first give a
concrete definition, leaving an abstract characterisation to Section 5.

###### Definition 6

Let $\left(\mathbf{V},*,J,\circ,I\right)$ be a duoidal category and
$(\mathbf{M},\oplus,e)$ a monoidal category. A _$\mathbf{V}$ -Freyd category
over $\mathbf{M}$_ consists of

  * •

a bifunctor
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{V}$

  * •

an extranatural family $\mathsf{idt}\colon I\to\mathbf{C}(a,a)$, meaning
$\mathbf{C}(\mathrm{id},f).\mathsf{idt}=\mathbf{C}(f,\mathrm{id}).\mathsf{idt}$

  * •

an extranatural family
$\mathsf{seq}\colon\mathbf{C}(a,b)\circ\mathbf{C}(b,c)\to\mathbf{C}(a,c)$,
meaning $\mathsf{seq}$ is natural in $a$ and $c$, and
$\mathsf{seq}.(\mathrm{id}\circ\mathbf{C}(f,\mathrm{id}))=\mathsf{seq}.(\mathbf{C}(\mathrm{id},f)\circ\mathrm{id})$

  * •

a morphism $\mathsf{zero}\colon J\to\mathbf{C}(e,e)$

  * •

a natural family
$\mathsf{par}\colon\mathbf{C}(a_{1},b_{1})*\mathbf{C}(a_{2},b_{2})\to\mathbf{C}(a_{1}\oplus
a_{2},b_{1}\oplus b_{2})$

satisfying the following axioms:

  1. (i)

$\mathsf{idt}$ is the identity for $\mathsf{seq}$, that is,
$\mathsf{seq}.(\mathsf{idt}\circ\mathrm{id})=\lambda$ and symmetrically;

  2. (ii)

$\mathsf{seq}$ is associative, that is,
$\mathsf{seq}.(\mathsf{seq}\circ\mathrm{id})=\mathsf{seq}.(\mathrm{id}\circ\mathsf{seq}).\alpha$;

  3. (iii)

$\mathsf{zero}$ is the identity for $\mathsf{par}$, that is,
$\mathbf{C}(\lambda^{-1},\lambda).\mathsf{par}.(\mathsf{zero}*\mathrm{id})=\lambda$
and symmetrically;

  4. (iv)

$\mathsf{par}$ is associative, that is,
$\mathbf{C}(\alpha^{-1},\alpha).\mathsf{par}.(\mathsf{par}*\mathrm{id})=\mathsf{par}.(\mathrm{id}*\mathsf{par}).\alpha$;

  5. (v)

$\mathsf{idt}$ respects $\mathsf{zero}$ via
$\mathsf{idt}.\epsilon=\mathsf{zero}$;

  6. (vi)

$\mathsf{idt}$ respects $\mathsf{par}$ via
$\mathsf{idt}.\nabla=\mathsf{par}.(\mathsf{idt}*\mathsf{idt})$;

  7. (vii)

$\mathsf{seq}$ respects $\mathsf{zero}$ via
$\mathsf{seq}.(\mathsf{zero}\circ\mathsf{zero}).\Delta=\mathsf{zero}$;

  8. (viii)

$\mathsf{seq}$ respects $\mathsf{par}$ via
$\mathsf{seq}.(\mathsf{par}\circ\mathsf{par}).\zeta=\mathsf{par}.(\mathsf{seq}*\mathsf{seq})\text{.}$

See Appendix 0.A for diagrams expressing the axioms.

###### Definition 7

A _morphism of $\mathbf{V}$-Freyd categories_ consists of a strong monoidal
functor $F_{0}\colon\mathbf{M}\to\mathbf{M}^{\prime}$ and a natural
transformation
$F_{1}\colon\mathbf{C}(a,b)\to\mathbf{C}^{\prime}\left(F_{0}a,F_{0}b\right)$
satisfying:

  * •

$F_{1}.\mathsf{idt}=\mathsf{idt}^{\prime}$;

  * •

$F_{1}.\mathsf{seq}=\mathsf{seq}^{\prime}.\left(F_{1}\circ F_{1}\right)$;

  * •

$\mathbf{C}^{\prime}\left(\mathrm{id},\mu\right).\mathsf{par}^{\prime}.\left(F_{1}*F_{1}\right)=\mathbf{C}^{\prime}\left(\mu,\mathrm{id}\right).F_{1}.\mathsf{par}$.

$\mathbf{V}$-Freyd categories and morphisms between them form a category
$\mathbf{V}\text{-}\mathbf{Freyd}$.

Our definition differs from the duoidally enriched categories of Batanin and
Markl [4] in a few important ways. They use $*$ for sequencing and $\circ$ for
parallel composition. Their analogues to items v, vi, vii and viii are
$\mathsf{idt}=\mathsf{zero}.\epsilon$,
$\mathsf{idt}=\mathsf{par}.(\mathsf{idt}\circ\mathsf{idt}).\Delta$,
$\mathsf{seq}.(\mathsf{zero}*\mathsf{zero})=\mathsf{zero}.\nabla$, and
$\mathsf{seq}.(\mathsf{par}*\mathsf{par})=\mathsf{par}.(\mathsf{seq}\circ\mathsf{seq}).\zeta\text{.}$
Additionally, their monoidal structure is more enriched while we inherit ours
from a $\mathbf{Set}$-category, namely $\mathbf{M}$. Thus, we believe both
notions are not inter-expressible.

##  3 Examples

This section works out three applications of duoidally enriched Freyd
categories: resource management (in Section 3.1), indexed state (in Section
3.2), and Kleisli categories of Lawvere theories (in Section 3.3).

###  3.1 Stateful functions and separated monoids

To deal with resources abstractly, we first introduce the novel notion of a
separated monoid.

###### Definition 8

A monoid $(M,\bullet,e)$ is _separated_ when it comes with a binary relation
$\|$ such that: $e\|m$ and $m\|e$; and $mm^{\prime}\|n$ iff $m\|n$ and
$m^{\prime}\|n$; and $m\|nn^{\prime}$ iff $m\|n$ and $m\|n^{\prime}$.

Examples include $(\mathbb{N},+,0)$ with $x\|y$ iff $x=0$ or $y=0$; finite
subsets $(\mathcal{P}_{f}(R),\cup,\emptyset)$ of a fixed set $R$, with $P\|Q$
iff $P\cap Q=\emptyset$; and products of separated monoids under pointwise
separation. Separated monoids parametrise duoidal categories of resources as
follows.

###### Definition 9

Let $(M,\|)$ be a separated monoid. The category $\mathbf{Label}_{M}$ of _$M$
-labelled sets_ has as objects functions $\ell\colon A\to M$ and as morphisms
functions $f\colon A\to A^{\prime}$ with $\ell^{\prime}f=\ell$. This category
has a monoidal structure $\bullet$ as follows: on objects,
$\ell\bullet\ell^{\prime}\colon A\times A^{\prime}\to M$ sends
$(a,a^{\prime})$ to $\ell(a)\bullet\ell^{\prime}(a^{\prime})$; on morphisms,
$f\bullet f^{\prime}=f\times f^{\prime}$; the unit $\mathsf{cst}_{e}\colon
1\to M$ picks out $e\in M$. There is a second monoidal structure $\|$ as
follows: on objects, $\ell\|\ell^{\prime}$ is the restriction of
$\ell\bullet\ell^{\prime}$ to
$\\{(a,a^{\prime})\mid\ell(a)\|\ell^{\prime}(a^{\prime})\\}$; on morphisms,
$f\|f^{\prime}=f\times f^{\prime}$. The category
$\left(\mathbf{Label}_{M},\|,\mathsf{cst}_{e},\bullet,\mathsf{cst}_{e}\right)$
is duoidal with
$\zeta\colon\left(\ell_{1}\bullet\ell^{\prime}_{1}\right)\|\left(\ell_{2}\bullet\ell^{\prime}_{2}\right)\to\left(\ell_{1}\|\ell_{2}\right)\bullet\left(\ell^{\prime}_{1}\|\ell^{\prime}_{2}\right)$
the restricted version of the $\zeta$ for
$\left(\mathbf{Set},\times,1,\times,1\right)$.

Think of objects in $\mathbf{Label}_{M}$ as sets of elements labelled with
their resource needs. The multiplication of $M$ combines resources, and the
separation $\|$ relates non-conflicting resources. We will now describe an
enriched Freyd category where morphisms are labelled by resources as in the
introduction.

Fix a countable family $R=\\{x,y,z,\ldots\\}$ of sets which we think of as
resources. The set $\mathcal{P}_{f}(R)$ of finite subsets of $R$ is a monoid
under union, and becomes a separated monoid under disjointness. For set of
resources $Q\in\mathcal{P}_{f}(R)$, fix a product of sets $\Pi_{x\in
Q}x\eqqcolon\Pi_{Q}$ which thus combines the resources in $Q$. Write
$\pi_{Q^{\prime}}\colon\Pi_{Q}\to\Pi_{Q^{\prime}}$ for the projection if
$Q^{\prime}\subseteq Q$, and given a map $f\colon a\times\Pi_{Q^{\prime}}\to
b\times\Pi_{Q^{\prime}}$ for sets $a$ and $b$, write $f_{Q^{\prime}}^{Q}$ for
the map $a\times\Pi_{Q}\to b\times\Pi_{Q}$ induced by $f$ when
$Q^{\prime}\subseteq Q$ which leaves the extra resources $Q\setminus
Q^{\prime}$ unchanged.

We will define a $\mathbf{Label}_{\mathcal{P}_{f}(R)}$-Freyd category over
$\mathbf{Set}$ of state-transforming functions. Let $\mathbf{C}(a,b)$ be the
function from the disjoint union of
$\mathbf{Set}(a\times\Pi_{Q},b\times\Pi_{Q})$ over $Q\in\mathcal{P}_{f}(R)$ to
$\mathcal{P}_{f}(R)$, that sends $f\colon a\times\Pi_{Q}\to b\times\Pi_{Q}$ to
$Q$. Thus, a map $f\in\mathbf{C}(a,b)$ with label $Q$ is an effectful
computation from $a$ to $b$ which can effect only resources in $Q$. This
becomes a bifunctor under pre- and post-composition. Writing $\cup$ for
$\bullet$ and $\cap$ for $\|$ for the sake of concreteness, the structure maps
are:

$\displaystyle\mathsf{idt}\colon\mathsf{cst}_{\emptyset}$
$\displaystyle\to\mathbf{C}(a,a)$
$\displaystyle\mathsf{zero}\colon\mathsf{cst}_{\emptyset}$
$\displaystyle\to\mathbf{C}(1,1)$ $\displaystyle\star$
$\displaystyle\mapsto(\emptyset,\mathrm{id}{}_{a\times 1})$
$\displaystyle\star$ $\displaystyle\mapsto(\emptyset,\mathrm{id}{})$
$\displaystyle\mathsf{seq}\colon\mathbf{C}(a,b)\cup\mathbf{C}(b,c)$
$\displaystyle\to\mathbf{C}(a,c)$ $\displaystyle\left((P,f),(Q,g)\right)$
$\displaystyle\mapsto\left(P\cup Q,g_{Q}^{P\cup Q}.f_{P}^{P\cup Q}\right)$
$\displaystyle\mathsf{par}\colon\mathbf{C}(a,b)\cap\mathbf{C}(a^{\prime},b^{\prime})$
$\displaystyle\to\mathbf{C}(a\times a^{\prime},b\times b^{\prime})$
$\displaystyle((Q,f),(Q^{\prime},f^{\prime}))$ $\displaystyle\mapsto$
$\displaystyle\left(Q\cup
Q^{\prime},\left(\mathrm{id}\times\left\langle\pi_{Q},\pi_{Q^{\prime}}\right\rangle^{-1}\right)m^{-1}.(f\times
f^{\prime}).m.\left(\mathrm{id}\times\left\langle\pi_{Q},\pi_{Q^{\prime}}\right\rangle\right)\right)$

where $\left\langle\pi_{Q},\pi_{Q^{\prime}}\right\rangle\colon\Pi_{Q\cup
Q^{\prime}}\to\Pi_{Q}\times\Pi_{Q^{\prime}}$ is invertible because $Q\cap
Q^{\prime}=\emptyset$ and $m$ is middle-four interchange. So $\mathsf{par}$
places maps in parallel up to rearranging state.

###  3.2 Indexed state

An important computational effect is global state. However, it is often
inflexible as the type of storage remains constant over time. In this example
the type can vary. We use the duoidal category of finitary endofunctors on
$\mathbf{Set}$ of Example 5 to give a
$\left[\mathbf{Set},\mathbf{Set}\right]_{f}$-Freyd category over
$\mathbf{Set}$ based on the state monad $(s\times(-))^{s}$, extending Atkey’s
example [3]. Define $\mathbf{C}(a,b)=(b\times(-))^{a}$, which is a bifunctor
via pre- and post-composition. The natural structure maps are:

$\displaystyle\mathsf{idt}_{X}\colon X$ $\displaystyle\to\left(a\times
X\right)^{a}$ $\displaystyle\mathsf{zero}_{X}\colon X$
$\displaystyle\to\left(1\times X\right)^{1}$ $\displaystyle x$
$\displaystyle\mapsto\lambda a.(x,a)$ $\displaystyle x$
$\displaystyle\mapsto\lambda\star.(x,\star)$
$\displaystyle\mathsf{seq}_{X}\colon\left(b\times\left(\left(c\times
X\right)^{b}\right)\right)^{a}$ $\displaystyle\to\left(c\times X\right)^{a}$
$\displaystyle f$ $\displaystyle\mapsto\mathrm{eval}.f$
$\displaystyle\mathsf{par}_{X}\colon\textstyle\int^{Y,Z}X^{Y\times
Z}\times\left(b\times Y\right)^{a}\times\left(c\times Z\right)^{a^{\prime}}$
$\displaystyle\to((b\times c)\times X)^{a\times a^{\prime}}$
$\displaystyle(k,f,g)$ $\displaystyle\mapsto(\mathrm{id}\times k).m.(f\times
g)$

where $\mathrm{eval}\colon b\times\left(c\times X\right)^{b}\to c\times X$ is
the evaluation map and $m$ is the middle-four interchange. $\mathsf{idt}$ and
$\mathsf{seq}$ are the unit and multiplication of a state monad but with
varying types of state.

###  3.3 Kleisli categories of Lawvere theories

Lawvere theories model effectful computations. Functional programmers might be
more familiar with Kleisli categories of monads, to which they are closely
related. Here we describe an indexed version, which models independent effects
in parallel. Let $\mathbf{Law}$ be the category of Lawvere theories. Its
initial object is the theory $\mathcal{S}$ of sets, the unit for the _tensor
product_ $\otimes$ of Lawvere theories [10]. This makes $\mathbf{Law}$ a
symmetric monoidal category, with the special property that there exist
inclusion maps
$\phi_{i}\colon\mathcal{L}_{i}\to\mathcal{L}_{1}\otimes\mathcal{L}_{2}$. Thus
the functor category $\left[\mathbf{Law},\mathbf{Set}\right]$ is monoidal
under Day convolution with unit the constant functor
$\mathbf{Law}(\mathcal{S},-)\simeq\mathbb{1}$. As this category also has
products, Example 3 makes it duoidal.

Now, $\mathbf{Law}$ is equivalent to the category of finitary monads [1,
Chapter 3]: any Lawvere theory $\mathcal{L}$ induces a monad $T(\mathcal{L})$,
and any map $\theta$ of Lawvere theories induces a monad morphism $T(\theta)$.
Every monad $T$ on $\mathbf{Set}$ is canonically bistrong: there are maps
$\mathrm{st}_{T}\colon a\times Tb\to T(a\times b)$ and
$\mathrm{st^{\prime}}_{T}\colon Ta\times b\to T(a\times b)$ making the two
induced maps $(a\times Tb)\times c\to T((a\times b)\times c)$ equal. Each
monad morphism $T(\theta)$ preserves strength: $T(\theta)_{a\times
b}.\mathrm{st}_{T(\mathcal{L})}=\mathrm{st}_{T(\mathcal{L}^{\prime})}.(\mathrm{id}\times
T(\theta)_{b})$.

We now show a $[\mathbf{Law},\mathbf{Set}]$-Freyd category over $\mathbf{Set}$
given by the Kleisli construction on Lawvere theories. Define on objects
$\mathbf{C}(a,b)=T(-)(b)^{a}$, and on morphisms
$\mathbf{C}(f,g)\colon\mathbf{C}(a,b)\Rightarrow\mathbf{C}(a^{\prime},b^{\prime})$
by $\mathbf{C}(f,g)_{\mathcal{L}}(k)=T(\mathcal{L})(g).k.f$, finally:

$\displaystyle\mathsf{idt}_{\mathcal{L}}\colon 1$ $\displaystyle\to
T(\mathcal{L})(a)^{a}$ $\displaystyle\mathsf{zero}_{\mathcal{L}}\colon 1$
$\displaystyle\to T(\mathcal{L})(1)^{1}$ $\displaystyle\star$
$\displaystyle\mapsto\eta$ $\displaystyle\star$ $\displaystyle\mapsto\eta$
$\displaystyle\mathsf{seq}_{\mathcal{L}}\colon T(\mathcal{L})(b)^{a}\times
T(\mathcal{L})(c)^{b}$ $\displaystyle\to T(\mathcal{L})(c)^{a}$
$\displaystyle(f,g)$ $\displaystyle\mapsto\mu.T(\mathcal{L})g.f$
$\displaystyle\mathsf{par}_{\mathcal{L}}\colon\textstyle\int^{\mathcal{L}_{1},\mathcal{L}_{2}}\mathbf{Law}(\mathcal{L}_{1}\\!\otimes\\!\mathcal{L}_{2},\mathcal{L})\\!\times\\!T(\mathcal{L}_{1})(b_{1})^{a_{1}}\\!\times\\!T(\mathcal{L}_{2})(b_{2})^{a_{2}}\to
T(\mathcal{L})(b_{1}\\!\times\\!b_{2})^{a_{1}\times a_{2}}$
$\displaystyle\left(\theta,f_{1},f_{2}\right)\mapsto
T(\theta).\mu.T(\mathcal{L}_{1}\otimes\mathcal{L}_{2})(\mathrm{st^{\prime}}).\mathrm{st}.\left(T(\phi_{1})\times
T(\phi_{2})\right).\left(f_{1}\times f_{2}\right)$

Intuitively, $\mathsf{par}$ lets us put Kleisli maps in parallel as long as
their effects are forced to commute (by $\otimes$). So
$\mathsf{idt}_{\mathcal{L}}$ and $\mathsf{seq}_{\mathcal{L}}$ are the identity
and composition for the Kleisli category of $T(\mathcal{L})$. The definition
of $\mathsf{par}_{\mathcal{L}}$ seems noncanonical because of the use of
$T(\mathcal{L}_{1}\otimes\mathcal{L}_{2})(\mathrm{st^{\prime}}).\mathrm{st}$,
but it is not:
$\mu.T(\mathcal{L}_{1}\otimes\mathcal{L}_{2})(\mathrm{st^{\prime}}).\mathrm{st}.\left(T(\phi_{1})\times
T(\phi_{2})\right)$ and
$\mu.T(\mathcal{L}_{1}\otimes\mathcal{L}_{2})(\mathrm{st}).\mathrm{st^{\prime}}.\left(T(\phi_{1})\times
T(\phi_{2})\right)$ are equal by definition of
$\mathcal{L}_{1}\otimes\mathcal{L}_{2}$.

##  4 Adjunction between $\mathbf{Subset}\text{-}\mathbf{Freyd}$ and
$\mathbf{Freyd}$

Now let us explain how $\mathbf{V}$-Freyd categories generalise Freyd
categories. Our approach is similar to Power’s [19] in that we work with
$\mathbf{Subset}$-enriched categories. Take $\mathbf{V}=\mathbf{Subset}$ and
consider a $\mathbf{Subset}$-Freyd category
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{Subset}$;
it comes equipped with a premonoidal-like structure via $\mathsf{par}$ and
$\mathsf{idt}$. We call a morphism $f\inplus\mathbf{C}(a,b)$ which is a member
of the distinguished subset a _distinguished morphism_. We will show they are
central in the premonoidal sense.

First observe that $\mathsf{idt}\colon\left(1,1\right)\to\mathbf{C}(a,a)$ is a
$\mathbf{Subset}$ morphism, so $\mathsf{idt}(\star)\inplus\mathbf{C}(a,a)$ is
distinguished. Thus, for $g\in\mathbf{C}(a^{\prime},b^{\prime})$ we find
$\big{(}\mathsf{idt}(\star),g\big{)}\in\mathbf{C}\left(a,a\right)\otimes\mathbf{C}(a^{\prime},b^{\prime})$
by definition of $\otimes$. Hence the pair is in the domain of $\mathsf{par}$,
giving $\mathsf{par}\big{(}\mathsf{idt}(\star),g\big{)}\in\mathbf{C}(a\oplus
a^{\prime},a\oplus b^{\prime})$ which we denote by $a\rtimes_{\mathsf{par}}g$.
Similarly, for any $f\in\mathbf{C}(a,b)$ we have
$f\ltimes_{\mathsf{par}}b^{\prime}\in\mathbf{C}(a\oplus b^{\prime},b\oplus
b^{\prime})$. We may also construct $f\ltimes_{\mathsf{par}}a^{\prime}$ and
$b\rtimes_{\mathsf{par}}g$. Hence it makes sense to ask if
$\mathsf{seq}(a\rtimes_{\mathsf{par}}g,f\ltimes_{\mathsf{par}}b^{\prime})=\mathsf{seq}(f\ltimes_{\mathsf{par}}a^{\prime},b\rtimes_{\mathsf{par}}g)$,
and if this equation (and its mirrored version by placing $g$ on the left)
holds for all $f$, we call $g$ _central_ in analogy to the binoidal case from
Definition 1.

Next we claim that distinguished morphisms
$g\inplus\mathbf{C}(a^{\prime},b^{\prime})$ are central. Note that
$\big{(}\mathsf{idt}(\star),g\big{)}\inplus\mathbf{C}(a^{\prime},a^{\prime})\times\mathbf{C}(a^{\prime},b^{\prime})$
and
$\big{(}g,\mathsf{idt}(\star)\big{)}\inplus\mathbf{C}(a^{\prime},b^{\prime})\times\mathbf{C}(b^{\prime},b^{\prime})$
are distinguished and in the domain of $\mathsf{seq}$. For any
$f\in\mathbf{C}(a,b)$, we have
$\big{(}(\mathsf{idt}(\star),f),(g,\mathsf{idt}(\star))\big{)}\in\big{(}\mathbf{C}(a,a)\times\mathbf{C}(a,b)\big{)}\otimes\big{(}\mathbf{C}(a^{\prime},b^{\prime})\times\mathbf{C}(b^{\prime},b^{\prime})\big{)}$
and similarly
$\big{(}(f,\mathsf{idt}(\star)),(\mathsf{idt}(\star)),g\big{)}\in\big{(}\mathbf{C}(a,b)\times\mathbf{C}(b,b)\big{)}\otimes\big{(}\mathbf{C}(a^{\prime},a^{\prime})\times\mathbf{C}(a^{\prime},b^{\prime})\big{)}$
by definition of $\otimes$ and are thus in the domain of
$\mathsf{seq}\otimes\mathsf{seq}$. We now apply
$\mathsf{par}.(\mathsf{seq}\otimes\mathsf{seq})$ to each pair and find they
equal $\mathsf{par}\left(f,g\right)$. Item viii states
$\mathsf{par}.(\mathsf{seq}\otimes\mathsf{seq})=\mathsf{seq}.(\mathsf{par}\times\mathsf{par}).\zeta$
and therefore
$\mathsf{seq}(a\rtimes_{\mathsf{par}}g,f\ltimes_{\mathsf{par}}b^{\prime})=\mathsf{par}(f,g)=\mathsf{seq}(f\ltimes_{\mathsf{par}}a^{\prime},b\rtimes_{\mathsf{par}}g)$
(and the mirrored equation analogously), so $g$ is central.

Distinguished morphisms have their centrality preserved by
$\mathbf{Subset}$-Freyd maps as they are mapped to distinguished morphisms,
but central morphisms need not be distinguished. Thus, Definition 7 ensures
that membership in the distinguished subset is preserved by
$\mathbf{Subset}$-Freyd maps, so centrality of distinguished morphisms of
$\mathbf{C}$ is preserved by all maps. Furthermore, bifunctorality of
$\mathbf{C}$ ensures that for all $f\in\mathbf{M}\left(a,b\right)$,
$\mathbf{C}\left(\mathrm{id},f\right)\left(\mathsf{idt}\left(\star\right)\right)\inplus\mathbf{C}(a,b)$,
and so the image of $\mathbf{M}$ is central and this centrality is preserved.
The same is true for a Freyd category $J\colon\mathbf{M}\to\mathbf{C}$, the
image of $\mathbf{M}$ under $J$ is central and this centrality is preserved by
all morphisms of Freyd categories. This preservation requirement is the
difference between Freyd categories and $\mathbf{Subset}$-Freyd categories:
the latter can require more central morphisms than the image of $\mathbf{M}$
to have centrality preserved. The rest of this subsection proves that there is
an adjunction between $\mathbf{Freyd}$ and
$\mathbf{Subset}\text{-}\mathbf{Freyd}$. The left adjoint
$\mathfrak{F}\colon\mathbf{Freyd}\to\mathbf{Subset}\text{-}\mathbf{Freyd}$ is
a free functor that only requires the image of $\mathbf{M}$ to be preserved.
The right adjoint
$\mathfrak{U}\colon\mathbf{Subset}\text{-}\mathbf{Freyd}\to\mathbf{Freyd}$
forgets the extra distinguished central morphisms.

###### Proposition 1

There is a functor
$\mathfrak{F}\colon\mathbf{Freyd}\to\mathbf{Subset}\text{-}\mathbf{Freyd}$
defined on objects as
$\mathfrak{F}(\mathbf{C})(a,b)=\big{(}J(\mathbf{M}(a,b)),\mathbf{C}(a,b)\big{)}$
and $\mathfrak{F}(\mathbf{C})(f,g)=\mathbf{C}(Jf,Jg)$.

######  Proof (Proof sketch)

$\mathfrak{F}(\mathbf{C})$ is well-defined on morphisms because $J$ is
identity-on-objects, and it is bifunctorial by bifunctorality of hom and
functorality of $J$. The structure maps are:

  * •

$\mathsf{idt}\colon(1,1)\to\mathfrak{F}(\mathbf{C})(a,a)$ is
$*\mapsto\mathrm{id}$;

  * •

$\mathsf{seq}\colon\mathfrak{F}(\mathbf{C})(a,b)\times\mathfrak{F}(\mathbf{C})(b,c)\to\mathfrak{F}(\mathbf{C})(a,c)$
is $(f,g)\mapsto g.f$;

  * •

$\mathsf{zero}\colon(1,1)\to\mathfrak{F}(\mathbf{C})(e,e)$ is
$*\mapsto\mathrm{id}$;

  * •

$\mathsf{par}\colon\mathfrak{F}(\mathbf{C})(a_{1},b_{1})\otimes\mathfrak{F}(\mathbf{C})(a_{2},b_{2})\to\mathfrak{F}(\mathbf{C})(a_{1}\oplus
a_{2},b_{1}\oplus b_{2})$ is $(f_{1},f_{2})\mapsto f_{1}\otimes f_{2}$; this
is well-defined whether $(f_{1},f_{2})$ is in
$J(\mathbf{M}(a_{1},b_{1}))\times\mathbf{C}(a_{2},b_{2})$ or is in
$\mathbf{C}(a_{1},b_{1})\times J(\mathbf{M}(a_{2},b_{2}))$ as $J$ preserves
centrality of $\mathbf{M}=Z(\mathbf{M})$.

The (extra)naturality of the structure maps comes from the extranaturality of
composition, functorality of $\mathbf{M}$’s monoidal product, and $J$ being a
strict premonoidal functor preserving centrality. Items i and ii are true by
$\mathbf{C}$’s composition, items iv and iii follow from the strict
premonoidality of $J$ and the naturality of unitors and associators, and items
v and vii are trivial. Finally, items vi and viii follow from $\mathbf{C}$’s
premonoidal structure.

Finally, it is easy to check that $\mathfrak{F}(F)=F$ is well-defined and
functorial.

###### Proposition 2

There is a functor
$\mathfrak{U}\colon\mathbf{Subset}\text{-}\mathbf{Freyd}\to\mathbf{Freyd}$
that sends an object
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{Subset}$
to the functor $J\colon\mathbf{M}\to\mathfrak{U}(\mathbf{C})$ defined as
follows:

  * •

the category $\mathfrak{U}(\mathbf{C})$ has the same objects as $\mathbf{M}$
but homsets $\mathfrak{U}(\mathbf{C})(a,b)=A$ where
$(X,A)\coloneqq\mathbf{C}(a,b)$, with composition $g.f=\mathsf{seq}(f,g)$, and
identity $\mathrm{id}{}_{a}=\mathsf{idt}(\star)$;

  * •

the functor $J$ is the identity on objects and
$J(f)=\mathbf{C}(\mathrm{id}{}_{a},f)(\mathsf{idt}(\star))$ on morphisms;

  * •

the binoidal structure on $\mathfrak{U}(\mathbf{C})$ is $a\rtimes b=a\ltimes
b=a\oplus_{\mathbf{M}}b$ on objects and $a\rtimes
f=\mathsf{par}(\mathsf{idt}(\star),f)$ and $f\ltimes
b=\mathsf{par}(f,\mathsf{idt}(\star))$ on morphisms.

######  Proof (Proof sketch)

It is mechanical to check that $\mathfrak{U}(\mathbf{C})$ is a well-defined
Freyd category. Given a morphism $F=\left(F_{0},F_{1}\right)$ from
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{Subset}$
to
$\mathbf{C}^{\prime}\colon\mathbf{M}^{\prime}{}^{\mathrm{op}}\times\mathbf{M}^{\prime}\to\mathbf{Subset}$,
we must define a morphism $\mathfrak{U}\left(F\right)\colon
J_{\mathfrak{U}\left(\mathbf{C}\right)}\to
J_{\mathfrak{U}\left(\mathbf{C}^{\prime}\right)}$. We define
$\mathfrak{U}\left(F\right)_{0}$ to be the strong monoidal functor $F_{0}$,
and define $\mathfrak{U}\left(F\right)_{1}$ as $F_{0}$ on objects and as
$F_{1}$ on homsets. This is a well-defined morphism of Freyd categories. It is
straightforward to verify that $\mathfrak{U}$ is functorial.

###### Theorem 4.1

The functors of Propositions 1 and 2 form an adjunction
$\mathfrak{F}\dashv\mathfrak{U}$.

######  Proof (Proof sketch)

For the unit $\boldsymbol{\eta}$ of the adjunction we may take the identity as
a short calculation shows that
$\mathfrak{U}\mathfrak{F}=\mathrm{Id}_{\mathbf{Freyd}}$. A second calculation
shows that for a $\mathbf{Subset}$-Freyd category
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{Subset}$,
we have
$\mathfrak{F}\mathfrak{U}\left(\mathbf{C}\right)\left(a,b\right)=\big{(}\mathbf{C}(\mathrm{id},\mathbf{M}(a,b))(\mathsf{idt}(\star)),\mathbf{C}(a,b)\big{)}$,
and so each component
$\boldsymbol{\epsilon}_{\mathbf{C}}\colon\mathfrak{F}\mathfrak{U}\left(\mathbf{C}\right)\to\mathbf{C}$
of the counit can be defined as
${\boldsymbol{\epsilon}_{\mathbf{C}}}_{0}=\mathrm{Id}_{\mathbf{M}}$ and
${\boldsymbol{\epsilon}_{\mathbf{C}}}_{1}=\mathrm{id}{}_{{\mathbf{C}\left(a,b\right)}}\colon\mathfrak{F}\mathfrak{U}\left(\mathbf{C}\right)\left(a,b\right)\to\mathbf{C}\left(a,b\right)$.
Note that the underlying $\mathbf{Set}$ map for
${\boldsymbol{\epsilon}_{\mathbf{C}}}_{1}$ is the identity map, but this is
not an identity in $\mathbf{Subset}$. This counit is natural, and this unit
and counit satisfy the zig-zag identities for an adjunction.

Recall that an adjunction $F\dashv G$ with unit $\eta\colon\mathrm{Id}\to GF$
and counit $\epsilon\colon FG\to\mathrm{Id}$ is _idempotent_ if any of
$F\eta$, $\epsilon F$, $\eta G$, or $G\epsilon$ are invertible [9, Section
3.8]. In the case of the previous theorem, clearly
$\mathfrak{F}\boldsymbol{\eta}$ is invertible as $\boldsymbol{\eta}$ is the
identity, so this adjunction is idempotent. This leads to the following
theorem detailing just how $\mathbf{Subset}\text{-}\mathbf{Freyd}$ generalises
$\mathbf{Freyd}$.

###### Theorem 4.2

The full coreflective subcategory of $\mathbf{Subset}\text{-}\mathbf{Freyd}$
consisting of objects
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{Subset}$
for which $\mathbf{C}\left(a,b\right)$ has the distinguished subset
$\mathbf{C}\left(\mathrm{id},\mathbf{M}\left(a,b\right)\right)\left(\mathsf{idt}\left(\star\right)\right)$
is equivalent to $\mathbf{Freyd}$.

######  Proof (Proof sketch)

The following is a general fact about idempotent adjunctions [9, Section 3.8]:
if $F\dashv G$ is an idempotent adjunction with associated monad $T=GF$ and
comonad $S=FG\colon\mathbf{A}\to\mathbf{A}$, then the category of algebras of
$T$ is equivalent to the category of coalgebras of $S$, and the category of
coalgebras of $S$ is a full coreflective subcategory of $\mathbf{A}$ given by
the objects of $\mathbf{A}$ for which $\epsilon\colon SA\to A$ is invertible.

The category of algebras for the monad $\mathfrak{U}\mathfrak{F}=\mathrm{Id}$
is equivalent to $\mathbf{Freyd}$, which is therefore a full coreflective
subcategory of $\mathbf{Subset}\text{-}\mathbf{Freyd}$. Furthermore, we can
characterize the objects of this subcategory as $\mathbf{Subset}$-Freyd
categories $\mathbf{C}$ for which to
$\boldsymbol{\epsilon}\colon\mathfrak{F}\mathfrak{U}\left(\mathbf{C}\right)\to\mathbf{C}$
is invertible. Concretely, this means
${\boldsymbol{\epsilon}_{\mathbf{C}}}_{1}$ must be invertible in
$\mathbf{Subset}$. But the underlying $\mathbf{Set}$ map is the identity,
establishing the claim.

##  5 Abstract characterisation

Definition 6 is a very concrete way to specify a $\mathbf{V}$-Freyd category,
involving a nontrivial amount of data and axioms. Yet it fits together, as we
show in this subsection by giving a characterisation in the style of [12].
Recall that a natural transformation between lax monoidal functors is
_monoidal_ when it respects the coherence maps $\mu$ and $\eta$. Write
$\mathbf{MonCat_{lax}}\big{(}\mathbf{C},\mathbf{D}\big{)}$ for the category of
lax monoidal functors from $\mathbf{C}$ to $\mathbf{D}$ and monoidal natural
transformations between them. If $\mathbf{A}$ and $\mathbf{B}$ are monoidal
categories, so are $\mathbf{A}^{\mathrm{op}}$ and
$\mathbf{A}\times\mathbf{B}$, with componentwise structure. Thus we may
consider
$\mathbf{MonCat_{lax}}\big{(}\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V}\big{)}$
for the monoidal category $(\mathbf{V},*,J)$. We will lift the other monoidal
structure $(\mathbf{V},\circ,I)$ to
$\mathbf{MonCat_{lax}}\big{(}\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V}\big{)}$
and prove that a $\mathbf{V}$-Freyd category is exactly a monoid with respect
to this monoidal structure, under additional assumptions on $\mathbf{V}$. Most
proofs are deferred to Appendix 0.B.

###### Definition 10

A duoidal category $\mathbf{V}$ is a _cocomplete duoidal category_ if
$\mathbf{V}$ is cocomplete and $*$ and $\circ$ are cocontinuous in each
argument. In a cocomplete duoidal category, the following diagrams and their
symmetric versions commute:

${{J*\text{colim}(D)}}$${{\text{colim}\left(J*D\right)}}$${{\text{colim}(D)}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$
${{I\circ\text{colim}(D)}}$${{\text{colim}\left(I\circ
D\right)}}$${{\text{colim}(D)}}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$$\scriptstyle{\simeq}$

where the top isomorphism is colimit preservation and the others are induced
by unitors.

The rest of this subsection assumes that $\mathbf{V}$ is a cocomplete duoidal
category; importantly, this is satisfied for presheaf categories. This
restriction will be mitigated in Section 6.2 for small $\mathbf{V}$. We also
assume that $\mathbf{M}$ is small. All laxness is with respect to
$(\mathbf{V},*,J)$. We now lift $(\mathbf{V},\circ,I)$; first the unit, then
composition.

###### Proposition 3

There is a lax monoidal functor
$\underline{\hom}_{\mathbf{M}}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{V}$
defined on objects as
$\underline{\hom}_{\mathbf{M}}(a,b)=\coprod_{\sigma\in\hom_{\mathbf{M}}(a,b)}I$.

###### Proposition 4

If $S,\,T\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{V}$ are lax
monoidal functors, the functor
$S\mathbin{\hat{\circ}}T\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{V}$
defined using coends as $(S\mathbin{\hat{\circ}}T)(a,c)=\int^{b}T(a,b)\circ
S(b,c)$ is lax monoidal.

###### Proposition 5

$\big{(}\mathbf{MonCat_{lax}}(\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V}),\mathbin{\hat{\circ}},\underline{\hom}_{\mathbf{M}}\big{)}$
is a monoidal category.

###### Proof

Lemmas 5, 6 and 7 in Appendix 0.B show that the $\circ$-composition is
functorial, associative, and has $\underline{\hom}_{\mathbf{M}}$ as left and
right unit. That leaves only the triangle and pentagon identities, which
follow from cocontinuity and the equivalent identities for $\circ$.

With these preparations we can characterise $\mathbf{V}$-Freyd categories
abstractly.

###### Theorem 5.1

Let $\mathbf{V}$ be a cocomplete duoidal category. Then a $\mathbf{V}$-Freyd
category
$\mathbf{C}\colon\mathbf{M}\times\mathbf{M}^{\mathrm{op}}\to\mathbf{V}$ is
exactly a monoid in
$\mathbf{MonCat_{lax}}(\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V})$.

######  Proof (Proof sketch)

A monoid $\mathbf{C}$ in
$\mathbf{MonCat_{lax}}(\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V})$
consists of two maps $e\colon\underline{\hom}_{\mathbf{M}}\to\mathbf{C}$ and
$m\colon\mathbf{C}\mathbin{\hat{\circ}}\mathbf{C}\to\mathbf{C}$, inducing
$\mathsf{idt}$ and $\mathsf{seq}$ satisfying unit and associativity
conditions. The lax monoidal structure of $\mathbf{C}$ gives $\mathsf{zero}$
and $\mathsf{par}$ respectively, so identity and associativity conditions
follow. Finally, the components of $e$ and $m$ are monoidal natural
transformations, ensuring that $\mathsf{idt}$ and $\mathsf{seq}$ respect
$\mathsf{zero}$ and $\mathsf{par}$.

We note that by Fujii’s observations [7], PROs and PROPs are equivalent to
$\mathbf{Set}$-Freyd categories over $\mathbf{N}$ and $\mathbf{P}$
respectively because $(\mathbf{Set},\times,\times)$ is a cocomplete duoidal
category.

##  6 Change of enrichment

After defining enriched categories, a natural next step is to consider a
change of enrichment. Any monoidal functor $\mathbf{V}\to\mathbf{W}$ induces a
functor $\mathbf{V}\text{-}\mathbf{Cat}\to\mathbf{W}\text{-}\mathbf{Cat}$. We
will show that the same holds for the appropriate type of functors between
duoidal categories and enriched Freyd categories (in Section 6.1). We will
then use that to alleviate the restriction of duoidal cocompleteness on the
abstract characterisation of Section 5 (in Section 6.2) at the cost of losing
a direction of the correspondence. Finally, changing enrichment along a
forgetful functor gives an underlying (unenriched) Freyd category
$J\colon\mathbf{M}\to\mathbf{C}$ with $\mathbf{C}$ monoidal, which we show
recovers the pure computations in the examples of Section 3 (in Section 6.3).

###  6.1 Lifting duoidal functors

To talk about change of enrichment, we first need to define the appropriate
type of functor between the enriching categories along which to change.

###### Definition 11

[2, Definition 6.54] Take duoidal categories
$\left(\mathbf{V},*_{\mathbf{V}},J_{\mathbf{V}},\circ_{\mathbf{V}},I_{\mathbf{V}}\right)$
and
$\left(\mathbf{W},*_{\mathbf{W}},J_{\mathbf{W}},\circ_{\mathbf{W}},I_{\mathbf{W}}\right)$.
A functor $F\colon\mathbf{V}\\!\to\\!\mathbf{W}$ is a _double lax monoidal
functor_ when equipped with $\eta_{*}$, $\mu_{*}$, $\eta_{\circ}$, and
$\mu_{\circ}$ such that $\left(F,\eta_{*},\mu_{*}\right)$ is lax monoidal for
$*_{\mathbf{V}}$ and $*_{\mathbf{W}}$,
$\left(F,\eta_{\circ},\mu_{\circ}\right)$ is lax monoidal for
$\circ_{\mathbf{V}}$ and $\circ_{\mathbf{W}}$, and the following diagrams
commute:

${{\left(F(A)\circ_{\mathbf{W}}F(B)\right)*_{\mathbf{W}}\left(F(C)\circ_{\mathbf{W}}F(D)\right)}}$${{\left(F(A)*_{\mathbf{W}}F(C)\right)\circ_{\mathbf{W}}\left(F(B)*_{\mathbf{W}}F(D)\right)}}$${{F\left(A\circ_{\mathbf{V}}B\right)*_{\mathbf{W}}F\left(C\circ_{\mathbf{V}}D\right)}}$${{F\left(A*_{\mathbf{V}}C\right)\circ_{\mathbf{W}}F\left(B*_{\mathbf{V}}D\right)}}$${{F\left(\left(A\circ_{\mathbf{V}}B\right)*_{\mathbf{V}}\left(C\circ_{\mathbf{V}}D\right)\right)}}$${{F\left(\left(A*_{\mathbf{V}}C\right)\circ_{\mathbf{V}}\left(B*_{\mathbf{V}}D\right)\right)}}$$\scriptstyle{\mu_{\circ}*\mu_{\circ}}$$\scriptstyle{\mu_{*}}$$\scriptstyle{\zeta}$$\scriptstyle{\mu_{*}\circ\mu_{*}}$$\scriptstyle{\mu_{\circ}}$$\scriptstyle{F\zeta}$${{F(J_{\mathbf{V}})}}$${{F(I_{\mathbf{V}})}}$${{J_{\mathbf{W}}}}$${{I_{\mathbf{W}}}}$$\scriptstyle{F\epsilon}$$\scriptstyle{\eta_{*}}$$\scriptstyle{\epsilon}$$\scriptstyle{\eta_{\circ}}$
${{J_{\mathbf{W}}}}$${{F(J_{\mathbf{V}})}}$${{F\left(J_{\mathbf{V}}\circ_{\mathbf{V}}J_{\mathbf{V}}\right)}}$${{J_{\mathbf{W}}\circ_{\mathbf{W}}J_{\mathbf{W}}}}$${{F(J_{\mathbf{V}})\circ_{\mathbf{W}}F(J_{\mathbf{V}})}}$$\scriptstyle{\eta_{*}}$$\scriptstyle{F\Delta}$$\scriptstyle{\Delta}$$\scriptstyle{\eta_{*}\circ\eta_{*}}$$\scriptstyle{\mu_{\circ}}$${{I_{\mathbf{W}}}}$${{F(I_{\mathbf{V}})}}$${{F\left(I_{\mathbf{V}}*_{\mathbf{V}}I_{\mathbf{V}}\right)}}$${{I_{\mathbf{W}}*_{\mathbf{W}}I_{\mathbf{W}}}}$${{F(I_{\mathbf{V}})*_{\mathbf{W}}F(I_{\mathbf{V}})}}$$\scriptstyle{\eta_{\circ}}$$\scriptstyle{F\nabla}$$\scriptstyle{\nabla}$$\scriptstyle{\eta_{\circ}*\eta_{\circ}}$$\scriptstyle{\mu_{*}}$

Here now is the change-of-enrichment theorem for duoidally enriched Freyd
categories.

###### Theorem 6.1

Let $F\colon\mathbf{V}\to\mathbf{W}$ be a double lax monoidal functor. For a
$\mathbf{V}$-Freyd category
$\mathbf{C}\colon\mathbf{M}^{\mathrm{op}}\times\mathbf{M}\to\mathbf{V}$,
define $\overline{F}(\mathbf{C})(a,b)\coloneqq F(\mathbf{C}(a,b))$ with
structure maps $\mathsf{idt}_{F}\coloneqq F\mathsf{idt}.\eta_{\circ}$,
$\mathsf{seq}_{F}\coloneqq F\mathsf{seq}.\mu_{\circ}$,
$\mathsf{zero}_{F}\coloneqq F\mathsf{zero}.\eta_{*}$, and
$\mathsf{par}_{F}\coloneqq F\mathsf{par}.\mu_{*}$. For a map
$G=(G_{0},G_{1})\colon\mathbf{C}\to\mathbf{C}^{\prime}$, define
$\overline{F}(G)\coloneqq(G_{0},FG_{1})$. This $\overline{F}$ is a functor
$\mathbf{V}\text{-}\mathbf{Freyd}\to\mathbf{W}\text{-}\mathbf{Freyd}$.

###### Proof

See Appendix 0.C.

###### Example 8

Let $M$ and $N$ be separated monoids and $\phi\colon M\to N$ a homomorphism
such that $\phi(m)\mathop{\|}\phi(m^{\prime})$ implies
$m\mathop{\|}m^{\prime}$. Then $\phi$ induces a double lax monoidal functor
$\phi_{*}\colon\mathbf{Label}_{M}\to\mathbf{Label}_{N}$ given by
$\ell\mapsto\phi.\ell$ on objects and $f\mapsto f$ on morphisms. The maps
$\eta_{*}$, $\mu_{*}$, and $\eta_{\circ}$ are all identities, while
$\mu_{\circ}\colon\\{(a,a^{\prime})\mid\phi.\ell(a)\|\phi.\ell^{\prime}(a^{\prime})\\}\to\\{(a,a^{\prime})\mid\ell(a)\|\ell^{\prime}(a^{\prime})\\}$
is the inclusion, and so $\phi_{*}$ is clearly double lax monoidal. Apply
Theorem 6.1 to the example from Section 3.1 along the map
$\mathcal{P}_{f}(!)\colon\mathcal{P}_{f}(R)\to\mathcal{P}_{f}(1)$, which is a
homomorphism such that
$\mathcal{P}_{f}(!)(P)\cap\mathcal{P}_{f}(!)(Q)=\emptyset$ implies $P\cap
Q=\emptyset$. We get
$\mathcal{P}_{f}(!)_{*}(\mathbf{C})(a,b)=\sum_{Q\in\mathcal{P}_{f}(R)}\left(\mathbf{Set}(a\times\Pi_{Q},b\times\Pi_{Q})\right)\to\mathcal{P}_{f}(1)$,
$(Q,f)\mapsto\emptyset\text{ if }Q=\emptyset\text{, else }1$. This change of
enrichment alters the example to only allowing maps to be put in parallel if
at least one of them requires no resources.

###### Example 9

We can use change of enrichment for the indexed state example of Section 3.2.
Consider Example 6 for $(\mathbf{Set},\times,1)$ (using universes for this
example to avoid size issues). There, the definition of Day convolution
$\times_{\mathrm{Day}}$ simplifies to
$(P\times_{\mathrm{Day}}Q)(a,b)=\int^{b_{2},b_{2}}\mathbf{Set}(b_{1}\times
b_{2},b)\times P(a,b_{1})\times Q(a,b_{2})$ and its unit becomes $k(a,b)=b$.
The Kleisli construction turns a finitary endofunctor on $\mathbf{Set}$ into a
profunctor as follows. Define
$\mathrm{Kl}\colon\left[\mathbf{Set},\mathbf{Set}\right]_{f}\to\mathbf{Prof}(\mathbf{Set})$
by $\mathrm{Kl}(F)(a,b)=\mathbf{Set}(a,Fb)$, and coherence maps:

$\displaystyle\eta_{*}\colon k$ $\displaystyle\to\mathrm{Kl}(\mathrm{Id})$
$\displaystyle\mu_{*}\colon\mathrm{Kl}(F_{1})\times_{\mathrm{Day}}\mathrm{Kl}(F_{2})$
$\displaystyle\to\mathrm{Kl}(F_{1}\times_{\mathrm{Day}}F_{2})$ $\displaystyle
b$ $\displaystyle\mapsto\mathsf{cst}_{b}$ $\displaystyle(k,f_{1},f_{2})$
$\displaystyle\mapsto\lambda a.(k,f_{1}(a),f_{2}(a))$
$\displaystyle\eta_{\circ}\colon\hom$
$\displaystyle\to\mathrm{Kl}(\mathrm{Id})$
$\displaystyle\mu_{\circ}\colon\mathrm{Kl}(F)\diamond\mathrm{Kl}(G)$
$\displaystyle\to\mathrm{Kl}(F\circ G)$ $\displaystyle f$
$\displaystyle\mapsto f$ $\displaystyle(f,g)$ $\displaystyle\mapsto Fg.f$

This makes $\mathrm{Kl}$ a double lax monoidal functor. Theorem 6.1 then gives
a $\mathbf{Prof}(\mathbf{Set})$-Freyd category defined by
$\mathrm{Kl}(\mathbf{C})(a,b)(x,y)\coloneqq\mathbf{Set}(x,\left(b\times
y\right)^{a})$.

###  6.2 Yoneda embedding

The Yoneda embedding of a small monoidal category is a strong monoidal functor
with respect to Day convolution. This extends to small duoidal categories.

###### Proposition 6

The Yoneda embedding
$\mathbf{V}\\!\to\\![\mathbf{V}^{\mathrm{op}},\mathbf{Set}]$ is a double lax
monoidal functor from small $\left(\mathbf{V},*,J,\circ,I\right)$ to
$\big{(}[\mathbf{V}^{\mathrm{op}},\mathbf{Set}],*_{\mathrm{Day}},\mathbf{V}(-,J),\circ_{\mathrm{Day}},\mathbf{V}(-,I)\big{)}$.

###### Proof

See [11] for the fact that it is lax monoidal for each monoidal structure
separately. The diagrams of Definition 11 are verified straightforwardly.

It follows from Theorem 6.1 that every $\mathbf{V}$-Freyd category for small
$\mathbf{V}$ induces a $[\mathbf{V}^{\mathrm{op}},\mathbf{Set}]$-Freyd
category. But $[\mathbf{V}^{\mathrm{op}},\mathbf{Set}]$ is duoidally
cocomplete, so the setting in which the abstract characterisation of Theorem
5.1 applies. We conclude that the characterisation extends beyond the
duoidally cocomplete setting in the sense that every $\mathbf{V}$-Freyd
category for small $\mathbf{V}$ induces a monoid in
$\mathbf{MonCat_{lax}}(\mathbf{M}^{\mathrm{op}}\times\mathbf{M},[\mathbf{V}^{\mathrm{op}},\mathbf{Set}])$.

###  6.3 Forgetful functors

Any category enriched in a monoidal category $\mathbf{V}$ has an underlying
(unenriched) category, got by changing the enrichment along the ‘forgetful’
monoidal functor $\mathbf{V}(I,-)\colon\mathbf{V}\to\mathbf{Set}$. A similar
process plays out for duoidal categories.

###### Proposition 7

Let $\left(\mathbf{V},*,J,\circ,I\right)$ be a duoidal category and write
$\phi\colon J\to J*J$ for the inverse of the unitors. Then
$\mathbf{V}(J,-)\colon\mathbf{V}\to\mathbf{Set}$ is a double lax monoidal
functor with coherence maps:

$\displaystyle\eta_{*}\colon 1$ $\displaystyle\to\mathbf{V}(J,J)$
$\displaystyle\mu_{*}\colon\mathbf{V}(J,A_{1})\times\mathbf{V}(J,A_{2})$
$\displaystyle\to\mathbf{V}(J,A_{1}*A_{2})$ $\displaystyle\star$
$\displaystyle\mapsto\mathrm{id}$ $\displaystyle(f_{1},f_{2})$
$\displaystyle\mapsto(f_{1}*f_{2}).\phi$ $\displaystyle\eta_{\circ}\colon 1$
$\displaystyle\to\mathbf{V}(J,I)$
$\displaystyle\mu_{\circ}\colon\mathbf{V}(J,A_{1})\times\mathbf{V}(J,A_{2})$
$\displaystyle\to\mathbf{V}(J,A_{1}\circ A_{2})$ $\displaystyle\star$
$\displaystyle\mapsto\epsilon$ $\displaystyle(f_{1},f_{2})$
$\displaystyle\mapsto(f_{1}\circ f_{2}).\Delta$

Applying Theorem 6.1 along the forgetful functor of the previous proposition
in the case of the examples of Section 3 will show that this recovers the
underlying pure computations. Note that a $\mathbf{Set}$-Freyd category
$\mathbf{C}$ has a trivial instance of the exchange axiom, item viii, and so
$\mathbf{C}$ is a monoidal category with identity-on-objects monoidal functor
$J\colon\mathbf{M}\to\mathbf{C}$.

###### Example 10

Applying the forgetful functor to the stateful function example of Section 3.1
results in the (unenriched) category with
$\mathbf{Label}_{\mathcal{P}_{f}(R)}(\mathsf{cst}_{\emptyset},\mathbf{C}(a,b))$
as the homsets. Because labels are preserved, the morphisms in this
(unenriched) category are exactly the elements of $\mathbf{C}(a,b)$ which have
label $\emptyset$, i.e. maps $a\times 1\to b\times 1$ which are pure
functions.

###### Example 11

Changing the enrichment of the indexed state example from Section 3.2 along
the forgetful functor gives the (unenriched) category with homsets
$\left[\mathbf{Set},\mathbf{Set}\right]_{f}(\mathrm{Id},\mathbf{C}(a,b))$. If
$\phi\colon\mathrm{Id}\to(b\times(-))^{a}$ is such a natural transformation,
then the function $\phi_{1}\colon 1\to(b\times 1)^{a}$, which is equivalent to
choosing a function $f\colon a\to b$, completely determines $\phi$, because
for any set $X$ and $x\in X$ by naturality
$1\xrightarrow{x}X\xrightarrow{\phi_{X}}(b\times
X)^{a}=1\xrightarrow{\phi_{1}}(b\times 1)^{a}\xrightarrow{(\mathrm{id}\times
x).-}(b\times X)^{a}$, whence $\phi_{X}(x)(a)=(f(a),x)$. Therefore the
morphisms in this (unenriched) category are all functions $a\to b$.

###### Example 12

Changing the enrichment of the Kleisli categories of Lawvere theories example
from Section 3.3 along the forgetful functor gives the (unenriched) category
with homsets $[\mathbf{Law},\mathbf{Set}](\mathbb{1},\mathbf{C}(a,b))$.
Consider such a natural transformation $\phi\colon\mathbb{1}\to T(-)(b)^{a}$.
It is completely determined by its component at $\mathcal{S}$. For any
$\mathcal{L}$ let $\iota\colon\mathcal{S}\to\mathcal{L}$ be the unique map,
then naturality implies $\phi_{\mathcal{L}}=T(\iota)\phi_{\mathcal{S}}$.
Furthermore, $\phi_{\mathcal{S}}(\star)\in T(\mathcal{S})(b)^{a}=b^{a}$. So
the morphisms in this (unenriched) category again are all functions $a\to b$.

##  7 Conclusion

We have defined a version of Freyd categories enriched over any duoidal
category $\mathbf{V}$, and morphisms between them. We used various duoidal
categories to give examples based on separation of resources, parameterised
monads, and the Kleisli construction for Lawvere theories. By enriching with
$\mathbf{Subset}$, we have proven that the category of Freyd categories
$\mathbf{Freyd}$ is a full coreflective subcategory of
$\mathbf{Subset}\text{-}\mathbf{Freyd}$, thus establishing that
$\mathbf{V}$-Freyd categories indeed generalise Freyd categories.
Additionally, we proved an abstract characterisation of $\mathbf{V}$-Freyd
categories over small $\mathbf{M}$ for duoidally cocomplete $\mathbf{V}$, they
are monoids in
$\mathbf{MonCat_{lax}}\big{(}\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V}\big{)}$.
Finally, we provided change of enrichment and examples thereof.

##### Future work

There are several directions for further investigation:

  * •

The abstract characterisation of Section 5 may be part of a larger structure,
namely a _bicategory with proarrow equipment_ , whose objects are monoidal
categories, arrows are strong monoidal functors, proarrows are lax monoidal
profunctors, and cells are lax monoidal natural transformations. In this
setting, a $\mathbf{V}$-Freyd category would be a monad and the vertical monad
morphisms would be a $\mathbf{V}$-Freyd morphism. This would enable applying
general constructions for monads in a bicategory.

  * •

Relatedly, an _fc-multicategory_ structure on
$\mathbf{MonCat_{lax}}(\mathbf{M}^{\mathrm{op}}\times\mathbf{M},\mathbf{V})$
may bypass cocompleteness in characterising $\mathbf{V}$-Freyd categories as
monoids.

  * •

The abstract characterisation of Section 5 also uses the free
$\mathbf{V}$-category on $\mathbf{M}$. It may be fruitful to change the
definition of a $\mathbf{V}$-Freyd category to be a $\mathbf{V}$-functor
$J\colon\mathbf{M}\to\mathbf{C}$ where we extend $\mathbf{V}$-categories in a
way similar to Morrison and Penneys [16].

  * •

Freyd categories can have the property of being _closed_. In this case they
induce a strong monad. A similar definition may be possible for
$\mathbf{V}$-Freyd categories. This could determine a higher-order semantics
for effectful programs based on duoidal categories. A nontrivial definition of
closure may require a $\mathbf{V}$-category $\mathbf{M}$ that is not free.

  * •

Our original motivation stemmed from the desire for semantics combining
differentiable and probabilistic programming, in particular, the possibility
of having a linear structure for the probabilistic fragment and a cartesian
one for differentiable terms. $\mathbf{Prof}$-Freyd categories may provide a
useful separation to aid the desired distinction between linear and cartesian
properties.

####  7.0.1 Acknowledgments

We would like to thank Robin Kaarsgaard, Ohad Kammar, and Matthew Di Meglio
for their input and encouragement, as well as the reviewers of all versions of
this work.

## References

  * [1] Adamek, J., Rosicky, J.: Locally presentable and accessible categories. Cambridge University Press (1994). https://doi.org/10.1017/CBO9780511600579
  * [2] Aguiar, M., Mahajan, S.: Monoidal Functors, Species and Hopf Algebras. American Mathematical Society (2010). https://doi.org/10.1090/crmm/029
  * [3] Atkey, R.: Algebras for parameterised monads. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) Algebra and Coalgebra in Computer Science, Lecture Notes in Computer Science, vol. 5728, pp. 3–17. Springer (2009). https://doi.org/10.1007/978-3-642-03741-2_2
  * [4] Batanin, M., Markl, M.: Centers and homotopy centers in enriched monoidal categories. Advances in Mathematics 230, 1811–1858 (2012). https://doi.org/10.1016/j.aim.2012.04.011
  * [5] Day, B.: On closed categories of functors. In: Midwest Category Seminar. Lecture Notes in Mathematics, vol. 137, pp. 1–38 (1970)
  * [6] Forcey, S.: Enrichment over iterated monoidal categories. Algebraic & Geometric Topology 4, 95–119 (2004). https://doi.org/10.2140/agt.2004.4.95
  * [7] Fujii, S.: A unified framework for notions of algebraic theory. Theory and Applications of Categories 34(40), 1246–1316 (2019)
  * [8] Garner, R., López Franco, I.: Commutativity. Journal of Pure and Applied Algebra 220(5), 1707–1751 (2016). https://doi.org/10.1016/j.jpaa.2015.09.003
  * [9] Grandis, M.: Category theory and applications: a textbook for beginners. World Scientific, 2 edn. (Apr 2021). https://doi.org/10.1142/12253
  * [10] Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006). https://doi.org/10.1016/j.tcs.2006.03.013
  * [11] Im, G.B., Kelly, G.M.: A universal property of the convolution monoidal structure. Journal of Pure and Applied Algebra 43, 75–88 (1986). https://doi.org/10.1016/0022-4049(86)90005-8
  * [12] Jacobs, B., Heunen, C., Hasuo, I.: Categorical semantics for Arrows. Journal of Functional Programming 19(3–4), 403–438 (2009). https://doi.org/10.1017/S0956796809007308
  * [13] Lack, S.: Composing PROPs. Theory and Applications of Categories 13(9), 147–163 (2004)
  * [14] Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Information and Computation 185(2), 182–210 (2003). https://doi.org/10.1016/S0890-5401(03)00088-9
  * [15] Moggi, E.: Notions of computation and monads. Information and Computation 93, 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4
  * [16] Morrison, S., Penneys, D.: Monoidal categories enriched in braided monoidal categories. International Mathematical Research Notes 11, 3527–3579 (2019). https://doi.org/10.1093/imrn/rnx217
  * [17] Plotkin, G., Power, J.: Computational effects and operations: an overview. In: Domains. Electronic Notes in Theoretical Computer Science, vol. 73, pp. 149–163 (2004). https://doi.org/10.1016/j.entcs.2004.08.008
  * [18] Power, J., Robinson, E.: Premonoidal categories and notions of computation. Mathematical Structures in Computer Science 7(5), 453–468 (1997). https://doi.org/10.1017/S0960129597002375
  * [19] Power, J.: Premonoidal categories as categories with algebraic structure. Theoretical Computer Science 278(1-2), 303–321 (May 2002). https://doi.org/10.1016/S0304-3975(00)00340-6, https://www.sciencedirect.com/science/article/pii/S0304397500003406, publisher: Elsevier
  * [20] Staton, S.: Freyd categories are enriched Lawvere theories. In: Proceedings of the Workshop on Algebra, Coalgebra and Topology. Electronic Notes in Theoretical Computer Science, vol. 303, pp. 197–206 (2014). https://doi.org/10.1016/j.entcs.2014.02.010

##  Appendix 0.A Definition of $\mathbf{V}$-Freyd category

This appendix spells out the type diagrams of Definition 6 of
$\mathbf{V}$-Freyd categories.

Extranaturality of $\mathsf{idt}$:

${I}$${{\mathbf{C}(b,b)}}$${{\mathbf{C}(a,a)}}$${{\mathbf{C}(a,b)}}$$\scriptstyle{\mathsf{idt}}$$\scriptstyle{\mathbf{C}(f,\mathrm{id})}$$\scriptstyle{\mathsf{idt}}$$\scriptstyle{\mathbf{C}(\mathrm{id},f)}$

Extranaturality of $\mathsf{seq}$:

${{\mathbf{C}(a,b)\circ\mathbf{C}(b^{\prime},c)}}$${{\mathbf{C}(a,b^{\prime})\circ\mathbf{C}(b^{\prime},c)}}$${{\mathbf{C}(a,b)\circ\mathbf{C}(b,c)}}$${{\mathbf{C}(a,c)}}$$\scriptstyle{\mathbf{C}(\mathrm{id},f)\circ\mathrm{id}}$$\scriptstyle{\mathsf{seq}}$$\scriptstyle{\mathrm{id}\circ\mathbf{C}(f,\mathrm{id})}$$\scriptstyle{\mathsf{seq}}$

$\mathsf{idt}$ is the identity for $\mathsf{seq}$:

${{I\circ\mathbf{C}(a,b)}}$${{\mathbf{C}(a,a)\circ\mathbf{C}(a,b)}}$${{\mathbf{C}(a,b)}}$$\scriptstyle{\lambda}$$\scriptstyle{\mathsf{seq}}$$\scriptstyle{\mathsf{idt}\circ\mathrm{id}}$
${{\mathbf{C}(a,b)\circ
I}}$${{\mathbf{C}(a,b)\circ\mathbf{C}(b,b)}}$${{\mathbf{C}(a,b)}}$$\scriptstyle{\rho}$$\scriptstyle{\mathsf{seq}}$$\scriptstyle{\mathrm{id}\circ\mathsf{idt}}$

$\mathsf{seq}$ is associative:

${{\left(\mathbf{C}(a,b)\circ\mathbf{C}(b,c)\right)\circ\mathbf{C}(c,d)}}$${{\mathbf{C}(a,b)\circ\left(\mathbf{C}(b,c)\circ\mathbf{C}(c,d)\right)}}$${{\mathbf{C}(a,c)\circ\mathbf{C}(c,d)}}$${{\mathbf{C}(a,b)\circ\mathbf{C}(b,d)}}$${{\mathbf{C}(a,d)}}$$\scriptstyle{\alpha}$$\scriptstyle{\mathrm{id}\circ\mathsf{seq}}$$\scriptstyle{\mathsf{seq}}$$\scriptstyle{\mathsf{seq}\circ\mathrm{id}}$$\scriptstyle{\mathsf{seq}}$

$\mathsf{zero}$ is the identity for $\mathsf{par}$:

${{J*\mathbf{C}(a,b)}}$${{\mathbf{C}(e,e)*\mathbf{C}(a,b)}}$${{\mathbf{C}(a,b)}}$${{\mathbf{C}(e\oplus
a,e\oplus
b)}}$$\scriptstyle{\lambda}$$\scriptstyle{\mathsf{zero}*\mathrm{id}}$$\scriptstyle{\mathsf{par}}$$\scriptstyle{\mathbf{C}(\lambda^{-1},\lambda)}$
${{\mathbf{C}(a,b)*J}}$${{\mathbf{C}(a,b)*\mathbf{C}(e,e)}}$${{\mathbf{C}(a,b)}}$${{\mathbf{C}(b\oplus
e,b\oplus
e)}}$$\scriptstyle{\rho}$$\scriptstyle{\mathrm{id}*\mathsf{zero}}$$\scriptstyle{\mathsf{par}}$$\scriptstyle{\mathbf{C}(\rho^{-1},\rho)}$

$\mathsf{par}$ is associative:

${{\left(\mathbf{C}(a_{1},b_{1})*\mathbf{C}(a_{2},b_{2})\right)*\mathbf{C}(a_{3},b_{3})}}$${{\mathbf{C}(a_{1},b_{1})*\left(\mathbf{C}(a_{2},b_{2})*\mathbf{C}(a_{3},b_{3})\right)}}$${{\mathbf{C}(a_{1}\oplus
a_{2},b_{1}\oplus
b_{2})*\mathbf{C}(a_{3},b_{3})}}$${{\mathbf{C}(a_{1},b_{1})*\mathbf{C}(a_{2}\oplus
a_{3},b_{2}\oplus b_{3})}}$${{\mathbf{C}((a_{1}\oplus a_{2})\oplus
a_{3},(b_{1}\oplus b_{2})\oplus b_{3})}}$${{\mathbf{C}(a_{1}\oplus(a_{2}\oplus
a_{3}),b_{1}\oplus(b_{2}\oplus
b_{3}))}}$$\scriptstyle{\alpha}$$\scriptstyle{\mathrm{id}*\mathsf{par}}$$\scriptstyle{\mathsf{par}}$$\scriptstyle{\mathsf{par}*\mathrm{id}}$$\scriptstyle{\mathsf{par}}$$\scriptstyle{\mathbf{C}(\alpha^{-1},\alpha)}$

$\mathsf{idt}$ respects $\mathsf{zero}$:

${J}$${I}$${{\mathbf{C}(e,e)}}$$\scriptstyle{\epsilon}$$\scriptstyle{\mathsf{idt}}$$\scriptstyle{\mathsf{zero}}$

$\mathsf{idt}$ respects $\mathsf{par}$:

${{I*I}}$${{\mathbf{C}(a,a)*\mathbf{C}(b,b)}}$${I}$${{\mathbf{C}(a\oplus
b,a\oplus
b)}}$$\scriptstyle{\mathsf{par}}$$\scriptstyle{\mathsf{idt}*\mathsf{idt}}$$\scriptstyle{\nabla}$$\scriptstyle{\mathsf{idt}}$

$\mathsf{seq}$ respects $\mathsf{zero}$:

${J}$${{J\circ
J}}$${{\mathbf{C}(e,e)}}$${{\mathbf{C}(e,e)\circ\mathbf{C}(e,e)}}$$\scriptstyle{\mathsf{zero}}$$\scriptstyle{\mathsf{zero}\circ\mathsf{zero}}$$\scriptstyle{\Delta}$$\scriptstyle{\mathsf{seq}}$

$\mathsf{seq}$ respects $\mathsf{par}$:

${{\left(\mathbf{C}(a_{1},b_{1})\\!\circ\\!\mathbf{C}(b_{1},c_{1})\right)\\!*\\!\left(\mathbf{C}(a_{2},b_{2})\\!\circ\\!\mathbf{C}(b_{2},c_{2})\right)}}$${{\left(\mathbf{C}(a_{1},b_{1})\\!*\\!\mathbf{C}(a_{2},b_{2})\right)\\!\circ\\!\left(\mathbf{C}(b_{1},c_{1})\\!*\\!\mathbf{C}(b_{2},c_{2})\right)}}$${{\mathbf{C}(a_{1},c_{1})*\mathbf{C}(a_{2},c_{2})}}$${{\mathbf{C}(a_{1}\oplus
a_{2},b_{1}\oplus b_{2})\circ\mathbf{C}(b_{1}\oplus b_{2},c_{1}\oplus
c_{2})}}$${{\mathbf{C}(a_{1}\oplus a_{2},c_{1}\oplus
c_{2})}}$$\scriptstyle{\zeta}$$\scriptstyle{\mathsf{par}\circ\mathsf{par}}$$\scriptstyle{\mathsf{seq}}$$\scriptstyle{\mathsf{seq}*\mathsf{seq}}$$\scriptstyle{\mathsf{par}}$

##  Appendix 0.B Proofs for abstract characterisation

This appendix contains proofs of the abstract characterisation of
$\mathbf{V}$-Freyd categories of Section 5. They rely on properties of
$\mathbf{V}$-Freyd categories listed in the following four lemmas, that are
mechanical to verify.

###### Lemma 1

The unitors of $\circ$ respect $\mathsf{zero}$ and $\mathsf{par}$:

$\displaystyle\rho.\mathsf{zero}$
$\displaystyle=(\mathsf{zero}\circ\epsilon).\Delta$
$\displaystyle\mathsf{zero}.\lambda$
$\displaystyle=(\epsilon\circ\mathsf{zero}).\Delta$
$\displaystyle\rho.\mathsf{par}$
$\displaystyle=(\mathsf{par}\circ\nabla).\zeta.(\rho*\rho)$
$\displaystyle\mathsf{par}.\lambda$
$\displaystyle=(\mathsf{par}\circ\nabla).\zeta.(\lambda*\lambda)$

###### Lemma 2

The associator of $\circ$ respects $\mathsf{zero}$ and $\mathsf{par}$:

$\displaystyle\alpha.(\mathsf{zero}\circ(\mathsf{zero}\circ\mathsf{zero})).(\mathrm{id}\circ\Delta).\Delta$
$\displaystyle=((\mathsf{zero}\circ\mathsf{zero})\circ\mathsf{zero}).(\Delta\circ\mathrm{id}).\Delta$
$\displaystyle\alpha.(\mathsf{par}\circ(\mathsf{par}\circ\mathsf{par})).(\mathrm{id}\circ\zeta).\zeta$
$\displaystyle=((\mathsf{par}\circ\mathsf{par})\circ\mathsf{par})).(\zeta\circ\mathrm{id}).\zeta.(\alpha*\alpha)$

###### Lemma 3

The unitors of $*$ respect $\mathsf{zero}$ and $\mathsf{par}$:

$\displaystyle\mathrm{id}$
$\displaystyle=(\mathsf{par}\circ\mathsf{par}).\zeta.(\mathrm{id}*((\mathsf{zero}\circ\mathsf{zero}).\Delta)).\rho$
$\displaystyle\mathrm{id}$
$\displaystyle=(\mathsf{par}\circ\mathsf{par}).\zeta.(((\mathsf{zero}\circ\mathsf{zero}).\Delta)*\mathrm{id}).\lambda$

###### Lemma 4

The associator of $*$ respects $\mathsf{par}$:

$\displaystyle((\mathsf{par}.(\mathsf{par}*\mathrm{id}))\circ(\mathsf{par}.(\mathsf{par}*\mathrm{id})).\zeta.(\zeta*\mathrm{id})=$
$\displaystyle((\mathsf{par}.(\mathrm{id}*\mathsf{par}))\circ(\mathsf{par}.(\mathrm{id}*\mathsf{par})).\zeta.(\mathrm{id}*\zeta).\alpha$

The previous lemmas require all the axioms of a duoidal category between them,
except for $\circ$ being a monoid in $(\mathbf{V},*,J)$. This latter property
is used in the abstract characterisation.

######  Proof (Proof of Proposition 3)

Bifunctorality is inherited from $\hom_{\mathbf{M}}$. The coherence morphisms
making it lax monoidal are $\eta\colon
J\xrightarrow{\epsilon}I\xrightarrow{\iota_{\mathrm{id}_{0}}}\coprod\nolimits_{\sigma}I\cong\underline{\hom}_{\mathbf{M}}(e,e)$
and

$\displaystyle\mu\colon$
$\displaystyle\big{(}\textstyle\coprod\nolimits_{\sigma_{1}}I\big{)}*\big{(}\textstyle\coprod\nolimits_{\sigma_{2}}I\big{)}\cong\textstyle\coprod\nolimits_{\sigma_{1},\sigma_{2}}I*I\xrightarrow{\textstyle\coprod\nabla}\textstyle\coprod\nolimits_{\sigma_{1},\sigma_{2}}I\xrightarrow{[\iota_{\sigma_{1}\oplus\sigma_{2}}]_{\sigma_{1},\sigma_{2}}}\textstyle\coprod\nolimits_{\sigma}\text{.}$

The coherence diagrams commute by cocontinuity and the monoidal structure
$(I,\nabla,\epsilon)$.

######  Proof (Proof of Proposition 4)

The coherence morphisms are:

$\displaystyle\eta_{S\mathbin{\hat{\circ}}T}\colon$ $\displaystyle
J\xrightarrow{\Delta}J\circ J\xrightarrow{\eta_{S}\circ\eta_{T}}T(e,e)\circ
S(e,e)\to\textstyle\int^{b}T(e,b)\circ
S(b,e)\cong(S\mathbin{\hat{\circ}}T)(e,e)$
$\displaystyle\mu_{S\mathbin{\hat{\circ}}T}\colon$
$\displaystyle(S\mathbin{\hat{\circ}}T)(a,c)*(S\mathbin{\hat{\circ}}T)(a^{\prime},c^{\prime})$
$\displaystyle\simeq$
$\displaystyle\textstyle\int^{b,b^{\prime}}\left(T(a,b)\\!\circ\\!S(b,c)\right)*\left(T(a^{\prime},b^{\prime})\\!\circ\\!S(b^{\prime},c^{\prime})\right)$
$\displaystyle\xrightarrow{\int\\!\zeta}$
$\displaystyle\textstyle\int^{b,b^{\prime}}\left(T(a,b)\\!*\\!T(a^{\prime},b^{\prime})\right)\circ\left(S(b,c)\\!*\\!S(b^{\prime},c^{\prime})\right)$
$\displaystyle\xrightarrow{\int\\!\mu_{T}\circ\mu_{S}}$
$\displaystyle\textstyle\int^{b,b^{\prime}}T(a\oplus a^{\prime},b\oplus
b^{\prime})\circ S(b\oplus b^{\prime},c\oplus c^{\prime})$
$\displaystyle\rightarrow$ $\displaystyle\textstyle\int^{b}T(a\oplus
a^{\prime},b)\circ S(b,c^{\prime}\oplus
c^{\prime})\simeq(S\mathbin{\hat{\circ}}T)(a\oplus a^{\prime},c\oplus
c^{\prime})$

Cocontinuity and Lemmas 3 and 4 finish the proof.

###### Lemma 5

The $\circ$-composition of Proposition 4 is functorial.

###### Proof

It is easy to see that $\mathbin{\hat{\circ}}$ is well-defined on objects.
Bifunctorality for morphisms then follows from bifunctorality of $\circ$ and
functorality of coends.

###### Lemma 6

The functor $\underline{\hom}_{\mathbf{M}}$ of Proposition 3 is the left and
right identity of the $\circ$-composition of Proposition 4.

###### Proof

The isomorphism on objects involves cocontinuity, the unitors of $\circ$, left
Kan extending along the identity. Naturality is inherited from the naturality
of the constructions involved. The unitors must also be monoidal natural
transformations, which is true via cocontinuity and Lemma 1.

###### Lemma 7

The $\circ$-composition of Proposition 4 is associative.

###### Proof

The isomorphism uses cocontinuity and the associator of $\circ$. Naturality is
inherited from the naturality of the constructions involved. The associator is
a monoidal natural transformation by cocontinuity and Lemma 2.

##  Appendix 0.C Proofs for change of enrichment

######  Proof (Proof of Theorem 6.1)

Items i, ii, iii and iv hold by the axioms for lax monoidal functors for the
same reason lax monoidal functors preserve monoids. Items v, vi, vii and viii
each require the use of an axiom of double lax monoidal functors as shown
below.

$\displaystyle\mathsf{idt}_{F}.\epsilon$
$\displaystyle=F\mathsf{idt}.\eta_{\circ}.\epsilon$
$\displaystyle=F\mathsf{idt}.F\epsilon.\eta_{*}$
$\displaystyle=F\mathsf{zero}.\eta_{*}$ $\displaystyle=\mathsf{zero}_{F}$
$\displaystyle\mathsf{idt}_{F}.\nabla$
$\displaystyle=F\mathsf{idt}.\eta_{\circ}.\nabla$
$\displaystyle=F\mathsf{idt}.F\nabla.\mu_{*}.(\eta_{\circ}*\eta_{\circ})$
$\displaystyle=F\mathsf{par}.F(\mathsf{idt}*\mathsf{idt}).\mu_{*}.(\eta_{\circ}*\eta_{\circ})$
$\displaystyle=F\mathsf{par}.\mu_{*}.(F\mathsf{idt}*F\mathsf{idt}).(\eta_{\circ}*\eta_{\circ})$
$\displaystyle=\mathsf{par}_{F}.(\mathsf{idt}_{F}*\mathsf{idt}_{F})$
$\displaystyle\mathsf{seq}_{F}.(\mathsf{zero}_{F}\circ\mathsf{zero}_{F}).\Delta$
$\displaystyle=F\mathsf{seq}.\mu_{\circ}.(F\mathsf{zero}\circ
F\mathsf{zero}).(\eta_{*}\circ\eta_{*}).\Delta$
$\displaystyle=F\mathsf{seq}.F(\mathsf{zero}\circ\mathsf{zero}).\mu_{\circ}.(\eta_{*}\circ\eta_{*}).\Delta$
$\displaystyle=F\mathsf{seq}.F(\mathsf{zero}\circ\mathsf{zero}).F\Delta.\eta_{*}$
$\displaystyle=F\mathsf{zero}.\eta_{*}$ $\displaystyle=\mathsf{zero}_{F}$
$\displaystyle\mathsf{seq}_{F}.(\mathsf{par}_{F}\circ\mathsf{par}_{F}).\zeta$
$\displaystyle=F\mathsf{seq}.\mu_{\circ}.(F\mathsf{par}\circ
F\mathsf{par}).(\mu_{*}\circ\mu_{*}).\zeta$
$\displaystyle=F\mathsf{seq}.F(\mathsf{par}\circ\mathsf{par}).\mu_{\circ}.(\mu_{*}\circ\mu_{*}).\zeta$
$\displaystyle=F\mathsf{seq}.F(\mathsf{par}\circ\mathsf{par}).F\zeta.\mu_{\circ}.(\mu_{*}\circ\mu_{*})$
$\displaystyle=F\mathsf{par}.F(\mathsf{seq}*\mathsf{seq}).\mu_{\circ}.(\mu_{*}\circ\mu_{*})$
$\displaystyle=F\mathsf{par}.\mu_{\circ}.(F\mathsf{seq}*F\mathsf{seq}).(\mu_{*}\circ\mu_{*})$
$\displaystyle=\mathsf{par}_{F}.(\mathsf{seq}_{F}*\mathsf{seq}_{F})$

Similar checks show that $\overline{F}(G)$ is a $\mathbf{W}$-Freyd map.
$\overline{F}$ is functorial by functorality of $F$.