theorem for free: relation cartesian product

Question

I am digging through a paper Theorems for free and a bit confused on the source of some conjectures (page 5):

Is it an axiom or it can be implied from some other axioms?

UPD

Question is about Cartesian product definition for relations. Is it an axiom or it can be derived from relation/Cartesian production definition?

UPD2

To expand on my source of confusion.

I have tried to derive this definition, but it differs from the one given in the paper. $\newcommand{\mc}{\mathcal}$

Then we have from the paper definitions for $\mc A$ and $\mc B$: $$\mc A: A \iff A'$$ $$\mc B: B \iff B'$$

from Cartesian product definition

$$(X, Y) \in \mc A \times \mc B$$

$X$ and $Y$ are values from corresponding relations $\mc A$ and $\mc B$ and it is possible to expand these values:

$$X \in \mc A, X = (x, x'), \ x \in A,\ x' \in A'$$ $$Y \in \mc B, Y = (y, y'), \ y \in B,\ y' \in B'$$

and then it appears:

$$((x, x'), (y, y')) \in \mc A \times \mc B$$

Tuple type is different from the paper one.

$$((A, A'), (B, B'))\ my\ type$$ $$((A, B), (A', B'))\ paper\ type$$

What is wrong?

Answer 1

It is a definition. The statement about a product of functions follows from the definition, since if $a,b$ are functions then $((x, y), (x', y')) \in a \times b$ iff $(x, x')\in a, (y, y')\in b$ iff $x' = ax, y' = ay$. Therefore $a\times b$ is a function, as every $(x,y)$ has a unique $(x', y')$ (this is $(ax, ay)$) such that $((x, y), (x', y'))\in a\times b$, and by definition $(a\times b)(x, y) = (ax, ay)$.

Answer 2

$\newcommand{\mc}{\mathcal}$ $\mc A\times\mc B$ is not the cartesian product of $\mc A$ and $\mc B$ as sets, but it is a new definition. In fact, it is the cartesian product in the category of relations.

For example (there may be other choices of morphisms), the objects are relations, and a morphism $f : \mc A\to\mc B$ is a pair $(f_1, f_2)$ where $f_1 : A\to B$, $f_2 : A'\to B'$ such that $$x\mc A y\implies(f_1 x)\mc B (f_2 y).$$

Then you can check that $\mc A\times \mc B$ as given above satisfies the universal property of the product where

$$\hat\pi_1 : \mc A\times\mc B\to \mc A\\\hat\pi_2 :\mc A\times\mc B\to B$$ are given by $$(\pi_1 : A\times B\to A,\pi_1':A'\times B'\to A')\\ (\pi_2 : A\times B\to B,\pi_2':A'\times B'\to B'),$$ and given $$f : \mc C\to \mc A\qquad g :\mc C\to\mc B,$$ we obtain $$\langle f,g\rangle :\mc C\to\mc A\times\mc B$$ by the pair $(f_1\times g_1, f_2\times g_2)$, where notice this time the product of functions is taken in the category of sets.