---
abstract: 'A new categorical framework is provided for dealing with multiple arguments in a programming language with effects, for example in a language with imperative features. Like related frameworks (Monads, Arrows, Freyd categories), we distinguish two kinds of functions. In addition, we also distinguish two kinds of equations. Then, we are able to define a kind of product, that generalizes the usual categorical product. This yields a powerful tool for deriving many results about languages with effects.'
author:
- |
    Jean-Guillaume Dumas\
    LJK, University of Grenoble, France. [[`J`ean-Guillaume.Dumas@imag.fr]{}]{}\
    Dominique Duval\
    LJK, University of Grenoble, France. [[`D`ominique.Duval@imag.fr]{}]{}\
    Jean-Claude Reynaud\
    Malhiver, 38640 Claix, France. [[`J`ean-Claude.Reynaud@imag.fr]{}]{}
bibliography:
- 'prod.bib'
date: 'July 4., 2007'
title: Sequential products in effect categories
---

\[section\] \[thm\][Corollary]{} \[thm\][Lemma]{} \[thm\][Proposition]{} \[thm\][Assumption]{}

\[thm\][Remark]{} \[thm\][Remarks]{} \[thm\][Example]{} \[thm\][Examples]{} \[thm\][Definition]{} \[thm\][Convention]{} \[thm\][Conjecture]{} \[thm\][Problem]{} \[thm\][Open Problem]{} \[thm\][Algorithm]{} \[thm\][Observation]{} \[thm\][Question]{}

Introduction
============

The aim of this paper is to provide a new categorical framework dealing with multiple arguments in a programming language with effects, for example in a language with imperative features. In our *cartesian effect categories*, as in other related frameworks (Monads, Arrows, Freyd categories), two kinds of functions are distinguished. The new feature here is that two kinds of equations are also distinguished. Then, we define a kind of product, that is mapped to the usual categorical product when the distinctions (between functions and between equations) are forgotten. In addition, we prove that cartesian effect categories determine Arrows.

A well-established framework for dealing with computational effects is the notion of *strong monads*, that is used in Haskell [@Moggi91; @Wadler93]. Monads have been generalized on the categorical side to *Freyd categories* [@PowerRobinson97] and on the functional programming side to *Arrows* [@Hughes00]. The claims that Arrows generalize Monads and that Arrows are Freyd categories are made precise in [@HeunenJacobs06]. In all these frameworks, effect-free functions are distinguished among all functions, generalizing the distinction of *values* among all *computations* in [@Moggi91]. In this paper, as in [@BentonHyland03; @HeunenJacobs06], effect-free functions are called *pure* functions; however, the symbols ${\mathbf{C}}$ and ${\mathbf{V}}$, that are used for the category of all functions and for the subcategory of pure functions, respectively, are reminiscent of Moggi’s terminology.

In all these frameworks, one major issue is about the order of evaluation of the arguments of multivariate operations. When there is no effect, the order does not matter, and the notion of product in a cartesian category provides a relevant framework. So, the category ${\mathbf{V}}$ is cartesian, and *products of pure funtions* are defined by the usual characteristic property of products. But, when effects do occur, the order of evaluation of the arguments becomes fundamental, which cannot be dealt with the categorical product. So, the category ${\mathbf{C}}$ is not cartesian, and products of functions do not make sense, in general. However, some kind of *sequential product of computations* should make sense, in order to evaluate the arguments in a given order. This is usually defined, by composition, from some kinds of products of a computation with an identity. This is performed by the *strength* of the monad [@Moggi91], by the *symmetric premonoidal category* of the Freyd category [@PowerRobinson97], and by the *first* operator of Arrows [@Hughes00].

In this paper, the framework of *cartesian effect categories* is introduced. We still distinguish two kinds of functions: pure functions among arbitrary functions, that form two categories ${\mathbf{V}}$ and ${\mathbf{C}}$, with ${\mathbf{V}}$ a subcategory of ${\mathbf{C}}$, and ${\mathbf{V}}$ cartesian. Let us say that the functions are *decorated*, either as pure or as arbitrary. The new feature that is introduced in this paper is that we also distinguish two kinds of equations: strong equations and *semi-equations*, respectively denoted ${\equiv}$ and ${\lesssim}$, so that equations also are *decorated*. Strong equations can be seen, essentially, as equalities between computations, while semi-equations are much weaker, and can be seen as a kind of approximation relation. Moreover, as suggested by the symbols ${\equiv}$ and ${\lesssim}$, the strong equations form an equivalence relation, while the semi-equations form a preorder relation. Then, we define the *semi-product* of two functions when at least one is pure, by a characteristic property that is a decorated version of the characteristic property of the usual product. Since all identities are values, we get the semi-product of any function with an identity, that is used for building sequential products of functions.

Cartesian effect categories give rise to Arrows, in the sense of [@Hughes00], and they provide a deduction system: it is possible to decorate many proofs on cartesian categories in order to get proofs on cartesian effect categories.

As for terminology, our *graphs* are directed multi-graphs, made of *points* (or vertices, or objects) and *functions* (or edges, arrows, morphisms). We use *weak* categories rather than categories, i.e., we use a congruence $\equiv$ rather than the equality, however this “syntactic” choice is not fundamental here. As for notations, we often omit the subscripts in the diagrams and in the proofs.

Cartesian weak categories are reminded in section \[sec:weak\], then cartesian effect categories are defined in section \[sec:effect\]; they are compared with Arrows in section \[sec:related\], and examples are presented in section \[sec:exam\]. In appendix \[app:proof\] are given the proofs of some properties of cartesian weak categories, that are well-known, followed by their decorated versions, that yield proofs of properties of cartesian effect categories.

