2.8. Canonical bijections

For all objects x,y we shall say that x determines y if there is an invariant functor T such that T(x) = y. Then the role of y as free variable can be played by the term T(x), thus by the use of x. This is a meta-preorder on the universe, but not a predicate of set theory as it involves a meta-concept. Rather, it is meant to abbreviate the use of T.
Similarly, a function f : EF will be said canonical if it is defined as Ex → T(x) for some invariant functor T. A bijection f will be said bicanonical if both f and f−1 are canonical. When a bijection f : E ↔  F is canonical (resp. bicanonical), we write f : EF (resp. f : EF); or, with its defining functor, T : EF which means that (ExT(x)) is injective with image F. We shall write EF (resp. EF) to mean the existence of a canonical (resp. bicanonical) bijection, that is kept implicit.
Canonical bijections can fail to be bicanonical especially when their defining functor is not injective:
2E ≅ ℘(E), {x}E ≅ {x} and E×{x} ≅ E, whereas {xEE{x} and E ≡ {0}×E.
This is a meta-preorder on the class of sets, preserved by constructions: for example if EE′ and FF′ then E×FE′×F′ and FEFE using the direct image of the graph (while we may not have FEFE when E′ does not determine E). It will often look like a property of numbers as the existence of a bijection between finite sets implies the equality of their numbers of elements.
The transposition of oriented pairs (E×FF×E) extends to graphs (℘(E×F) ≡ ℘(F×E)) and to operations: GE×FGF×E where fGE×F is transposed by tf(x,y)=f(y,x).

Sums of sets, sums of functions

If S=∐iI Ei then ∐: ∏iI ℘(Ei) ≅ ℘(S), whose inverse SRRI = (IiR(i)) depends on I. In particular for two sets E and F we have (℘(F))E ≅ ℘(E×F).
The sum over I of functions fi where ∀iI, Ei = Domfi is defined by
iI fi = (S ∋ (i,x) ↦ fi(x))
f=∐iI fi⇔ (Dom f=S∧∀iI, fi= f(i)=fji)    where ji=(Eix ↦ (i,x))
Thus the canonical bijections (bicanonical if I= Dom S, thus if E ≠ ∅ in the case I×E)


(fi)iI ∈ (FE)I⇒ 
Gr fi ⊂ ℘(I×(E×F)) ≡ ℘((I×EF) ⊃ Gr

Product of functions or recurrying

Transposing a relation R exchanges its curried forms R andR, by a bijection (℘(F))E  ↔  (℘(E))F with parameter F. Similarly we have a bijection (FE)I ↔ (FI)E, canonical if I ≠ ∅ (to let (FE)I determine E), defined by a binder ∏ called the product of the functions fiFE for iI:

FiE ≅ (
fi = (Ex ↦ (fi(x))iI)
  ∀g, g =
fi  ⇔ (g : E →
Im fi ∧∀iI, fi = πig)
Dom f = Dom g = Ef×g = (Ex ↦ (f(x),g(x)))
 IE×FE ≡ (I×F)E

Fϕ(x) (

1. First foundations of mathematics
2. Set theory (continued)
2.1. Tuples, families
2.2. Boolean operators on families of sets
2.3. Products, graphs and composition
2.4. Uniqueness quantifiers, functional graphs
2.5. The powerset axiom
2.6. Injectivity and inversion
2.7. Properties of binary relations ; ordered sets
2.8. Canonical bijections
2.9. Equivalence relations and partitions
2.10. Axiom of choice
2.11. Notion of Galois connection
3. Model theory