- A list of
*n*domain functors (sometimes not available but not needed since domains are usually fixed by the context); - Its evaluator is an (
*n*+1)-ary operator (resp. predicate) written in filled form as*f*(*x*_{0},…,*x*_{n−1}), with arguments one*n*-ary operation (resp. relation)*f*, and its*n*arguments*x*_{0},…,*x*_{n−1}; - Its definer binds
*n*variables to their respective ranges on a term (resp. a formula).

*E*×*F* ∋ (*x*,*y*) ↦ *A*(*x*,*y*)

One aspect is that relations are reducible to operations, and vice-versa:

- The notion of
*n*-ary relation can be constructed as a class of*n*-ary operations, by taking the Boolean pair as target set, as we did in 1.4 (for predicates) and will formalize in 2.4. - Inversely, the notion of
*n*-ary operation can be constructed as a class of (*n*+1)-ary relations (2.7).

*b* = (*E* ∋ *x* ↦ (*F* ∋ *y* ↦ *B*(*x*,*y*)))

Dom *b* = *E* ∧ ∀*x*∈*E*, Dom *b*(*x*) = *F*
∧ ∀*y*∈*F*, *B*(*x*,*y*) = *b*(*x*)(*y*)

The first domain functor comes as Dom

This somehow makes each binary operation work as a function evaluator, by giving

Similarly, the notion of *n*-ary relation can be defined in curried form as a class,
giving the role of definer to a succession of *n*−1 uses of the function
definer and 1 use of the set-builder.
The curried form *r* of a binary relation with domains *E* and *F*, is so defined
from a binary predicate *R*, and evaluated back as *R*,
by the equivalent formulas

*r* = (*E* ∋ *x* ↦
{*y* ∈ *F* | *R*(*x*,*y*)})

Dom *r* = *E* ∧ (∀*x*∈*E*, *r*(*x*) ⊂ *F*
∧ ∀*y*∈*F*, *R*(*x*,*y*) ⇔ *y* ∈ *r*(*x*))

These constructions have the defect of breaking the symmetry of role between arguments. The next construction method, by tuples, will preserve this symmetry, and will be usually preferred for this reason.

The definer and evaluator symbols for tuples take a special form because, while tuples are meta-functions, the role they play in the theory differs from those of functors or functions.

AnNow, each structure
(resp. operation, relation) can be re-formalized as a unary structure (resp. a function,
a unary relation) with domain a type (resp. a class which is actually a set) of tuples, to be
used with the relevant tuples definer. This can be implicitly done by re-interpreting the notation:
*S*(*x*,*y*) can be read seeing *S* either as a binary
structure (resp. operation, relation), or as a unary one taking as argument the
ordered pair given by the term (*x*,*y*) formed by the ordered pair definer
with arguments *x* and *y*.

The role of *n*-tuple evaluator is played by a list of *n* functors
called *projections* which extract each variable from the given pack.
This list plays the role of the function evaluator curried in the reverse way, by fixing its
meta-argument whose range (the domain of tuples as meta-functions) is not seen by
the theory as a set of objects but as a list of *n* symbols to be taken separately.

For

∀_{E }*x*, ∀_{F }*y*,
∀_{P }*z*, (*x* = π_{0}(*z*) ∧ *y* =
π_{1}(*z*)) ⇔ (*x*,*y*) = *z*

∀_{P }*z*, (π_{0}(*z*),
π_{1}(*z*)) = *z*

∀_{E }*x*,
∀_{F }*y*, π_{0}(*x*,*y*) = *x*

∀_{E }*x*, ∀_{F }*y*,
π_{1}(*x*,*y*) = *y*

∀_{E }*x*,*x'*, ∀_{F }*y*,*y'*,
(*x*,*y*) = (*x'*,*y'*) ⇔ (*x* = *x'* ∧ *y* = *y'*)

For this, since tuples are meta-functions, they are naturally represented by functions.
This involves copying their meta-domain, which is a list of symbols, into a set (of
elements). Namely, let us represent the domain of considered *n*-tuples by the set
*V _{n}* of

∀*i*∈*V _{n}*, π

More tools need to be introduced before defining in set theory the tuple definers (2.4) and the operation definers working with tuples (2.7).

FR : 2.3. Curryfication et uplets