The standard way of using ZFC to encode the rest of mathematics is sometimes criticized because it introduces unnecessary, strange properties such as, for example $1\in 2$ if we encode integers by ordinals.
From a constructivist type theorist's perspective, uples or functions or complex numbers should have nothing to do with the membership relation, we should have some sort of "free algebra".
Formally, consider a set $M$, a binary relation $\varepsilon$ on $M$, and a partition $S\cup P \cup C \cup F$ of $M$. The intention is that $S$ represents sets, $P$ represents pairs, $C$ represents complex numbers and $F$ represents functions.
I say that $M$ is a "free model" of usual mathematics if
(1) $(M,\varepsilon)$ satisfies all the axioms of ZFC except extensionality.
(2) $(S,\varepsilon)$ satisfies all the axioms of ZFC. In partcular, extensionality is satisfied on $S$ : If two elements of $S$ have the same $\varepsilon$-elements (in $M$), they are equal.
(3) All the elements in $P,C,F$ are $\varepsilon$-empty.
(4) There is a bijection $M^2 \to P$.
(5) There is a bijection ${\mathbb C} \to C$.
(6) There is a bijection ${\cal F}(M) \to F$, where ${\cal F}(M)$ is the set of all partial functions from $M$ to $M$, i.e. the set of all $A\subseteq M^2$ satisfying $(a,b)\in A,(a,b')\in A \Rightarrow b=b'$.
Note that the bijection in (6) is necessarily outside $M$.
Let us assume that ZFC is consistent. Does it necessarily follow that there is a "free model" of usual mathematics ?
I thought of starting with a countable model and using transfinite induction, but it is not clear how one should define pairs or functions in the new model.