Cartesian weak categories {#sec:weak}
=========================

Weak categories are reminded in this section, with their notion of product. Except for the minor fact that equality is weakened as a congruence, all this section is very well known. Some detailed proofs are given in appendix \[app:proof\], with their decorated versions.

Weak categories {#subsec:weak-cat}
---------------

A weak category is like a category, except that the equations (for unitarity and associativity) hold only “up to congruence”.

\[defi:weak-cat\] A *weak category* is a graph where:

-   for each point $X$ there is a loop ${\mathrm{id}}_X:X\to X$ called the *identity* of $X$,

-   for each consecutive functions $f:X\to Y$, $g:Y\to Z$, there is a function $g\circ f:X\to Z$ called the *composition* of $f$ and $g$,

-   and there is a relation $\equiv$ between parallel functions (each $f_1\equiv f_2$ is called an *equation*), such that:

    -   $\equiv$ is a *congruence*, i.e., it is an equivalence relation and for each $f:X\to Y$, $g_1,g_2:Y\to Z$, $h:Z\to W$, if $g_1\equiv g_2$ then $g_1\circ f\equiv g_2\circ f$ (*substitution*) and $h\circ g_1 \equiv h\circ g_2$ (*replacement*),

    -   for each $f:X\to Y$, the *unitarity equations* hold: $f\circ{\mathrm{id}}_X\equiv f$ and ${\mathrm{id}}_Y\circ f\equiv f$,

    -   and for each $f:X\to Y$, $g:Y\to Z$, $h:Z\to W$, the *associativity equation* holds: $h\circ (g \circ f) \equiv (h\circ g) \circ f$.

So, a weak category is a special kind of a bicategory, and a category is a weak category where the congruence is the equality.

Products {#subsec:weak-prod}
--------

In a weak category, a *weak product*, or simply a *product*, is defined as a product “up to congruence”. We focus on nullary products (i.e., terminal points) and binary products; it is well-know that products of any arity can be recovered from those.

\[defi:weak-term\] A *(weak) terminal point* is a point $U$ (for “*Unit*”) such that for every point $X$ there is a function ${{\langle \, \rangle}}_X:X\to U$, unique up to congruence.

\[defi:weak-prod\] A *binary cone* is made of two functions with the same source ${Y_1{\stackrel{f_1}{\longleftarrow}}X{\stackrel{f_2}{\longrightarrow}}Y_2}$. A *binary (weak) product* is a binary cone ${Y_1{\stackrel{q_1}{\longleftarrow}}Y_1\times Y_2{\stackrel{q_2}{\longrightarrow}}Y_2}$ such that for every binary cone with the same base ${Y_1{\stackrel{f_1}{\longleftarrow}}X{\stackrel{f_2}{\longrightarrow}}Y_2}$ there is a function ${\langle f_1,f_2 \rangle}:X\to Y_1\times Y_2$, called the *pair* of $f_1$ and $f_2$, unique up to congruence, such that: $$q_1\circ {\langle f_1,f_2 \rangle}\equiv f_1  \;\mbox{ and }\;
 q_2\circ {\langle f_1,f_2 \rangle}\equiv f_2 \;.$$

As usual, all terminal points are isomorphic, and the fact of using $U$ for denoting a terminal point corresponds to the choice of one terminal point. Similarly, all products on a given base are isomorphic (in a suitable sense), and the notations correspond to the choice of one product for each base.

\[defi:weak-ccat\] A *cartesian weak category* is a weak category with a chosen terminal point and chosen binary products.

Products of functions {#subsec:weak-prodfn}
---------------------

\[defi:weak-arr-prod\] In a cartesian weak category, the *(weak) binary product* of two functions $f_1:X_1\to Y_1$ and $f_2:X_2\to Y_2$ is the function: $$f_1\times f_2 = {\langle f_1\circ p_1,f_2\circ p_2 \rangle}:
X_1\times X_2 \to Y_1\times Y_2 \;.$$

So, the binary product of functions is characterized, up to congruence, by the equations: $$q_1 \circ (f_1\times f_2) \equiv  f_1 \circ p_1 \;\mbox{ and }\; 
  q_2 \circ (f_1\times f_2) \equiv  f_2 \circ p_2 \;.$$ The defining equations of a pair and a product can be illustrated as follows: $$\xymatrix@C=5pc{ 
  & Y_1  \\
  X \ar[ru]^{f_1}  \ar[rd]_{f_2} \ar[r]^{{\langle f_1,f_2 \rangle}} &
    Y_1 \times Y_2 \ar[u]_{q_1} \ar[d]^{q_2}  
    \ar@{}[ld]|(.3){\equiv} \ar@{}[lu]|(.3){\equiv} \\
  & Y_2  \\
  }
  \qquad\qquad
  \xymatrix@C=5pc{ 
  X_1 \ar[r]^{f_1} & Y_1  \\
  X_1\times X_2 \ar[u]^{p_1} \ar[d]_{p_2} \ar[r]^{f_1\times f_2} 
    \ar@{}[rd]|{\equiv} \ar@{}[ru]|{\equiv } & 
    Y_1 \times Y_2 \ar[u]_{q_1} \ar[d]^{q_2}  \\
  X_2 \ar[r]^{f_2} & Y_2 \\
  }$$ So, the products are defined from the pairs (note that we use the same symbols $f_1,f_2$ for the general case $f_i:X_i\to Y_i$ and for the special case $f_i:X\to Y_i$). The other way round, the pairs can be recovered from the products and the *diagonals*, i.e., the pairs ${\langle {\mathrm{id}},{\mathrm{id}}\rangle}$; indeed, it is easy to prove that for each cone ${X_1{\stackrel{f_1}{\longleftarrow}}X{\stackrel{f_2}{\longrightarrow}}X_2}$ $${\langle f_1,f_2 \rangle} \equiv (f_1\times f_2) \circ {\langle {\mathrm{id}}_X,{\mathrm{id}}_X \rangle}\;.$$

In the following, we consider products ${X_1{\stackrel{p_1}{\longleftarrow}}X_1\times X_2{\stackrel{p_2}{\longrightarrow}}X_2}$, ${Y_1{\stackrel{q_1}{\longleftarrow}}Y_1\times Y_2{\stackrel{q_2}{\longrightarrow}}Y_2}$ and ${Z_1{\stackrel{r_1}{\longleftarrow}}Z_1\times Z_2{\stackrel{r_2}{\longrightarrow}}Z_2}$.

\[prop:weak-equiv\] For each $f_1\equiv f'_1:X_1\to Y_1$ and $f_2\equiv f'_2:X_2\to Y_2$

1.  if $X_1=X_2$ $${\langle f_1,f_2 \rangle} \equiv {\langle f'_1,f'_2 \rangle} \;,$$

2.  in all cases $$f_1 \times f_2 \equiv f'_1 \times f'_2 \;.$$

\[prop:weak-comp\] For each $f_1:X_1\to Y_1$, $f_2:X_2\to Y_2$, $g_1:Y_1\to Z_1$, $g_2:Y_2\to Z_2$

1.  if $X_1=X_2$ and $Y_1=Y_2$ and $f_1=f_2(=f)$ $${\langle g_1,g_2 \rangle} \circ f \equiv {\langle g_1\circ f,g_2\circ f \rangle} \;,$$

2.  if $X_1=X_2$ $$(g_1 \times g_2) \circ {\langle f_1,f_2 \rangle} \equiv 
          {\langle g_1\circ f_1,g_2\circ f_2 \rangle} \;,$$

3.  in all cases $$(g_1 \times g_2) \circ (f_1 \times f_2) \equiv 
       (g_1\circ f_1) \times (g_2\circ f_2) \;.$$

Let us consider the products ${X_1{\stackrel{p_1}{\longleftarrow}}X_1\times X_2{\stackrel{p_2}{\longrightarrow}}X_2}$ and ${X_2{\stackrel{p'_2}{\longleftarrow}}X_2\times X_1{\stackrel{p'_1}{\longrightarrow}}X_1}$. The *swap* function is the isomorphism: $$\gamma_{(X_1,X_2)} = {\langle p'_1,p'_2 \rangle}_{p_1,p_2} = {\langle p'_1,p'_2 \rangle}:
   X_2\times X_1\to X_1\times X_2\;,$$ characterized by: $$p_1\circ \gamma_{(X_1,X_2)}\equiv p'_1
  \;\mbox{ and }\; p_2\circ \gamma_{(X_1,X_2)}\equiv p'_2 \;.$$

\[prop:weak-swap\] For each $f_1:X_1\to Y_1$ and $f_2:X_2\to Y_2$, let $\gamma_Y=\gamma_{(Y_1,Y_2)}$ and $\gamma_X=\gamma_{(X_1,X_2)}$, then:

1.  if $X_1=X_2$ $$\gamma_Y \circ {\langle f_2,f_1 \rangle} \equiv {\langle f_1,f_2 \rangle} \;,$$

2.  in all cases $$\gamma_Y \circ (f_2\times f_1) \circ \gamma_X^{-1} \equiv 
         f_1 \times f_2 \;.$$

Let us consider the products ${X_1{\stackrel{p_1}{\longleftarrow}}X_1\times X_2{\stackrel{p_2}{\longrightarrow}}X_2}$, ${X_1\times X_2{\stackrel{p_{1,2}}{\longleftarrow}}(X_1\times X_2)\times X_3{\stackrel{p_3}{\longrightarrow}}X_3}$, ${X_2{\stackrel{p'_2}{\longleftarrow}}X_2\times X_3{\stackrel{p'_3}{\longrightarrow}}X_3}$ and ${X_1{\stackrel{p'_1}{\longleftarrow}}X_1\times (X_2\times X_3){\stackrel{p'_{2,3}}{\longrightarrow}}X_2\times X_3}$. The *associativity* function is the isomorphism: $$\alpha_{(X_1,X_2,X_3)} = 
  {\langle {\langle p'_1,p'_2\circ p'_{2,3} \rangle}_{p_1,p_2},
    p'_3\circ p'_{2,3} \rangle}_{p_{1,2},p_3}:
   X_1\times (X_2\times X_3) \to (X_1\times X_2)\times X_3\;,$$ characterized by: $$p_1\circ p_{1,2}\circ \alpha_{(X_1,X_2,X_3)} \equiv p'_1
  \,,\; 
  p_2\circ p_{1,2}\circ \alpha_{(X_1,X_2,X_3)} \equiv p'_2\circ p'_{2,3}
  \;\mbox{ and }\; 
  p_3\circ \alpha_{(X_1,X_2,X_3)} \equiv p'_3\circ p'_{2,3} \;.$$

\[prop:weak-assoc\] For each $f_1:X_1\to Y_1$, $f_2:X_2\to Y_2$ and $f_3:X_3\to Y_3$, let $\alpha_Y=\alpha_{(Y_1,Y_2,Y_3)}$ and $\alpha_X=\alpha_{(X_1,X_2,X_3)}$, then:

1.  if $X_1=X_2=X_3$ $$\alpha_Y \circ {\langle f_1,{\langle f_2,f_3 \rangle} \rangle} 
      \equiv {\langle {\langle f_1,f_2 \rangle},f_3 \rangle} \;,$$

2.  in all cases $$\alpha_Y \circ (f_1\times (f_2\times f_3)) \equiv 
         ((f_1 \times f_2)\times f_3) \circ \alpha_X \;.$$

In the definition of the binary product $f_1\times f_2$, both $f_1$ and $f_2$ play symmetric rôles. This symmetry can be broken: “first $f_1$ then $f_2$” corresponds to $({\mathrm{id}}_{Y_1}\times f_2) \circ (f_1\times{\mathrm{id}}_{X_2})$, using the intermediate product $Y_1\times X_2$, while “first $f_2$ then $f_1$” corresponds to $(f_1\times{\mathrm{id}}_{Y_2}) \circ ({\mathrm{id}}_{X_1}\times f_2)$, using the intermediate product $X_1\times Y_2$. These are called the *(left and right) sequential products* of $f_1$ and $f_2$. The three versions of the binary product of functions coincide, up to congruence; this is a kind of *parallelism* property, meaning that both $f_1$ and $f_2$ can be computed either simultaneously, or one after the other, in any order:

\[prop:weak-seq\] For each $f_1:X_1\to Y_1$ and $f_2:X_2\to Y_2$ $$f_1\times f_2 \equiv ({\mathrm{id}}_{Y_1}\times f_2) \circ (f_1\times{\mathrm{id}}_{X_2})
\equiv (f_1\times{\mathrm{id}}_{X_2}) \circ ({\mathrm{id}}_{Y_1}\times f_2) \;.$$

Cartesian effect categories {#sec:effect}
===========================

Sections \[subsec:effect-cat\] to \[subsec:effect-semifn\] form a decorated version of section \[sec:weak\]. Roughly speaking, a kind of structure is *decorated* when there is some classification of its ingredients. Here, the classification involves two kinds of functions and two kinds of equations. Effect categories are defined in section \[subsec:effect-cat\] as decorated weak categories. In section \[subsec:effect-semi\], semi-products are defined as decorated weak products, then cartesian effect category as decorated cartesian weak categories. Decorated propositions are stated here, and the corresponding decorated proofs are given in appendix \[app:proof\]. Then, in sections \[subsec:effect-seq\] and \[subsec:effect-proj\], the sequential product of functions is defined by composing semi-products, and some of its properties are derived.

Effect categories {#subsec:effect-cat}
-----------------

A *(weak) subcategory* ${\mathbf{V}}$ of a weak category ${\mathbf{C}}$ is a subcategory of ${\mathbf{C}}$ such that each equation of ${\mathbf{V}}$ is an equation of ${\mathbf{C}}$. It is a *wide (weak) subcategory* when ${\mathbf{V}}$ and ${\mathbf{C}}$ have the same points, and each equation of ${\mathbf{C}}$ between functions in ${\mathbf{V}}$ is an equation in ${\mathbf{V}}$. Then only one symbol ${\equiv}$ can be used, for both ${\mathbf{V}}$ and ${\mathbf{C}}$.

\[defi:effect-cat\] Let ${\mathbf{V}}$ be a weak category. An *effect category extending* ${\mathbf{V}}$ is a weak category ${\mathbf{C}}$, such that ${\mathbf{V}}$ is a wide subcategory of ${\mathbf{C}}$, together with a relation ${\lesssim}$ between parallel functions in ${\mathbf{C}}$ such that:

-   the relation ${\lesssim}$ is weaker than ${\equiv}$ for $f_1,f_2$ in ${\mathbf{C}}$, $\,f_1{\equiv}f_2 \Rightarrow f_1{\lesssim}f_2$;

-   ${\lesssim}$ is transitive;

-   ${\lesssim}$ and ${\equiv}$ coincide on ${\mathbf{V}}$ for $v_1,v_2$ in ${\mathbf{V}}$, $\,v_1{\equiv}v_2 \iff v_1{\lesssim}v_2$;

-   ${\lesssim}$ satisfies the substitution property:\
    if $f:X\to Y$ and $g_1{\lesssim}g_2:Y\to Z$ then $g_1\circ f{\lesssim}g_2\circ f:X\to Z$;

-   ${\lesssim}$ satisfies the replacement property *with respect to ${\mathbf{V}}$*:\
    if $g_1{\lesssim}g_2:Y\to Z$ and $v:Z\to W$ in ${\mathbf{V}}$ then $v\circ g_1 {\lesssim}v\circ g_2:Y\to W$.

The first property implies that ${\lesssim}$ is reflexive, and when ${\equiv}$ is the equality it means precisely that ${\lesssim}$ is reflexive. Since ${\lesssim}$ is transitive and weaker than ${\equiv}$, if either $f_1{\equiv}f_2{\lesssim}f_3$ or $f_1{\lesssim}f_2{\equiv}f_3$, then $f_1{\lesssim}f_3$; this is called the *compatibility* of ${\lesssim}$ with ${\equiv}$. An effect category is *strict* when ${\equiv}$ is the equality. In this paper, there is no major difference between effect categories and strict effect categories.

A *pure function* is a function in ${\mathbf{V}}$. The symbol ${\rightsquigarrow}$ is used for pure functions, and $\to$ for all functions. It follows from definition \[defi:effect-cat\] that all the identities of ${\mathbf{C}}$ are pure, the composition of pure functions is pure, and more precisely a composition of functions is pure if and only if all the composing functions are pure. It should be noted that there can be equations $f{\equiv}v$ between a non-pure function and a pure one; then the function $f$ is proved effect-free, without being pure. This “syntactic” choice could be argued; note that this situation disappears when the congruence ${\equiv}$ is the equality. The relation ${\lesssim}$ is called the *semi-congruence* of the effect category, and each $f_1{\lesssim}f_2$ is called a *semi-equation*. The semi-congruence generally is not a congruence, for two reasons: it may not be symmetric, and it may not satisfy the replacement property for all functions.

Examples of strict effect categories are given in section \[sec:exam\]. For dealing with partiality in section \[subsec:exam-partial\], the semi-congruence ${\lesssim}$ coincides with the usual ordering of partial functions, it is not symmetric but it satisfies the replacement property for all partial functions. On the other hand, in section \[subsec:exam-state\], the semi-congruence ${\lesssim}$ means that two functions in an imperative language have the same result but may act differently on the state, it is an equivalence relation that does not satisfy the replacement property for non-pure functions.

Clearly, if the decorations are forgotten, i.e., if both the distinction between pure functions and arbitrary functions and the distinction between the congruence and the semi-congruence are forgotten, then an effect category is just a weak category.

A cartesian effect category, as defined below, is an effect category where ${\mathbf{V}}$ is cartesian and where this cartesian structure on ${\mathbf{V}}$ has some kind of generalization to ${\mathbf{C}}$, that does *not*, in general, turn ${\mathbf{C}}$ into a cartesian weak category.

Semi-products {#subsec:effect-semi}
-------------

Now, let us assume that ${\mathbf{C}}$ is an effect category extending ${\mathbf{V}}$, and that ${\mathbf{V}}$ is cartesian. We define nullary and binary *semi-products* in ${\mathbf{C}}$, for building pairs of functions when at least one of them is pure.

\[defi:effect-term\] A *semi-terminal point* in ${\mathbf{C}}$ is a terminal point $U$ in ${\mathbf{V}}$ such that every function $g:X\to U$ satisfies $g{\lesssim}{{\langle \, \rangle}}_X$.

\[defi:effect-prod\] A *binary semi-product* in ${\mathbf{C}}$ is a binary product ${Y_1{\stackrel{q_1}{\leftsquigarrow}}Y_1\times Y_2{\stackrel{q_2}{\rightsquigarrow}}Y_2}$ in ${\mathbf{V}}$ such that:

-   for every binary cone with the same base ${Y_1{\stackrel{f_1}{\longleftarrow}}X{\stackrel{v_2}{\rightsquigarrow}}Y_2}$ and with $v_2$ pure, there is a function ${\langle f_1,v_2 \rangle}_{q_1,q_2}={\langle f_1,v_2 \rangle}:X\to Y_1\times Y_2$, unique up to ${\equiv}$, such that $$q_1\circ {\langle f_1,v_2 \rangle} {\equiv}f_1 \;\mbox{ and }\;  
      q_2\circ {\langle f_1,v_2 \rangle} {\lesssim}v_2 \;,$$

-   and for every binary cone with the same base ${Y_1{\stackrel{v_1}{\leftsquigarrow}}X{\stackrel{f_2}{\longrightarrow}}Y_2}$ and with $v_1$ pure, there is a function ${\langle v_1,f_2 \rangle}_{q_1,q_2}={\langle v_1,f_2 \rangle}:X\to Y_1\times Y_2$, unique up to ${\equiv}$, such that $$q_1\circ {\langle v_1,f_2 \rangle} {\lesssim}v_1 \;\mbox{ and }\;  
      q_2\circ {\langle v_1,f_2 \rangle} {\equiv}f_2 \;.$$

The defining (semi-)equations of a binary semi-product can be illustrated as follows: $$\xymatrix@C=5pc{ 
  & Y_1  \\
  X \ar@{~>}[ru]^{v_1} \ar@{~>}[rd]_{v_2} \ar@{~>}[r]^{{\langle v_1,v_2 \rangle}} &
    Y_1 \times Y_2 \ar@{~>}[u]_{q_1} \ar@{~>}[d]^{q_2}  
    \ar@{}[ld]|(.3){{\equiv}} \ar@{}[lu]|(.3){{\equiv}}\\
  & Y_2  \\
  }
  \qquad 
  \xymatrix@C=5pc{ 
  & Y_1  \\
  X \ar[ru]^{f_1}  \ar@{~>}[rd]_{v_2} \ar[r]^{{\langle f_1,v_2 \rangle}\;\;} &
    Y_1 \times Y_2 \ar@{~>}[u]_{q_1} \ar@{~>}[d]^{q_2}  
    \ar@{}[ld]|(.3){{\gtrsim}} \ar@{}[lu]|(.3){{\equiv}}\\
  & Y_2  \\
  } 
  \qquad
  \xymatrix@C=5pc{ 
  & Y_1  \\
  X \ar@{~>}[ru]^{v_1}  \ar[rd]_{f_2} \ar[r]^{{\langle v_1,f_2 \rangle}\;\;} &
    Y_1 \times Y_2 \ar@{~>}[u]_{q_1} \ar@{~>}[d]^{q_2}  
    \ar@{}[ld]|(.3){{\equiv}} \ar@{}[lu]|(.3){{\gtrsim}}\\
  & Y_2  \\
  }$$ Clearly, if the decorations are forgotten, then semi-products are just products.

The notation is not ambiguous. Indeed, if ${Y_1{\stackrel{v_1}{\leftsquigarrow}}X{\stackrel{v_2}{\rightsquigarrow}}Y_2}$ is a binary cone in ${\mathbf{V}}$, then the three definitions of the pair ${\langle v_1,v_2 \rangle}$ above coincide, up to congruence: let $t$ denote any one of the three pairs, then $t$ is characterized, up to congruence, by $q_1\circ t {\equiv}v_1$ and $q_2\circ t {\equiv}v_2$, because ${\equiv}$ and ${\lesssim}$ coincide on pure functions.

\[defi:effect-ccat\] A *cartesian effect category extending* a cartesian weak category ${\mathbf{V}}$ is an effect category extending ${\mathbf{V}}$ such that each terminal point of ${\mathbf{V}}$ is a semi-terminal point of ${\mathbf{C}}$ and each binary product of ${\mathbf{V}}$ is a binary semi-product of ${\mathbf{C}}$.

Semi-products of functions {#subsec:effect-semifn}
--------------------------

\[defi:effect-arr-prod\] In a cartesian effect category, the *binary semi-product* $f_1\times v_2$ of a function $f_1:X_1\to Y_1$ and a pure function $v_2:X_2{\rightsquigarrow}Y_2$ is the function: $$f_1\times v_2={\langle f_1\circ p_1,v_2\circ p_2 \rangle} : 
  X_1\times X_2 \to Y_1\times Y_2$$

It follows that $f_1\times v_2$ is characterized, up to ${\equiv}$, by: $$q_1 \circ (f_1\times v_2) {\equiv}f_1 \circ p_1 \;\mbox{ and }\; 
  q_2 \circ (f_1\times v_2) {\lesssim}v_2 \circ p_2$$ $$\xymatrix@C=5pc{ 
  X_1 \ar[r]^{f_1} & Y_1  \\
  X_1\times X_2 \ar@{~>}[u]^{p_1} \ar@{~>}[d]_{p_2} \ar[r]^{f_1\times v_2} 
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{{\equiv}} & 
    Y_1 \times Y_2 \ar@{~>}[u]_{q_1} \ar@{~>}[d]^{q_2}  \\
  X_2 \ar@{~>}[r]^{v_2} & Y_2 \\
  }$$ The *binary semi-product* $v_1\times f_2:X_1\times X_2\to Y_1\times Y_2$ of a pure function $v_1:X_1{\rightsquigarrow}Y_1$ and a function $f_2:X_2\to Y_2$ is defined in the symmetric way, and it is characterized, up to ${\equiv}$, by the symmetric property.

The notation is not ambiguous, because so is the notation for pairs; if $v_1$ and $v_2$ are pure functions, then the three definitions of $v_1\times v_2$ coincide, up to congruence.

Propositions about products in cartesian weak categories are called *basic* propositions. It happens that each basic proposition in section \[sec:weak\] has a *decorated* version, about semi-products of the form $f_1\times v_2$ in cartesian effect categories, that is stated below. The symmetric decorated version also holds, for semi-products of the form $v_1\times f_2$. Each function in the basic proposition is replaced either by a function or by a pure function, and each equation is replaced either by an equation (${\equiv}$) or by a semi-equation (${\lesssim}$ or ${\gtrsim}$).

In addition, in appendix \[app:proof\], the proofs of the decorated propositions are *decorated* versions of the *basic* proofs. It happens that no semi-equation appears in the decorated propositions below, but they are used in the proofs. Indeed, a major ingredient in the basic proofs is that a function ${\langle f_1,f_2 \rangle}$ or $f_1\times f_2$ is characterized, up to $\equiv$, by its projections, both up to $\equiv$. The decorated version of this property is that a function ${\langle f_1,f_2 \rangle}$ or $f_1\times f_2$, where $f_1$ or $f_2$ is pure, is characterized, up to $\equiv$, by its projections, one up to $\equiv$ *and the other one up to ${\lesssim}$*. It should be noted that even when some decorated version of a basic proposition is valid, usually not all the basic proofs can be decorated. In addition, when equations are decorated as semi-equations, some care is required when the symmetry and replacement properties are used.

\[prop:effect-equiv\] For each congruent functions $f_1{\equiv}f'_1:X\to Y_1$ and pure functions $v_2{\equiv}v'_2:X{\rightsquigarrow}Y_2$

1.  if $X_1=X_2$ $${\langle f_1,v_2 \rangle} {\equiv}{\langle f'_1,v'_2 \rangle} \;.$$

2.  in all cases $$f_1 \times v_2 {\equiv}f'_1 \times v'_2 \;.$$

\[prop:effect-comp\] For each functions $f_1:X_1\to Y_1$, $g_1:Y_1\to Z_1$ and pure functions $v_2:X_2{\rightsquigarrow}Y_2$, $w_2:Y_2{\rightsquigarrow}Z_2$

1.  if $X_1=X_2$ and $Y_1=Y_2$ and $f_1=v_2(=v)$ $${\langle g_1,w_2 \rangle} \circ f {\equiv}{\langle g_1\circ v,w_2\circ v \rangle} \;,$$

2.  if $X_1=X_2$ $$(g_1 \times w_2) \circ {\langle f_1,v_2 \rangle} {\equiv}{\langle g_1\circ f_1,w_2\circ v_2 \rangle} \;,$$

3.  in all cases $$(g_1 \times w_2) \circ (f_1 \times v_2) {\equiv}(g_1\circ f_1) \times (w_2\circ v_2) \;.$$

The swap and associativity functions are defined in the same way as in section \[sec:weak\]; they are products of projections, so that they are pure functions. It follows that the swap and associativity functions are characterized by the same equations as in section \[sec:weak\], and that they are still isomorphisms.

\[prop:effect-swap\] For each function $f_1:X\to Y_1$ and pure function $v_2:X{\rightsquigarrow}Y_2$, let $\gamma_Y=\gamma_{(Y_1,Y_2)}$ and $\gamma_X=\gamma_{(X_1,X_2)}$, then:

1.  if $X_1=X_2$ $$\gamma_Y \circ {\langle v_2,f_1 \rangle} {\equiv}{\langle f_1,v_2 \rangle} \;,$$

2.  in all cases $$\gamma_Y \circ (v_2\times f_1) \circ \gamma_X^{-1} {\equiv}f_1 \times v_2 \;.$$

\[prop:effect-assoc\] For each function $f_1:X_1\to Y_1$ and pure functions $v_2:X_2{\rightsquigarrow}Y_2$, $v_3:X_3{\rightsquigarrow}Y_3$, let $\alpha_Y=\alpha_{(Y_1,Y_2,Y_3)}$ and $\alpha_X=\alpha_{(X_1,X_2,X_3)}$, then:

1.  if $X_1=X_2=X_3$ $$\alpha_Y \circ {\langle f_1,{\langle v_2,v_3 \rangle} \rangle} 
      {\equiv}{\langle {\langle f_1,v_2 \rangle},v_3 \rangle} \;,$$

2.  in all cases: $$\alpha_Y \circ (f_1\times (v_2\times v_3)) {\equiv}((f_1 \times v_2)\times v_3) \circ \alpha_X \;.$$

The sequential product of a function $f_1:X_1\to Y_1$ and a pure function $v_2:X_2{\rightsquigarrow}Y_2$ can be defined as in section \[sec:weak\], using the intermediate products ${Y_1{\stackrel{s_1}{\leftsquigarrow}}Y_1\times X_2{\stackrel{s_2}{\rightsquigarrow}}X_2}$ and ${X_1{\stackrel{t_1}{\leftsquigarrow}}X_1\times Y_2{\stackrel{t_2}{\rightsquigarrow}}Y_2}$. It does coincide with the semi-product of $f_1$ and $v_2$, up to congruence:

\[prop:effect-seq\] For each function $f_1:X_1\to Y_1$ and pure function $v_2:X_2{\rightsquigarrow}Y_2$ $$f_1\times v_2 {\equiv}({\mathrm{id}}_{Y_1}\times v_2) \circ (f_1\times{\mathrm{id}}_{X_2})
{\equiv}(f_1\times{\mathrm{id}}_{X_2}) \circ ({\mathrm{id}}_{Y_1}\times v_2) \;.$$

Sequential products of functions {#subsec:effect-seq}
--------------------------------

It has been stated in proposition \[prop:weak-seq\] that, in a cartesian weak category, the binary product of functions coincide with both sequential products, up to congruence: $$f_1\times f_2 \equiv ({\mathrm{id}}_{Y_1}\times f_2) \circ (f_1\times{\mathrm{id}}_{X_2})
\equiv (f_1\times{\mathrm{id}}_{X_2}) \circ ({\mathrm{id}}_{Y_1}\times f_2) \;.$$ In a cartesian effect category, when $f_1$ and $f_2$ are any functions, the product $f_1\times f_2$ is not defined. But $({\mathrm{id}}_{Y_1}\times f_2) \circ (f_1\times{\mathrm{id}}_{X_2})$ and $(f_1\times{\mathrm{id}}_{X_2}) \circ ({\mathrm{id}}_{Y_1}\times f_2)$ make sense, thanks to semi-products, because identities are pure. They are called the sequential products of $f_1$ and $f_2$, and they do not coincide up to congruence, in general: parallelism is not satisfied.

\[defi:effect-seq-prod\] The *left binary sequential product* of two functions $f_1:X_1\to Y_1$ and $f_2:X_2\to Y_2$ is the function: $$f_1\ltimes f_2 = 
  ({\mathrm{id}}_{Y_1}\times f_2) \circ (f_1\times{\mathrm{id}}_{X_2}) : X_1\times X_2\to Y_1\times Y_2 \;.$$

So, the left binary sequential product is obtained from: $$\xymatrix@C=5pc{ 
  X_1 \ar[r]^{f_1} & Y_1 \ar@{~>}[r]^{{\mathrm{id}}} & Y_1  \\
  X_1\times X_2 \ar@{~>}[u]^{p_1} \ar@{~>}[d]_{p_2} 
    \ar[r]^{f_1\times {\mathrm{id}}} 
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{{\equiv}} & 
    Y_1 \times X_2 \ar@{~>}[u]^{s_1} \ar@{~>}[d]_{s_2}  
    \ar[r]^{{\mathrm{id}}\times f_2} 
    \ar@{}[rd]|{{\equiv}} \ar@{}[ru]|{{\gtrsim}} & 
    Y_1 \times Y_2 \ar@{~>}[u]^{q_1} \ar@{~>}[d]_{q_2}  \\
  X_2 \ar@{~>}[r]^{{\mathrm{id}}} & X_2 \ar[r]^{f_2} & Y_2 \\
  }$$ The left sequential product extends the semi-product:

\[prop:effect-seq-lproduct\] For each function $f_1$ and pure function $v_2$, $ f_1\ltimes v_2 {\equiv}f_1\times v_2 $.

&gt;From proposition \[prop:effect-comp\], $f_1\ltimes v_2 = ({\mathrm{id}}\times v_2) \circ (f_1\times{\mathrm{id}})
{\equiv}({\mathrm{id}}\circ f_1) \times (v_2\circ{\mathrm{id}})
{\equiv}f_1 \times v_2$.

Note that the diagonal ${\langle {\mathrm{id}}_X,{\mathrm{id}}_X \rangle}$ is a pair of pure functions. So, by analogy with the property ${\langle f_1,f_2 \rangle} \equiv (f_1\times f_2) \circ {\langle {\mathrm{id}}_X,{\mathrm{id}}_X \rangle}$ in weak categories:

\[defi:effect-seq-pair\] The *left sequential pair* of two functions $f_1:X\to Y_1$ and $f_2:X\to Y_2$ is: $${\langle f_1,f_2 \rangle}_l = (f_1\ltimes f_2) \circ {\langle {\mathrm{id}}_X,{\mathrm{id}}_X \rangle}\;.$$

The left sequential pairs do not satisfy the usual equations for pairs, as in definition \[defi:weak-prod\]. However, they satisfy some weaker properties, as stated in corollary \[cor:seq-pair\].

The *right binary sequential product* of $f_1$ and $f_2$ is defined in the symmetric way; it is the function: $$f_1\rtimes f_2 = 
  (f_1\times{\mathrm{id}}_{Y_2}) \circ ({\mathrm{id}}_{X_1}\times f_2) : 
  X_1\times X_2\to Y_1\times Y_2 \;.$$ It does also extend the product of a pure function and a function: for each pure function $v_1$, $ v_1\rtimes f_2 {\equiv}v_1\times f_2 $. The *right sequential pair* of $f_1:X\to Y_1$ and $f_2:X\to Y_2$ is: $${\langle f_1,f_2 \rangle}_r = (f_1\rtimes f_2) \circ {\langle {\mathrm{id}}_X,{\mathrm{id}}_X \rangle}\;.$$

Here are some properties of the sequential products that are easily deduced from the properties of semi-products in \[subsec:effect-semi\]. The symmetric properties also hold.

\[prop:seq-equiv\] For each congruent functions $f_1{\equiv}f'_1:X_1\to Y_1$ and $f_2{\equiv}f'_2:X_2\to Y_2$ $$f_1 \ltimes f_2 {\equiv}f'_1 \ltimes f'_2\;.$$

Clear, from \[prop:effect-equiv\].

\[prop:seq-comp\] For each functions $f_1:X_1\to Y_1$, $g_1:Y_1\to Z_1$, $g_2:Y_2\to Z_2$ and pure function $v_2:X_2{\rightsquigarrow}Y_2$ $$(g_1 \ltimes g_2) \circ (f_1 \times v_2) {\equiv}(g_1\circ f_1) \ltimes (g_2\circ v_2) \;.$$

$$\xymatrix@C=5pc{ 
  X_1 \ar[r]^{f_1} & Y_1 \ar[r]^{g_1} & Z_1 \ar@{~>}[r]^{{\mathrm{id}}} & Z_1  \\
  X_1 \times X_2 \ar@{~>}[u] \ar@{~>}[d]   \ar[r]^{f_1\times v_2} 
  \ar@{}[rd]|{{\equiv}} \ar@{}[ru]|{{\equiv}} &
  Y_1\times Y_2 \ar@{~>}[u] \ar@{~>}[d] 
    \ar[r]^{g_1\times {\mathrm{id}}} 
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{{\equiv}} & 
    Z_1 \times Y_2 \ar@{~>}[u] \ar@{~>}[d]  
    \ar[r]^{{\mathrm{id}}\times g_2} 
    \ar@{}[rd]|{{\equiv}} \ar@{}[ru]|{{\gtrsim}} & 
    Z_1 \times Z_2 \ar@{~>}[u] \ar@{~>}[d]  \\
  X_2 \ar@{~>}[r]^{v_2} & Y_2 \ar@{~>}[r]^{{\mathrm{id}}} & Y_2 \ar[r]^{g_2} & Z_2 \\
  }$$

&gt;From several applications of proposition \[prop:effect-comp\] and its symmetric version:\
$({\mathrm{id}}\times g_2) \circ (g_1\times{\mathrm{id}}) \circ (f_1 \times v_2)
{\equiv}({\mathrm{id}}\times g_2) \circ  ((g_1\circ f_1) \times v_2)
{\equiv}({\mathrm{id}}\times g_2) \circ ({\mathrm{id}}\times v_2) 
\circ ((g_1\circ f_1)\times{\mathrm{id}})
{\equiv}({\mathrm{id}}\times (g_2\circ v_2)) \circ ((g_1\circ f_1)\times{\mathrm{id}})$.

\[prop:seq-swap\] For each functions $f_1:X_1\to Y_1$ and $f_2:X_2\to Y_2$, the left and right sequential products are related by swaps: $$\gamma_Y \circ (f_2\rtimes f_1) \circ \gamma_X^{-1} {\equiv}f_1 \ltimes f_2 \;.$$

&gt;From proposition \[prop:effect-swap\] and its symmetric version:\
$ \gamma \circ ({\mathrm{id}}\times f_2) \circ (f_1\times{\mathrm{id}})
{\equiv}(f_2\times{\mathrm{id}}) \circ \gamma \circ (f_1\times{\mathrm{id}})
{\equiv}(f_2\times{\mathrm{id}}) \circ ({\mathrm{id}}\times f_1) \circ \gamma$.

\[prop:seq-assoc\] For each functions $f_1:X_1\to Y_1$, $f_2:X_2\to Y_2$ and $f_3:X_3\to Y_3$, let $\alpha_Y=\alpha_{(Y_1,Y_2,Y_3)}$ and $\alpha_X=\alpha_{(X_1,X_2,X_3)}$, then: : $$\alpha_Y \circ (f_1\ltimes (f_2\ltimes f_3)) {\equiv}((f_1 \ltimes f_2)\ltimes f_3) \circ \alpha_X \;.$$

&gt;From proposition \[prop:effect-assoc\].

Projections of sequential products {#subsec:effect-proj}
----------------------------------

Let us come back to a weak category, as in section \[sec:weak\]. The binary product of functions is characterized, up to congruence, by the equations: $$q_1 \circ (f_1\times f_2) \equiv  f_1 \circ p_1 \;\mbox{ and }\; 
  q_2 \circ (f_1\times f_2) \equiv  f_2 \circ p_2 \;,$$ so that for all constant functions $x_1:U\to X_1$ and $x_2:U\to X_2$ $$q_1 \circ (f_1\times f_2) \circ {\langle x_1,x_2 \rangle} \equiv f_1 \circ x_1 
\;\mbox{ and }\; 
  q_2 \circ (f_1\times f_2) \circ {\langle x_1,x_2 \rangle} \equiv f_2 \circ x_2 \;.$$ In a cartesian effect category, it is proved in theorem \[thm:seq-prod\] that $f_1\ltimes f_2$, when applied to a pair of constant pure functions ${\langle x_1,x_2 \rangle}$, returns on the $Y_1$ side a function that is semi-congruent to $f_1(x_1)$, and on the $Y_2$ side a function that is congruent to $f_2\circ x_2\circ {{\langle \, \rangle}}\circ f_1\circ x_1$, which means “first $f_1(x_1)$, then forget the result, then $f_2(x_2)$”. More precise statements are given in propositions \[prop:seq-val\] and \[prop:seq-com\]. Proofs are presented in the same formalized way as in appendix \[app:proof\].

As above, we consider the semi-terminal point $U$ and semi-products\
${X_1{\stackrel{p_1}{\leftsquigarrow}}X_1\times X_2{\stackrel{p_2}{\rightsquigarrow}}X_2}$, ${Y_1{\stackrel{q_1}{\leftsquigarrow}}Y_1\times Y_2{\stackrel{q_2}{\rightsquigarrow}}Y_2}$ and ${Y_1{\stackrel{s_1}{\leftsquigarrow}}Y_1\times X_2{\stackrel{s_2}{\rightsquigarrow}}X_2}$.

\[prop:seq-val\] For each functions $f_1:X_1\to Y_1$ and $f_2:X_2\to Y_2$ $$q_1\circ (f_1\ltimes f_2) {\lesssim}f_1\circ p_1 : X_1\times X_2\to Y_1\;.$$

$$\xymatrix@C=5pc{ 
  X_1 \ar[r]^{f_1} & Y_1 \ar@{~>}[r]^{{\mathrm{id}}} & Y_1  \\
  X_1\times X_2 \ar@{~>}[u]^{p_1} 
    \ar[r]^{f_1\times {\mathrm{id}}} 
    \ar@{}[ru]|{{\equiv}} \ar@/_4ex/[rr]_{f_1\ltimes f_2}^{=} & 
    Y_1 \times X_2 \ar@{~>}[u]^{s_1}   
    \ar[r]^{{\mathrm{id}}\times f_2} 
    \ar@{}[ru]|{{\gtrsim}} & 
    Y_1 \times Y_2 \ar@{~>}[u]^{q_1} \\
  }$$

\

  ------- ------------------------------------------------------------------------- ----------------------------------------
    $(a)$ $q_1\circ ({\mathrm{id}}\times f_2) {\lesssim}s_1$                        
    $(b)$ $q_1\circ (f_1\ltimes f_2) {\lesssim}s_1\circ (f_1\times{\mathrm{id}})$   $(a)$, ${\mathit{subst}}_{{\lesssim}}$
    $(c)$ $s_1\circ (f_1\times{\mathrm{id}}) {\equiv}f_1\circ p_1$                  
    $(d)$ $q_1\circ (f_1\ltimes f_2) {\lesssim}f_1\circ p_1$                        $(b)$, $(c)$, ${\mathit{comp}}$
  ------- ------------------------------------------------------------------------- ----------------------------------------

\

\[lem:seq-terminal\] For each function $f_1:X_1\to Y_1$ and pure function $x_2:U{\rightsquigarrow}X_2$ $${\langle {\mathrm{id}}_{Y_1},x_2\circ{{\langle \, \rangle}}_{Y_1} \rangle}\circ f_1 {\equiv}{\langle f_1,x_2\circ{{\langle \, \rangle}}_{X_1} \rangle}
  :  X_1 \to Y_1\times X_2 \;.$$

Both handsides can be illustrated as follows: $$\xymatrix@C=5pc{ 
  & Y_1 \ar@{~>}[r]^{{\mathrm{id}}} & Y_1  \\
  X_1 \ar[r]^{f_1} & Y_1 \ar@{=}[u] \ar@{~>}[d]_{{{\langle \, \rangle}}}  
    \ar@{~>}[r]^{{\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}}
    \ar@{}[rd]|{{\equiv}} \ar@{}[ru]|{{\equiv}} & 
    Y_1 \times X_2 \ar@{~>}[u]^{s_1} \ar@{~>}[d]_{s_2}  \\
  & U \ar@{~>}[r]^{x_2} & X_2 \\
  } \qquad \xymatrix@C=5pc{ 
  X_1 \ar[r]^{f_1} & Y_1  \\
  X_1 \ar@{=}[u] \ar@{~>}[d]_{{{\langle \, \rangle}}}  
    \ar[r]^{{\langle f_1,x_2\circ{{\langle \, \rangle}}\rangle}}
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{{\equiv}} & 
    Y_1 \times X_2 \ar@{~>}[u]^{s_1} \ar@{~>}[d]_{s_2}  \\
  U \ar@{~>}[r]^{x_2} & X_2 \\
  }$$

\

  --------- -------------------------------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------
    $(a_1)$ $s_1\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle} {\equiv}{\mathrm{id}}$                                         
    $(b_1)$ $s_1\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1 {\equiv}f_1$                                          $(a_1)$, ${\mathit{subst}}_{{\equiv}}$
    $(a_2)$ $s_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle} {\equiv}x_2\circ{{\langle \, \rangle}}$                        
    $(b_2)$ $s_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1 {\equiv}x_2\circ{{\langle \, \rangle}}\circ f_1$      $(a_2)$, ${\mathit{subst}}_{{\equiv}}$
    $(c_2)$ ${{\langle \, \rangle}}\circ f_1 {\lesssim}{{\langle \, \rangle}}$                                                                     semi-terminality of $U$
    $(d_2)$ $x_2\circ{{\langle \, \rangle}}\circ f_1{\lesssim}x_2\circ{{\langle \, \rangle}}$                                                      $(c_2)$, ${\mathit{repl}}_{{\lesssim}}$ ($x_2$ is pure)
    $(e_2)$ $s_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1 {\lesssim}x_2\circ{{\langle \, \rangle}}$             $(b_2)$, $(d_2)$, ${\mathit{trans}}_{{\lesssim}}$
      $(f)$ ${\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1 {\equiv}{\langle f_1,x_2\circ{{\langle \, \rangle}}\rangle}$   $(b_1)$, $(e_2)$
  --------- -------------------------------------------------------------------------------------------------------------------------------------- ---------------------------------------------------------

\

\[prop:seq-com\] For each functions $f_1:X_1\to Y_1$, $f_2:X_2\to Y_2$ and pure function $x_2:U{\rightsquigarrow}X_2$ $$q_2 \circ (f_1\ltimes f_2) \circ {\langle {\mathrm{id}}_{X_1},x_2\circ {{\langle \, \rangle}}_{X_1} \rangle}
{\equiv}f_2 \circ x_2 \circ {{\langle \, \rangle}}_{Y_1} \circ f_1 : X_1\to Y_2 \;.$$

Both handsides can be illustrated as follows: $$\xymatrix@C=3pc{ 
  X_1 \ar@{~>}[r]^{{\mathrm{id}}} & X_1 & &  \\
  X_1 \ar@{=}[u] \ar@{~>}[d]_{{{\langle \, \rangle}}} 
    \ar@{~>}[r]^{{\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\;} &
    X_1 \times X_2  \ar@/^4ex/[rr]^{f_1\ltimes f_2}_{=} 
    \ar@{~>}[u]_{p_1} \ar@{~>}[d]^{p_2} \ar[r]^{f_1\times{\mathrm{id}}}
    \ar@{}[ld]|{{\equiv}} \ar@{}[lu]|{{\equiv}} \ar@{}[rd]|{{\gtrsim}} & 
    Y_1 \times X_2 \ar@{~>}[d]^{s_2} \ar[r]^{{\mathrm{id}}\times f_2} 
    \ar@{}[rd]|{{\equiv}} & 
    Y_1 \times Y_2 \ar@{~>}[d]^{q_2}  \\
  U \ar@{~>}[r]^{x_2} & X_2 \ar@{~>}[r]^{{\mathrm{id}}} & X_2 \ar[r]^{f_2} & Y_2  \\
  } \quad 
  \xymatrix@C=2pc{ 
  \mbox{ } \\
  X_1 \ar[r]^{f_1} & Y_1 \ar@{~>}[d]_{{{\langle \, \rangle}}}  \\
  & U \ar@{~>}[r]^{x_2} & X_2 \ar[r]^{f_2} & Y_2  \\
  }$$

\

  ------- ---------------------------------------------------------------------------------------------------------------------------- --------------------------------------------------------------------
    $(a)$ $q_2\circ ({\mathrm{id}}\times f_2) {\equiv}f_2\circ s_2$                                                                    

    $(b)$ $q_2\circ (f_1\ltimes f_2) \circ  {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}                             $(a)$, ${\mathit{subst}}_{{\equiv}}$
            {\equiv}f_2\circ s_2\circ (f_1\times{\mathrm{id}}) \circ {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}$   

    $(c)$ $(f_1\times{\mathrm{id}}) \circ {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}                               prop. \[prop:effect-comp\]
            {\equiv}{\langle f_1,x_2\circ{{\langle \, \rangle}}\rangle}$                                                               

    $(d)$ ${\langle f_1,x_2\circ{{\langle \, \rangle}}\rangle}                                                                         lemma \[lem:seq-terminal\]
            {\equiv}{\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1$                                            

    $(e)$ $(f_1\times{\mathrm{id}}) \circ {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}                               $(c)$, $(d)$, ${\mathit{trans}}_{{\equiv}}$
            {\equiv}{\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1$                                            

    $(f)$ $f_2\circ s_2\circ (f_1\times{\mathrm{id}}) \circ {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}             $(e)$, ${\mathit{repl}}_{{\equiv}}$
            {\equiv}f_2\circ s_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1$                          

    $(g)$ $q_2\circ (f_1\ltimes f_2) \circ  {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}                             $(b)$, $(f)$, ${\mathit{trans}}_{{\equiv}}$
            {\equiv}f_2\circ s_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1$                          

    $(h)$ $p_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}  {\equiv}x_2\circ {{\langle \, \rangle}}$            

    $(i)$ $f_2\circ s_2\circ {\langle {\mathrm{id}},x_2\circ{{\langle \, \rangle}}\rangle}\circ f_1                                    $(h)$, ${\mathit{subst}}_{{\equiv}}$, ${\mathit{repl}}_{{\equiv}}$
            {\equiv}f_2\circ x_2\circ {{\langle \, \rangle}}\circ f_1 $                                                                

    $(j)$ $q_2\circ (f_1\ltimes f_2) \circ  {\langle {\mathrm{id}},x_2\circ {{\langle \, \rangle}}\rangle}                             $(g)$, $(i)$, ${\mathit{trans}}_{{\equiv}}$
            {\equiv}f_2\circ x_2\circ {{\langle \, \rangle}}\circ f_1$                                                                 
  ------- ---------------------------------------------------------------------------------------------------------------------------- --------------------------------------------------------------------

\

\[thm:seq-prod\] For each functions $f_1:X_1\to Y_1$, $f_2:X_2\to Y_2$ and pure functions $x_1:U{\rightsquigarrow}X_1$ and $x_2:U{\rightsquigarrow}X_2$, the function $(f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle}$ satisfies: $$q_1 \circ (f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle} 
  {\lesssim}f_1 \circ x_1 \;\mbox{ and }\;
   q_2 \circ (f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle} 
  {\equiv}f_2 \circ x_2 \circ {{\langle \, \rangle}}_{Y_1} \circ f_1 \circ x_1 \;.$$

$$\xymatrix@C=3pc{ 
  U \ar@{=}[d] \ar@{~>}[rr]^{x_1} && X_1 \ar[rrr]^{f_1} &&& Y_1 \\
  U \ar@{=}[d] \ar@{~>}[rr]^{{\langle x_1,x_2 \rangle}} && 
    X_1\times X_2 \ar[rrr]^{f_1\ltimes f_2} 
    \ar@{}[ru]|{{\gtrsim}} \ar@{}[rd]|{{\equiv}} &&& 
    Y_1 \times Y_2 \ar@{~>}[u]_{q_1} \ar@{~>}[d]^{q_2} \\
  U \ar@{~>}[r]^{x_1} & X_1 \ar[r]^{f_1} & Y_1 \ar@{~>}[r]^{{{\langle \, \rangle}}}
  & U \ar@{~>}[r]^{x_2} & X_2 \ar[r]^{f_2} & Y_2 \\
  }$$

\

  --------- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------
    $(a_1)$ $q_1\circ (f_1\ltimes f_2) {\lesssim}f_1\circ p_1$                                                                                                                                            prop. \[prop:seq-val\]

    $(b_1)$ $q_1\circ (f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle}                                                                                                                                    $(a_1)$, ${\mathit{subst}}_{{\lesssim}}$
            {\lesssim}f_1\circ p_1 \circ {\langle x_1,x_2 \rangle}$                                                                                                                                       

    $(c_1)$ $p_1 \circ {\langle x_1,x_2 \rangle}{\equiv}x_1$                                                                                                                                              (on values)

    $(d_1)$ $f_1\circ p_1 \circ {\langle x_1,x_2 \rangle}{\equiv}f_1\circ x_1$                                                                                                                            $(c_1)$, ${\mathit{repl}}_{{\equiv}}$

    $(e_1)$ $q_1 \circ (f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle}                                                                                                                                   $(b_1)$, $(d_1)$, ${\mathit{comp}}$
              {\lesssim}f_1 \circ x_1$                                                                                                                                                                    

    $(a_2)$ ${\langle x_1,x_2 \rangle} {\equiv}{\langle {\mathrm{id}}_{X_1},x_2\circ {{\langle \, \rangle}}_{X_1} \rangle} \circ x_1$                                                                     (on values)

    $(b_2)$ $q_2 \circ (f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle} {\equiv}q_2 \circ (f_1\ltimes f_2) \circ {\langle {\mathrm{id}}_{X_1},x_2\circ {{\langle \, \rangle}}_{X_1} \rangle} \circ x_1$   $(a_2)$, ${\mathit{repl}}_{{\equiv}}$

    $(c_2)$ $q_2 \circ (f_1\ltimes f_2) \circ {\langle {\mathrm{id}}_{X_1},x_2\circ {{\langle \, \rangle}}_{X_1} \rangle}                                                                                 prop. \[prop:seq-com\]
            {\equiv}f_2 \circ x_2 \circ {{\langle \, \rangle}}_{Y_1} \circ f_1$                                                                                                                           

    $(d_2)$ $q_2 \circ (f_1\ltimes f_2) \circ {\langle {\mathrm{id}}_{X_1},x_2\circ {{\langle \, \rangle}}_{X_1} \rangle}                                                                                 $(c_2)$, ${\mathit{subst}}_{{\equiv}}$
            \circ x_1                                                                                                                                                                                     
            {\equiv}f_2 \circ x_2 \circ {{\langle \, \rangle}}_{Y_1} \circ f_1\circ x_1$                                                                                                                  

    $(e_2)$ $q_2 \circ (f_1\ltimes f_2) \circ {\langle x_1,x_2 \rangle} {\equiv}f_2 \circ x_2 \circ {{\langle \, \rangle}}_{Y_1} \circ f_1\circ x_1$                                                      $(b_2)$, $(d_2)$, ${\mathit{trans}}_{{\equiv}}$
  --------- --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- -------------------------------------------------

\

The corresponding properties of left sequential pairs easily follow.

\[cor:seq-pair\] For each functions $f_1:X\to Y_1$, $f_2:X\to Y_2$ and pure function $x:U{\rightsquigarrow}X$ $$q_1\circ {\langle f_1,f_2 \rangle}_l {\lesssim}f_1 \,\mbox{, hence }\,
  q_1\circ {\langle f_1,f_2 \rangle}_l\circ x {\lesssim}f_1\circ x 
  \,\mbox{, and }\, q_2\circ {\langle f_1,f_2 \rangle}_l\circ x {\equiv}f_2 \circ x \circ {{\langle \, \rangle}}_{Y_1} \circ f_1 \circ x \;.$$

Effect categories and Arrows {#sec:related}
============================

Starting from [@Moggi91; @Wadler93], *monads* are used in Haskell for dealing with computational effects. A *Monad type* in Haskell is a unary type constructor that corresponds to a *strong monad*, in the categorical sense. Monads have been generalized on the categorical side to *Freyd categories* [@PowerRobinson97] and on the functional programming side to *Arrows* [@Hughes00]. A precise statement of the facts that Arrows generalize Monads and that Arrows are Freyd categories can be found in [@HeunenJacobs06], where each of the three notions is seen as a monoid in a relevant category. Now we prove that cartesian effect categories determine Arrows. In section \[sec:exam\] our approach is compared with the Monads approach, for two fundamental examples. In this section, all effect categories are strict: the congruence ${\equiv}$ is the equality.

Arrows {#subsec:related-arrows}
------

According to [@Paterson01], Arrows in Haskell are defined as follows.

\[defi:related-arr\] An *Arrow* is a binary type constructor class ${\mathtt{A}}$ of the form:

999 = 999 = 999 `class Arrow {\mathtt{A}} where`\
${\mathtt{arr}}:: (X\to Y)\to {\mathtt{A}}\;X\;Y$\
$({>\!\!>\!\!>}):: {\mathtt{A}}\;X\;Y \to {\mathtt{A}}\;Y\;Z \to {\mathtt{A}}\;X\;Z$\
${\mathtt{first}}:: {\mathtt{A}}\;X\;Y \to {\mathtt{A}}\;(X,Z)\;(Y,Z)$\

satisfying the following equations:

  ----- ------------------------------------------------------------------------------------------------ --- -------------------------------------------------------------------------------
   (1)                                                   ${\mathtt{arr}}\; {\mathrm{id}}{>\!\!>\!\!>}f $  =  $ f$
   (2)                                                   $f {>\!\!>\!\!>}{\mathtt{arr}}\; {\mathrm{id}}$  =  $ f$
   (3)                                                              $(f {>\!\!>\!\!>}g) {>\!\!>\!\!>}h $  =  $ f {>\!\!>\!\!>}(g {>\!\!>\!\!>}h)$
   (4)                                                                          ${\mathtt{arr}}\;(w.v) $  =  $ {\mathtt{arr}}\; v {>\!\!>\!\!>}{\mathtt{arr}}\; w$
   (5)                                                        ${\mathtt{first}}\; ({\mathtt{arr}}\; v) $  =  $ {\mathtt{arr}}\; (v\times{\mathrm{id}})$
   (6)                                                           ${\mathtt{first}}\;(f {>\!\!>\!\!>}g) $  =  $ {\mathtt{first}}\; f {>\!\!>\!\!>}{\mathtt{first}}\; g$
   (7)                     ${\mathtt{first}}\; f {>\!\!>\!\!>}{\mathtt{arr}}\; ({\mathrm{id}}\times v) $  =  $ {\mathtt{arr}}\; ({\mathrm{id}}\times v) {>\!\!>\!\!>}{\mathtt{first}}\; f$
   (8)                               ${\mathtt{first}}\; f {>\!\!>\!\!>}{\mathtt{arr}}\; {\mathtt{fst}}$  =  $ {\mathtt{arr}}\; {\mathtt{fst}}{>\!\!>\!\!>}f$
   (9)    $\;\;{\mathtt{first}}\; ({\mathtt{first}}\; f) {>\!\!>\!\!>}{\mathtt{arr}}\; {\mathtt{assoc}}$  =  $ {\mathtt{arr}}\; {\mathtt{assoc}}{>\!\!>\!\!>}{\mathtt{first}}\; f$
  ----- ------------------------------------------------------------------------------------------------ --- -------------------------------------------------------------------------------

where the functions $(\times)$, ${\mathtt{fst}}$ and ${\mathtt{assoc}}$ are defined as: $$\begin{array}{lll}
(\times) :: & (X\to X')\to(Y\to Y')\to (X,Y)\to (X',Y') &
(f\times g)(x,y)=(f\;x,g\;y) \\
{\mathtt{fst}}:: & (X,Y)\to X &
{\mathtt{fst}}(x,y)=x \\
({\mathtt{assoc}}) :: & ((X,Y),Z)\to (X,(Y,Z)) &
{\mathtt{assoc}}((x,y),z) = (x,(y,z)) \\
\end{array}$$

Cartesian effect categories determine Arrows {#subsec:related-cec-arr}
--------------------------------------------

Let ${\mathbf{V}}_H$ denote the category of Haskell types and ordinary functions, so that the Haskell notation $\mathtt{(X\to Y)}$ represents ${\mathbf{V}}_H(X,Y)$, made of the Haskell ordinary functions from $X$ to $Y$. An arrow ${\mathtt{A}}$ contructs a type ${\mathtt{A}}\;X\;Y$ for all types $X$ and $Y$. We slightly modify the definition of Arrows by allowing $\mathtt{(X\to Y)}$ to represent ${\mathbf{V}}(X,Y)$ for any cartesian category ${\mathbf{V}}$ and by requiring that ${\mathtt{A}}\;X\;Y$ is a set rather than a type. In addition, we use categorical notations instead of Haskell syntax.

So, from now on, for any cartesian category ${\mathbf{V}}$, an *Arrow $A$ on ${\mathbf{V}}$* associates to each points $X$, $Y$ of ${\mathbf{V}}$ a set $A(X,Y)$, together with three operations:

999 = 999 = 999 ${\mathtt{arr}}: {\mathbf{V}}(X,Y)\to A(X,Y)$\
${>\!\!>\!\!>}: A(X,Y) \to A(Y,Z) \to A(X,Z)$\
${\mathtt{first}}: A(X,Y) \to A(X\times Z,Y\times Z)$\

that satisfy the equations (1)-(9).

Basically, the correspondence between a cartesian effect category ${\mathbf{C}}$ extending ${\mathbf{V}}$ and an Arrow $A$ on ${\mathbf{V}}$ identifies ${\mathbf{C}}(X,Y)$ with $A(X,Y)$ for all types $X$ and $Y$. More precisely:

\[thm:related-arr\] Every cartesian effect category ${\mathbf{C}}$ extending ${\mathbf{V}}$ gives rise to an Arrow $A$ on ${\mathbf{V}}$, according to the following table:

The first and second line in the table say that $A(X,Y)$ is made of the functions from $X$ to $Y$ in ${\mathbf{C}}$ and that ${\mathtt{arr}}$ is the convertion from pure functions to arbitrary functions. The third and fourth lines say that ${>\!\!>\!\!>}$ is the (reverse) composition of functions and that ${\mathtt{first}}$ is the semi-product with the identity. Let us check that $A$ is an Arrow; the following table translates each property (1)-(9) in terms of cartesian effect categories (where $\rho_X:X\times U \to X$ is the projection), and gives the argument for its proof.

  ----- ----------------------------------------------------------------- --- --------------------------------------------------------- --------------------------------------------------
   (1)                                             $f\circ {\mathrm{id}}$  =  $f$                                                       unitarity in ${\mathbf{C}}$
   (2)                                           $ {\mathrm{id}}\circ f $  =  $f$                                                       unitarity in ${\mathbf{C}}$
   (3)                                               $h\circ (g\circ f) $  =  $ (h\circ g)\circ f $                                     associativity in ${\mathbf{C}}$
   (4)                                       $w\circ v$ in ${\mathbf{V}}$  =  $w\circ v$ in ${\mathbf{C}}$                              ${\mathbf{V}}\subseteq{\mathbf{C}}$ is a functor
   (5)                           $v\times{\mathrm{id}}$ in ${\mathbf{V}}$  =  $ v\times{\mathrm{id}}$ in ${\mathbf{C}}$                 non-ambiguity of “$\times$”
   (6)                                    $(g\circ f)\times{\mathrm{id}}$  =  $ (g\times{\mathrm{id}})\circ (f\times{\mathrm{id}})$     proposition \[prop:effect-comp\]
   (7)            $({\mathrm{id}}\times v) \circ (f\times{\mathrm{id}}) $  =  $ (f\times{\mathrm{id}}) \circ ({\mathrm{id}}\times v)$   proposition \[prop:effect-comp\]
   (8)                              $\rho\circ (f\times{\mathrm{id}}_U) $  =  $ f\circ \rho$                                            definition \[defi:effect-arr-prod\]
   (9)    $\alpha^{-1}\circ ((f\times{\mathrm{id}})\times{\mathrm{id}}) $  =  $ (f\times{\mathrm{id}})\circ\alpha^{-1}$                 proposition \[prop:effect-assoc\]
  ----- ----------------------------------------------------------------- --- --------------------------------------------------------- --------------------------------------------------

The translation of the Arrow combinators follows easily, using ${\langle f,g \rangle}_l=(f\ltimes g) \circ {\langle {\mathrm{id}},{\mathrm{id}}\rangle}$ as in section \[subsec:effect-seq\]:

  --------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------------------------------------------
                  $ (id \times f) = \gamma \circ (f \times id)  \circ \gamma  $                  ${\mathtt{second}}\;f  = {\mathtt{arr}}\;{\mathtt{swap}}{>\!\!>\!\!>}{\mathtt{first}}\;f {>\!\!>\!\!>}{\mathtt{arr}}\;{\mathtt{swap}}$
             $f \ltimes g  =  ({\mathrm{id}}\times g) \circ (f\times{\mathrm{id}})$                                           $f {*\!\!*\!\!*}g = {\mathtt{first}}\;f {>\!\!>\!\!>}{\mathtt{second}}\;g $
   ${\langle f,g \rangle}_l = (f\ltimes g) \circ {\langle {\mathrm{id}},{\mathrm{id}}\rangle}$                   $f {\&\!\!\&\!\!\&}g  = {\mathtt{arr}}(\lambda b \rightarrow (b,b)) {>\!\!>\!\!>}(f {*\!\!*\!\!*}g) $
  --------------------------------------------------------------------------------------------- ----------------------------------------------------------------------------------------------------------------------------------------

For instance, in [@Hughes00], the author states that ${\&\!\!\&\!\!\&}$ is not a categorical product since in general $(f {\&\!\!\&\!\!\&}g) {>\!\!>\!\!>}{\mathtt{arr}}\;{\mathtt{fst}}$ is different from $f$. We can state this more precisely in the effect category, where $(f {\&\!\!\&\!\!\&}g) {>\!\!>\!\!>}{\mathtt{arr}}\;{\mathtt{fst}}$ corresponds to $q_1 \circ {\langle f,g \rangle}_l $. Indeed, according to corollary \[cor:seq-pair\]: $$q_1 \circ {\langle f,g \rangle}_l  {\lesssim}f \;.$$

Examples {#sec:exam}
========

Here are presented some examples of strict cartesian effect categories. Several versions are given, some of them rely on monads.

Partiality {#subsec:exam-partial}
----------

Let ${\mathbf{V}}={\mathbf{Set}}$ be the category of sets and maps, and ${\mathbf{C}}={\mathbf{Part}}$ the category of sets and partial maps, so that ${\mathbf{V}}$ is a wide subcategory of ${\mathbf{C}}$. Let ${\lesssim}$ denote the usual ordering on partial maps: $f{\lesssim}g$ if and only if ${\mathcal{D}}(f)\subseteq{\mathcal{D}}(g)$ (where ${\mathcal{D}}$ denotes the domain of definition) and $f(x)=g(x)$ for all $x\in{\mathcal{D}}(f)$. The restriction of ${\lesssim}$ to ${\mathbf{V}}$ is the equality of total maps. Clearly ${\lesssim}$ is not symmetric, but it satisfies all the other properties of a congruence, in particular the replacement property with respect to all maps. So, ${\lesssim}$ is a semi-congruence (which satisfies replacement), that makes ${\mathbf{C}}$ a strict effect category extending ${\mathbf{V}}$. *Warning:* usually the notations are $v:X\to Y$ for a total map and $f:X{\rightharpoonup}Y$ for a partial map, but here we use respectively $v:X{\rightsquigarrow}Y$ (total) and $f:X\to Y$ (partial).

Let us define the pair ${\langle f,v \rangle}$ of a partial map $f:X\to Y_1$ and a total map $v:X{\rightsquigarrow}Y_2$ as the partial map ${\langle f,v \rangle}:X\to Y_1\times Y_2$ with the same domain of definition as $f$ and such that ${\langle f,v \rangle}(x)={\langle f(x),v(x) \rangle}$ for all $x\in{\mathcal{D}}(f)$. It is easy to check that we get a cartesian effect category. For illustrating the semi-product $f\times v$, there are two cases: either $f(x_1)$ is defined, or not, in which case we note $f(x_1)=\bot$. We use the traditional notation $\xymatrix@=1.5pc{ x \ar@{|->}[r]^{f} & y \\ }$ when $y=f(x)$ and its analog $\xymatrix@=1.5pc{ x \ar@{|~>}[r]^{v} & y \\ }$ when $y=v(x)$ and $v$ is pure. $$\xymatrix@C=5pc{ 
  x_1 \ar@{|->}[r]^{f} & y_1  \\
  {\langle x_1,x_2 \rangle} \ar@{|~>}[u] \ar@{|~>}[d] \ar@{|->}[r]^{f\times v} 
    \ar@{}[rd]|{=} \ar@{}[ru]|{=} & 
    {\langle y_1,y_2 \rangle} \ar@{|~>}[u] \ar@{|~>}[d]  \\
  x_2 \ar@{|~>}[r]^{v} & y_2 \\
  }  \qquad \mbox{ or }\qquad
   \xymatrix@C=5pc{ 
  x_1 \ar@{|->}[r]^{f} & \bot  \\
  {\langle x_1,x_2 \rangle} \ar@{|~>}[u] \ar@{|~>}[d] \ar@{|->}[r]^{f\times v} 
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{=} & 
    \bot \ar@{|~>}[u] \ar@{|~>}[d]  \\
  x_2 \ar@{|~>}[r]^{v} & y_2\ne \bot \\
  }$$

It can be noted that, in the previous example, ${\mathbf{C}}$ is a 2-category, with a 2-cell from $f$ to $g$ if and only if $f{\lesssim}g$. More generally, let ${\mathbf{C}}$ be a 2-category and ${\mathbf{V}}$ a sub-2-category where the unique 2-cells are the identities. Then by defining $f{\lesssim}g$ whenever there is a 2-cell from $f$ to $g$, we get a strict effect category. In such effect categories, the replacement property holds with respect to all functions in ${\mathbf{C}}$, but the semi-congruence is usually not symmetric.

Let us come back to the partiality example, from the slightly different point of view of the *Maybe monad*. First, let us present this point of view in a naive way, without monads. Let $U=\{\bot\}$ be a singleton, let “$+$” denote the disjoint union of sets, and for each set $X$ let $GX=X+U$ and let $\eta_X:X\to GX$ be the inclusion. Each partial map $f$ from $X$ to $Y$ can be extended as a total map $Gf$ from $X$ to $GY$, such that $Gf(x)=f(x)$ for $x\in{\mathcal{D}}(f)$ and $Gf(x)=\bot$ otherwise. This defines a bijection between the partial maps from $X$ to $Y$ and the total maps from $X$ to $GY$. Let ${\mathbf{C}}$ be the category such that its points are the sets, and a function $X\to Y$ in ${\mathbf{C}}$ is a function $X\to GY$ in ${\mathbf{Set}}$; we say that $X\to Y$ in ${\mathbf{C}}$ *stands for* $X\to GY$ in ${\mathbf{Set}}$. Let $J:{\mathbf{Set}}\to{\mathbf{C}}$ be the functor that is the identity on points and associates to each map $v_0:X\to Y$ the map $\eta_Y\circ v_0$. Let ${\mathbf{V}}=J({\mathbf{Set}})$. Then ${\mathbf{V}}$ is a wide subcategory of ${\mathbf{C}}$. For all $f,g:X\to Y$ in ${\mathbf{C}}$, that stand for $f,g:X\to GY$ in ${\mathbf{Set}}$, let: $$f{\lesssim}g \iff \forall x\in X\; (f(x)\ne\bot\Rightarrow (g(x)\ne\bot \wedge g(x)=f(x))\;.$$ This yields a strict effect category ${\mathbf{C}}$ extending ${\mathbf{V}}$, with the semi-congruence ${\lesssim}$, and as above the replacement property holds with respect to all functions in ${\mathbf{C}}$ but ${\lesssim}$ is not symmetric. Let $f:X\to Y_1$ in ${\mathbf{C}}$ and $v:X\to Y_2$ in ${\mathbf{V}}$, they stand respectively for $f:X\to GY_1$ and $v=\eta_{Y_2}\circ v_0$ with $v_0:X\to Y_2$. Then, in ${\mathbf{Set}}$, the pair ${\langle f,v_0 \rangle}:X\to GY_1 \times Y_2$ can be composed with: $$t:GY_1\times Y_2=(Y_1+U)\times Y_2\to (Y_1\times Y_2)+U =G(Y_1\times Y_2)\;,$$ that maps ${\langle y_1,y_2 \rangle}$ to itself and ${\langle \bot,y_2 \rangle}$ to $\bot$. Now, let ${\langle f,v \rangle}:X\to Y_1\times Y_2$ in ${\mathbf{C}}$ stand for ${\langle f,v \rangle}=t\circ {\langle f,v_0 \rangle}:X\to G(Y_1\times Y_2)$ in ${\mathbf{Set}}$. Then ${\langle f,v \rangle}$ is a semi-product, so that ${\mathbf{C}}$ is a cartesian effect category. The diagrams for illustrating the semi-product $f\times v$ are the same as above.

This point of view can also be presented using the the *Maybe monad* for managing failures, as follows. We have defined a functor $G:{\mathbf{Part}}\to{\mathbf{Set}}$, that is a right adjoint to the inclusion functor $I:{\mathbf{Set}}\subseteq{\mathbf{Part}}$. The corresponding monad has endofunctor $M=GI$ on ${\mathbf{Set}}$, the category ${\mathbf{C}}$ is the Kleisli category of $M$, and $J:{\mathbf{Set}}\to{\mathbf{C}}$ is the canonical functor associated to the monad. In addition, this monad $M$ is *strong*, and $t$ is the $(Y_1,Y_2)$ component of the *strength* of $M$. But the definition of the semi-congruence ${\lesssim}$, as above, is not part of the usual framework of monads.

State {#subsec:exam-state}
-----

Let ${\mathbf{V}}_0$ be a cartesian category, with a distinguished point $S$ for “the type of states”; for all $X$, let $\pi_X:S\times X\to X$ denotes the projection. Let ${\mathbf{C}}$ be the category with the same points as ${\mathbf{V}}_0$ and with a function $f:X\to Y$ for each function $f:S\times X\to S\times Y$ in ${\mathbf{V}}_0$; we say that $f:X\to Y$ in ${\mathbf{C}}$ *stands for* $f:S\times X\to S\times Y$ in ${\mathbf{V}}_0$. Let $J:{\mathbf{V}}_0\to{\mathbf{C}}$ be the identity-on-points functor which maps each $v_0:X\to Y$ in ${\mathbf{V}}_0$ to the function $J(v_0):X\to Y$ in ${\mathbf{C}}$ that stands for ${\mathrm{id}}_S\times v_0:S\times X\to S\times Y$ in ${\mathbf{V}}_0$. Let ${\mathbf{V}}=J({\mathbf{V}}_0)$, it is a wide subcategory of ${\mathbf{C}}$. For all $f,g:X\to Y$ in ${\mathbf{C}}$, let: $$f{\lesssim}g \iff \pi_Y\circ g = \pi_Y\circ f \;.$$ We get a strict effect category, where the semi-congruence ${\lesssim}$ is symmetric, but does not satisfy the replacement property with respect to all functions in ${\mathbf{C}}$. The semi-product of $f:X\to Y_1$ and $v:X{\rightsquigarrow}Y_2$ is defined as follows. Since $f:S\times X\to S\times Y_1$ in ${\mathbf{V}}_0$ and $v={\mathrm{id}}_S\times v_0$ for some $v_0:X\to Y$ in ${\mathbf{V}}_0$, the pair ${\langle f,v_0\circ\pi_X \rangle}:S\times X\to (S\times Y_1)\times Y_2$ exists in ${\mathbf{V}}_0$. By composing it with the isomorphism $(S\times Y_1)\times Y_2 \to S\times (Y_1\times Y_2)$ we get ${\langle f,v \rangle}:S\times X\to S\times (Y_1\times Y_2)$ in ${\mathbf{V}}_0$, i.e., ${\langle f,v \rangle}:X\to Y_1\times Y_2$ in ${\mathbf{C}}$. It is easy to check that this defines a semi-product, so that ${\mathbf{C}}$ is a cartesian effect category, where the characteristic property of the semi-product $f\times v$ can be illustrated as follows: $$\xymatrix@C=5pc{ 
  (s,x_1) \ar@{|->}[r]^{f} & (s',y_1)  \\
  (s,x_1,x_2) \ar@{|~>}[u] \ar@{|~>}[d] \ar@{|->}[r]^{f\times v} 
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{=} & 
    (s',y_1,y_2) \ar@{|~>}[u] \ar@{|~>}[d]  \\
  (s,x_2) \ar@{|~>}[r]^{v} & (s,y_2)\ne(s',y_2) 
    \ar@{|~>}[r]^{\quad\pi_Y} & y_2 \\
  }$$

The example above can be curried, thus recovering the *State monad*. A motivation for the introduction of Freyd categories in [@PowerRobinson97] is the possibility of dealing with state in a linear way, as above, rather than in the exponential way provided by the State monad. Now ${\mathbf{V}}_0$ is still a cartesian category with a distinguished point $S$, the “type of states”, and in addition ${\mathbf{V}}_0$ has exponentials $(S\times X)^S$ for each $X$. Then the endofunctor $M(X)=(S\times X)^S$ defines the State monad on ${\mathbf{V}}_0$, with composition defined as usual. It is well-known that $M$ is a strong monad, with strength $t_{Y_1,Y_2}=(S\times Y_1)^S\times Y_2 \to (S\times Y_1\times Y_2)^S$ obtained from ${\mathrm{app}}_{S\times Y_1}\times{\mathrm{id}}_{Y_2}:
S\times (S\times Y_1)^S\times Y_2 \to S\times Y_1\times Y_2$, where “${\mathrm{app}}$” denotes the application function. Hence, from $f:X\to M(Y_1)$ and $v_0:X\to Y_2$ in ${\mathbf{V}}_0$, we can build ${\langle f,v \rangle}=t_{Y_1,Y_2}\circ{\langle f,v_0 \rangle}:X\to M(Y_1\times Y_2)$. Let ${\mathbf{C}}$ be the Kleisli category of the monad $M$, let $J:{\mathbf{V}}_0\to{\mathbf{C}}$ be the canonical functor associated to the monad, and let ${\mathbf{V}}=J({\mathbf{V}}_0)$, then ${\mathbf{V}}$ is a wide subcategory of ${\mathbf{C}}$. A function $f:X\to Y$ in ${\mathbf{C}}$ stands for a function $f:X\to (S\times Y)^S$ in ${\mathbf{V}}_0$. Now, in addition to the usual framework of monads, for all $f,g:X\to Y$ in ${\mathbf{C}}$, i.e., $f,g:X\to (S\times Y)^S$ in ${\mathbf{V}}_0$, let: $$f{\lesssim}g \iff  {\pi_Y}^S \circ g = {\pi_Y}^S \circ f \;,$$ where ${\pi_Y}^S:(S\times Y)^S\to Y^S$ associates to each map $m:S\to S\times Y$ the map $\pi_Y\times m:S\to Y$. The relation ${\lesssim}$ defines a semi-conguence on ${\mathbf{C}}$, and ${\langle f,v \rangle}$ is a semi-product, so that ${\mathbf{C}}$ is a cartesian effect category. The characteristic property of the semi-product $f\times v$ can be illustrated as follows: $$\xymatrix@C=5pc{ 
  x_1 \ar@{|->}[r]^{f} & (s\mapsto(s',y_1))  \\
  (x_1,x_2) \ar@{|~>}[u] \ar@{|~>}[d] \ar@{|->}[r]^{f\times v} 
    \ar@{}[rd]|{{\gtrsim}} \ar@{}[ru]|{=} & 
    (s\mapsto(s',y_1,y_2)) \ar@{|~>}[u] \ar@{|~>}[d]  \\
  x_2 \ar@{|~>}[r]^{v} & (s\mapsto(s,y_2))\ne(s\mapsto(s',y_2)) 
    \ar@{|~>}[r]^{\qquad\pi_Y^{S}} & (s\mapsto y_2) \\
  }$$

Conclusion
==========

We have presented a new categorical framework, called a *cartesian effect category*, for dealing with the issue of multiple arguments in programming languages with computational effects. The major new feature in cartesian effect categories is the introduction of a *semi-congruence*, which allows to define *semi-products* and to prove their properties by decorating the usual definitions, properties and proofs about products in a category. Forthcoming work should study the nesting of several effects.

In order to deal with other issues related to effects, we believe that the idea of *decorations* in logic can be more widely used. This is the case for dealing with exceptions [@B-DuvRey05] (note that a previous attempt to define decorated products can be found in [@F-DuvRey04]). The framework of decorations might be used for generalizing this work in the direction of closed Freyd categories [@PowerThielecke99]. or traced premonoidal categories [@BentonHyland03]. Moreover, with one additional level of abstraction, decorations can be obtained from *morphisms between logics*, in the context of *diagrammatic logics* [@F-DuvLai02; @A-Duv03].

Proofs in cartesian effect categories {#app:proof}
=====================================

Here are proofs for some results in section \[subsec:weak-prod\], called *basic* proofs, followed by their *decorated* versions for the corresponding results in section \[subsec:effect-semi\]. All basic proofs are straightforward. All proofs are presented in a formalized way: each property is preceded by its label and followed by its proof. For the basic proofs, the properties of the congruence are denoted ${\mathit{trans}}$, ${\mathit{sym}}$, ${\mathit{subst}}$, ${\mathit{repl}}$, for respectively transitivity, symmetry, substitution, replacement. For the decorated proofs, the properties of the congruence and the semi-congruence are still denoted ${\mathit{trans}}$, ${\mathit{sym}}$, ${\mathit{subst}}$, ${\mathit{repl}}$, with subscript either ${\equiv}$ or ${\lesssim}$. It should be reminded that ${\mathit{sym}}_{{\lesssim}}$ does *not* hold, and that ${\mathit{repl}}_{{\lesssim}}$ is allowed *only* with respect to a pure function: if $g_1{\lesssim}g_2:Y\to Z$ and $v:Z{\rightsquigarrow}W$ then $v\circ g_1 {\lesssim}v\circ g_2:Y\to W$. In addition, ${\mathit{comp}}$ means compatibiblity of ${\lesssim}$ with ${\equiv}$, which means that if either $f_1{\equiv}f_2{\lesssim}f_3$ or $f_1{\lesssim}f_2{\equiv}f_3$ then $f_1{\lesssim}f_3$. In decorated proofs, “like *basic*” means that this part of the proof is exactly the same as in the basic proof. Proofs of propositions \[prop:weak-assoc\], \[prop:effect-assoc\](associativity) and \[prop:weak-seq\], \[prop:effect-seq\] (parallelism) are left to the reader.

\

  ----------- ---------------------------------------------------------------- --------------------------------------
    1.$\quad$ When $X_1=X_2$                                                   

      $(a_1)$ $q_1\circ {\langle f_1,f_2 \rangle} \equiv f_1$                  

      $(b_1)$ $f_1 \equiv f'_1$                                                

      $(c_1)$ $q_1\circ {\langle f_1,f_2 \rangle} \equiv f'_1$                 $(a_1)$, $(b_1)$, ${\mathit{trans}}$

      $(c_2)$ $q_2\circ {\langle f_1,f_2 \rangle} \equiv f'_2$                 like $(c_1)$

        $(d)$ ${\langle f_1,f_2 \rangle} \equiv {\langle f'_1,f'_2 \rangle}$   $(c_1)$, $(c_2)$

    2.$\quad$ In all cases                                                     

      $(e_1)$ $f_1\equiv f'_1$                                                 

      $(f_1)$ $f_1\circ p_1\equiv f'_1\circ p_1$                               $(e_1)$, ${\mathit{subst}}$

      $(f_2)$ $f_2\circ p_2\equiv f'_2\circ p_2$                               like $(f_1)$

        $(g)$ ${\langle f_1\circ p_1,f_2\circ p_2 \rangle} \equiv              $(f_1)$, $(f_2)$, $(1)$
              {\langle f'_1\circ p_1,f'_2\circ p_2 \rangle}$                   
  ----------- ---------------------------------------------------------------- --------------------------------------

\

\

  ----------- ----------------------------------------------------------------------------------------------------- -------------------------------------
    1.$\quad$ When $X_1=X_2$                                                                                        
      $(c_1)$ $q_1\circ {\langle f_1,f_2 \rangle} {\equiv}f'_1$                                                     like *basic*
      $(a_2)$ $q_2\circ {\langle f_1,f_2 \rangle} {\lesssim}f_2$                                                    
      $(b_2)$ $f_2 {\equiv}f'_2$                                                                                    
      $(c_2)$ $q_2\circ {\langle f_1,f_2 \rangle} {\lesssim}f'_2$                                                   $(a_2)$, $(b_2)$, ${\mathit{comp}}$
        $(d)$ ${\langle f_1,f_2 \rangle} {\equiv}{\langle f'_1,f'_2 \rangle}$                                       $(c_1)$, $(c_2)$
    2.$\quad$ In all cases                                                                                          
        $(g)$ ${\langle f_1\circ p_1,f_2\circ p_2 \rangle} {\equiv}{\langle f'_1\circ p_1,f'_2\circ p_2 \rangle}$   like *basic*
  ----------- ----------------------------------------------------------------------------------------------------- -------------------------------------

\

\
The three left handsides can be illustrated as follows: $$\xymatrix@C=3pc@R=1.5pc{ 
  & & Z_1 \\
  X \ar[r]^{f} & Y \ar[ru]^{g_1} \ar[rd]_{g_2} \ar[r] &
    \bullet \ar[u] \ar[d] 
    \ar@{}[ld]|(.3){\equiv} \ar@{}[lu]|(.3){\equiv} \\
  & & Z_2 \\
  } \quad
  \xymatrix@C=3pc@R=1.5pc{ 
  & Y_1 \ar[r]^{g_1} & Z_1 \\
  X \ar[ru]^{f_1} \ar[rd]_{f_2} \ar[r] &
    \bullet \ar[u] \ar[d] \ar[r] 
    \ar@{}[ld]|(.3){\equiv} \ar@{}[lu]|(.3){\equiv} &
    \bullet \ar[u] \ar[d] 
    \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} \\
  & Y_2 \ar[r]_{g_2} & Z_2 \\
  } \quad
  \xymatrix@C=3pc@R=1.5pc{ 
  X_1\ar[r]^{f_1} & Y_1 \ar[r]^{g_1} & Z_1 \\
  \bullet \ar[u] \ar[d] \ar[r] &
    \bullet \ar[u] \ar[d] \ar[r] 
    \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} &
    \bullet \ar[u] \ar[d] 
    \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} \\
  X_2 \ar[r]_{f_2} & Y_2  \ar[r]_{g_2} & Z_2 \\
  }$$

  ----------- ------------------------------------------------------------------------------------ ---------------------------------------------
    1.$\quad$ When $f_1=f_2(=f)$                                                                   

      $(a_1)$ $r_1\circ {\langle g_1,g_2 \rangle} \equiv g_1$                                      

      $(b_1)$ $r_1\circ{\langle g_1,g_2 \rangle}\circ f\equiv g_1\circ f $                         $(a_1)$, ${\mathit{subst}}$

      $(b_2)$ $r_2\circ {\langle g_1,g_2 \rangle} \circ f \equiv g_2 \circ f $                     like $(b_1)$

        $(c)$ ${\langle g_1,g_2 \rangle} \circ f \equiv {\langle g_1\circ f,g_2\circ f \rangle}$   $(b_1)$, $(b_2)$

    2.$\quad$ When $X_1=X_2$                                                                       

        $(d)$ $(g_1\times g_2) \circ {\langle f_1,f_2 \rangle}                                     $(1)$
              \equiv {\langle g_1\circ q_1 \circ {\langle f_1,f_2 \rangle},                        
              g_2\circ q_2 \circ {\langle f_1,f_2 \rangle} \rangle}$                               

      $(e_1)$ $q_1 \circ {\langle f_1,f_2 \rangle} \equiv f_1$                                     

      $(f_1)$ $g_1\circ q_1\circ{\langle f_1,f_2 \rangle} \equiv g_1\circ f_1$                     ${\mathit{repl}}$

      $(f_2)$ $g_2\circ q_2 \circ {\langle f_1,f_2 \rangle}\equiv g_2\circ f_2$                    like $(f_1)$

        $(g)$ ${\langle g_1\circ q_1 \circ {\langle f_1,f_2 \rangle},                              $(f_1)$, $(f_2)$, prop. \[prop:weak-equiv\]
              g_2\circ q_2 \circ {\langle f_1,f_2 \rangle} \rangle} \equiv                         
              {\langle g_1\circ f_1,g_2\circ f_2 \rangle}$                                         

        $(h)$ $(g_1\times g_2) \circ {\langle f_1,f_2 \rangle} \equiv                              $(d)$, $(g)$, ${\mathit{trans}}$
              {\langle g_1\circ f_1,g_2\circ f_2 \rangle}$                                         

    3.$\quad$ In all cases                                                                         

        $(k)$ $ (g_1 \times g_2) \circ {\langle f_1\circ p_1,f_2\circ p_2 \rangle} \equiv          $(2)$
                    {\langle g_1\circ f_1\circ p_1,g_2\circ f_2\circ p_2 \rangle}$                 
  ----------- ------------------------------------------------------------------------------------ ---------------------------------------------

\

\
The three left handsides can be illustrated as follows: $$\xymatrix@C=3pc@R=1.5pc{ 
  & & Z_1 \\
  X \ar@{~>}[r]^{v} & Y \ar[ru]^{g_1} \ar@{~>}[rd]_{w_2} \ar[r] &
    \bullet \ar@{~>}[u] \ar@{~>}[d] 
    \ar@{}[ld]|(.3){{\gtrsim}} \ar@{}[lu]|(.3){{\equiv}} \\
  & & Z_2 \\
  } \quad
  \xymatrix@C=3pc@R=1.5pc{ 
  & Y_1 \ar[r]^{g_1} & Z_1 \\
  X \ar[ru]^{f_1} \ar@{~>}[rd]_{v_2} \ar[r] &
    \bullet \ar@{~>}[u] \ar@{~>}[d] \ar[r] 
    \ar@{}[ld]|(.3){{\gtrsim}} \ar@{}[lu]|(.3){{\equiv}} &
    \bullet \ar@{~>}[u] \ar@{~>}[d] 
    \ar@{}[ld]|{{\gtrsim}} \ar@{}[lu]|{{\equiv}} \\
  & Y_2 \ar@{~>}[r]_{w_2} & Z_2 \\
  } \quad
  \xymatrix@C=3pc@R=1.5pc{ 
  X_1\ar[r]^{f_1} & Y_1 \ar[r]^{g_1} & Z_1 \\
  \bullet \ar@{~>}[u] \ar@{~>}[d] \ar[r] &
    \bullet \ar@{~>}[u] \ar@{~>}[d] \ar[r] 
    \ar@{}[ld]|{{\gtrsim}} \ar@{}[lu]|{{\equiv}} &
    \bullet \ar@{~>}[u] \ar@{~>}[d] 
    \ar@{}[ld]|{{\gtrsim}} \ar@{}[lu]|{{\equiv}} \\
  X_2 \ar@{~>}[r]_{v_2} & Y_2  \ar@{~>}[r]_{w_2} & Z_2 \\
  }$$

  ----------- --------------------------------------------------------------------------------------------------------------------------------------------- ------------------------------------------------
    1.$\quad$ When $f_1=v_2(=v)$                                                                                                                            

      $(b_1)$ $r_1\circ{\langle g_1,w_2 \rangle}\circ v{\equiv}g_1\circ v $                                                                                 like *basic*

      $(a_2)$ $r_2\circ {\langle g_1,w_2 \rangle} {\lesssim}w_2 $                                                                                           

      $(b_2)$ $r_2\circ{\langle g_1,w_2 \rangle}\circ v{\lesssim}w_2\circ v $                                                                               $(a_1)$, ${\mathit{subst}}_{{\lesssim}}$

        $(c)$ ${\langle g_1,w_2 \rangle} \circ v {\equiv}{\langle g_1\circ v,w_2\circ v \rangle}$                                                           $(b_1)$, $(b_2)$

    2.$\quad$ When $X_1=X_2$                                                                                                                                

        $(d)$ $(g_1\times w_2) \circ {\langle f_1,v_2 \rangle}                                                                                              $(1)$
              {\equiv}{\langle g_1\circ q_1 \circ {\langle f_1,v_2 \rangle},                                                                                
              w_2\circ q_2 \circ {\langle f_1,v_2 \rangle} \rangle}$                                                                                        

      $(f_1)$ $g_1\circ q_1\circ{\langle f_1,v_2 \rangle} {\equiv}g_1\circ f_1$                                                                             like *basic*

      $(e_2)$ $q_2 \circ {\langle f_1,v_2 \rangle} {\lesssim}v_2$                                                                                           

      $(f_2)$ $w_2\circ q_2\circ{\langle f_1,v_2 \rangle} {\lesssim}w_2\circ v_2$                                                                           ${\mathit{repl}}_{{\lesssim}}$ ($w_2$ is pure)

        $(g)$ ${\langle g_1\circ q_1 \circ {\langle f_1,v_2 \rangle},                                                                                       $(f_1)$, $(f_2)$, prop. \[prop:weak-equiv\]
              w_2\circ q_2 \circ {\langle f_1,v_2 \rangle} \rangle} {\equiv}{\langle g_1\circ f_1,w_2\circ v_2 \rangle}$                                    

        $(h)$ $(g_1\times w_2) \circ {\langle f_1,v_2 \rangle} {\equiv}{\langle g_1\circ f_1,w_2\circ v_2 \rangle}$                                         $(d)$, $(g)$, ${\mathit{trans}}_{{\equiv}}$

    3.$\quad$ In all cases                                                                                                                                  

        $(k)$ $ (g_1 \times w_2) \circ {\langle f_1\circ p_1,v_2\circ p_2 \rangle} {\equiv}{\langle g_1\circ f_1\circ p_1,w_2\circ v_2\circ p_2 \rangle}$   $(2)$
  ----------- --------------------------------------------------------------------------------------------------------------------------------------------- ------------------------------------------------

\

\
The two left handsides can be illustrated as follows: $$\xymatrix@C=2pc@R=1.5pc{ 
  & Y_1 \ar[r]^{{\mathrm{id}}} & Y_1 \\
  X \ar[ur]^{f_1} \ar[dr]_{f_2} \ar[r] & 
  Y_2\times Y_1 \ar[u]\ar[d] \ar[r] \ar@{}[ld]|(.3){\equiv} \ar@{}[lu]|(.3){\equiv} & 
  Y_1\times Y_2 \ar[u]\ar[d] \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} \\
   & Y_2 \ar[r]_{{\mathrm{id}}} & Y_2 \\
  }   \quad \xymatrix@C=2pc@R=1.5pc{ 
  X_1 \ar[r]^{{\mathrm{id}}} & X_1 \ar[r]^{f_1} & Y_1 \ar[r]^{{\mathrm{id}}} & Y_1 \\
  X_1\times X_2 \ar[u]\ar[d] \ar[r] & 
  X_2\times X_1 \ar[u]\ar[d] \ar[r] \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} & 
  Y_2\times Y_1 \ar[u]\ar[d] \ar[r] \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} & 
  Y_1\times Y_2 \ar[u]\ar[d] \ar@{}[ld]|{\equiv} \ar@{}[lu]|{\equiv} \\
  X_2 \ar[r]_{{\mathrm{id}}} & X_2 \ar[r]_{f_2} & Y_2 \ar[r]_{{\mathrm{id}}} & Y_2 \\
  }$$

  ----------- ---------------------------------------------------------------------------------------------------------------- ---------------------------------------------
    1.$\quad$ When $X_1=X_2$                                                                                                   

      $(a_1)$ $q_1\circ\gamma_Y \equiv q'_1$                                                                                   

      $(b_1)$ $q_1\circ\gamma_Y \circ {\langle f_2,f_1 \rangle}                                                                $(a_1)$, ${\mathit{subst}}$
              \equiv q'_1 \circ {\langle f_2,f_1 \rangle} $                                                                    

      $(c_1)$ $q'_1 \circ {\langle f_2,f_1 \rangle} \equiv f_1$                                                                

      $(d_1)$ $q_1\circ\gamma_Y \circ {\langle f_2,f_1 \rangle} \equiv f_1$                                                    $(b_1)$, $(c_1)$, ${\mathit{trans}}$

      $(d_2)$ $q_2\circ\gamma_Y \circ {\langle f_2,f_1 \rangle} \equiv f_2 $                                                   like $(d_1)$

        $(e)$ $\gamma_Y \circ {\langle f_2,f_1 \rangle} \equiv {\langle f_1,f_2 \rangle}$                                      $(d_1)$, $(d_2)$

    2.$\quad$ In all cases                                                                                                     

        $(f)$ ${\langle f_2\circ p'_2, f_1\circ p'_1 \rangle} \circ \gamma_X^{-1}                                              prop. \[prop:weak-comp\], ${\mathit{sym}}$
                \equiv {\langle f_2\circ p'_2\circ \gamma_X^{-1}, f_1\circ p'_1\circ \gamma_X^{-1} \rangle} $                  

        $(g)$ $\gamma_Y \circ {\langle f_2\circ p'_2, f_1\circ p'_1 \rangle} \circ \gamma_X^{-1}                               ${\mathit{repl}}$
                \equiv \gamma_Y \circ {\langle f_2\circ p'_2\circ \gamma_X^{-1}, f_1\circ p'_1\circ \gamma_X^{-1} \rangle} $   

        $(h)$ $\gamma_Y \circ {\langle f_2\circ p'_2\circ \gamma_X^{-1}, f_1\circ p'_1\circ \gamma_X^{-1} \rangle}             $(1)$
                \equiv {\langle f_1\circ p'_1\circ \gamma_X^{-1},f_2\circ p'_2\circ \gamma_X^{-1} \rangle}$                    

      $(i_1)$ $p'_1\circ \gamma_X^{-1} \equiv p_1$                                                                             

      $(j_1)$ $f_1\circ p'_1\circ \gamma_X^{-1} \equiv f_1\circ p_1$                                                           $(i_1)$, ${\mathit{repl}}$

      $(j_2)$ $f_2\circ p'_2\circ \gamma_X^{-1} \equiv f_2\circ p_2$                                                           like $(j_1)$

        $(k)$ $ {\langle f_1\circ p'_1\circ \gamma_X^{-1},f_2\circ p'_2\circ \gamma_X^{-1} \rangle}                            $(j_1)$, $(j_2)$, prop. \[prop:weak-equiv\]
              \equiv {\langle f_1\circ p_1,f_2\circ p_2 \rangle}$                                                              

        $(l)$ $\gamma_Y \circ {\langle f_2\circ p'_2, f_1\circ p'_1 \rangle} \circ \gamma_X^{-1}                               $(g)$, $(h)$, $(k)$, ${\mathit{trans}}$
              \equiv {\langle f_1\circ p_1,f_2\circ p_2 \rangle}$                                                              
  ----------- ---------------------------------------------------------------------------------------------------------------- ---------------------------------------------

\

\
The two left handsides can be illustrated as follows: $$\xymatrix@C=2pc@R=1.5pc{ 
  & Y_1 \ar@{~>}[r]^{{\mathrm{id}}} & Y_1 \\
  X \ar[ur]^{f_1} \ar@{~>}[dr]_{v_2} \ar[r] & 
  Y_2\times Y_1 \ar@{~>}[u]\ar@{~>}[d] \ar@{~>}[r] 
     \ar@{}[ld]|(.3){{\gtrsim}} \ar@{}[lu]|(.3){{\equiv}} & 
  Y_1\times Y_2 \ar@{~>}[u]\ar@{~>}[d] \ar@{}[ld]|{{\equiv}} \ar@{}[lu]|{{\equiv}} \\
   & Y_2 \ar@{~>}[r]_{{\mathrm{id}}} & Y_2 \\
  }   \quad \xymatrix@C=2pc@R=1.5pc{ 
  X_1 \ar@{~>}[r]^{{\mathrm{id}}} & X_1 \ar[r]^{f_1} & Y_1 \ar@{~>}[r]^{{\mathrm{id}}} & Y_1 \\
  X_1\times X_2 \ar@{~>}[u]\ar@{~>}[d] \ar@{~>}[r] & 
  X_2\times X_1 \ar@{~>}[u]\ar@{~>}[d] \ar[r] \ar@{}[ld]|{{\equiv}} \ar@{}[lu]|{{\equiv}} & 
  Y_2\times Y_1 \ar@{~>}[u]\ar@{~>}[d] \ar@{~>}[r] \ar@{}[ld]|{{\gtrsim}} \ar@{}[lu]|{{\equiv}} & 
  Y_1\times Y_2 \ar@{~>}[u]\ar@{~>}[d] \ar@{}[ld]|{{\equiv}} \ar@{}[lu]|{{\equiv}} \\
  X_2 \ar@{~>}[r]_{{\mathrm{id}}} & X_2 \ar@{~>}[r]_{v_2} & Y_2 \ar@{~>}[r]_{{\mathrm{id}}} & Y_2 \\
  }$$

  ----------- ------------------------------------------------------------------------------------ ----------------------------------------
    1.$\quad$ When $X_1=X_2$                                                                       

      $(d_1)$ $q_1\circ\gamma_Y \circ {\langle v_2,f_1 \rangle} {\equiv}f_1$                       like *basic*

      $(a_2)$ $q_2\circ\gamma_Y {\equiv}q'_2$                                                      

      $(b_2)$ $q_2\circ\gamma_Y \circ {\langle v_2,f_1 \rangle}                                    $(a_2)$, ${\mathit{subst}}_{{\equiv}}$
              {\equiv}q'_2 \circ {\langle v_2,f_1 \rangle} $                                       

      $(c_2)$ $q'_2 \circ {\langle v_2,f_1 \rangle} {\lesssim}v_2$                                 

      $(d_2)$ $q_2\circ\gamma_Y \circ {\langle v_2,f_1 \rangle} {\lesssim}v_2$                     $(b_2)$, $(c_2)$, ${\mathit{comp}}$

        $(e)$ $\gamma_Y \circ {\langle v_2,f_1 \rangle} {\equiv}{\langle f_1,v_2 \rangle}$         $(d_1)$, $(d_2)$

    2.$\quad$ In all cases                                                                         

        $(l)$ $\gamma_Y \circ {\langle f_2\circ p'_2, f_1\circ p'_1 \rangle} \circ \gamma_X^{-1}   like *basic*
              \equiv {\langle f_1\circ p_1,f_2\circ p_2 \rangle}$                                  
  ----------- ------------------------------------------------------------------------------------ ----------------------------------------

\
