The approach to algebraic specifications of set theories proposed by Tarski and Givant inspires current research aimed at taking advantage of the purely equational nature of the resulting formulations for enhanced automation of reasoning on aggregates of various kinds: sets, bags, hypersets, etc. The viability of the said approach rests upon the possibility to form ordered pairs and to decompose them by means of conjugated projections. Ordered pairs can be conceived of in many ways: along with the most classic one, several other pairing functions are examined, which can be preferred to it when either the axiomatic assumptions are too weak to enable pairing formation A la Kuratowski, or they are strong enough to make the specification of conjugated projections particularly simple, and their formal properties easy to check within the calculus of binary relations.