Definition. Weak product [math-O7B4]

Higher-Order Computability

A computability model $\mathbb{C}$ has weak (binary cartesian) products if there is an operation assigning to each $A,B \in \vert \mathbb{C} \vert$ a datatype $A \bowtie B \in \vert \mathbb{C} \vert$ along with operations $\pi_A \in \mathbb{C}[A \bowtie B, A]$ and $\pi_B \in \mathbb{C}[A \bowtie B, B]$, such that for any $f \in \mathbb{C}[C,A]$ and $g \in \mathbb{C}[C,B]$, there exists $\langle f,g \rangle \in \mathbb{C}[C, A \bowtie B]$ satisfying the following for all $c \in C$.

• $\langle f,g \rangle(c) \downarrow$ iff $f(c) \downarrow$ and $g(c) \downarrow$
• if $\langle f,g \rangle(c)$ is defined, then $\pi_A(\langle f,g \rangle(c)) = f(c)$ and $\pi_B(\langle f,g \rangle(c)) = g(c)$

We say that $d \in A \bowtie B$ represents the pair $(a,b)$ if $\pi_A(d) = a$ and $\pi_B(d) = b$.