The following terms are derived from the atomic functions and combinators of Definition 3.1. They are used to state the axioms of Section 4 and the results of the completeness proof.

• The unique term $A \to 1$, co-pairing $\langle f_1, f_2 \rangle = (f_1 + f_2) \mathbin{;} \mathsf{codiag}$, commutativity and associativity of co-products.
• The list notation of Section 4.6: the empty list $[\,] : 1 \to A^*$, $\mathsf{prepend} : A \times A^* \to A^*$, $\mathsf{append} : A^* \times A \to A^*$, $\mathsf{pure} : A \to A^*$, $\mathsf{binconcat} : A^* \times A^* \to A^*$, the homomorphism combinator $\mathrm{hom}\, f = f^* \mathbin{;} \mathsf{concat}$, and the concatenation $f \odot g = (f \times g) \mathbin{;} \mathsf{binconcat}$ of two terms with list outputs.
• The inverses of distributivity, $\mathsf{undistL}$ and $\mathsf{undistR}$ (Section 4.4).
• Definition 5.1 (Value). A value is a term of type $1 \to A$. For a list value $w$, the terms $w \cdot f$ and $f \cdot w$ prepend or append the output of $w$ to the output of $f$ (Section 5.2), and $\mathsf{head}_w : A^* \to A$ returns the first element of a list, or the output of $w$ for the empty list.
• Concatenation maps (Section 5.1). For a type constructor $F$ with one parameter, built from the parameter, $1$, $\times$, $+$ and $(-)^*$, the concatenation map $F(A) \rightarrowtail A^*$ lists all the elements of $A$ occurring in the input, from left to right. Similarly for type constructors with two parameters, with outputs in $(A + B)^*$. In particular, $\mathsf{unsplit} : A^* \times (B \times A^*)^* \to (A + B)^*$ is a concatenation map.
• The terms $\mathsf{shift} : (A \times B)^* \to 1 + A \times (B \times A)^* \times B$ and $\mathsf{unshift}$ of Table 1.
• The inverse $\mathsf{unpref}$ of group prefix multiplication (Section 4.4), which maps $[(a_1, g_1), \ldots, (a_n, g_n)]$ to $[(a_1, g_0^{-1} g_1), \ldots, (a_n, g_{n-1}^{-1} g_n)]$, where $g_0$ is the group identity.