Is there a nice definition of a homotopy type? We often talk about specific mathematical objects, even though the way we formalise them in set theory actually means that we're talking about multiple objects. For example "the" complete graph on $n$-nodes is actually many graphs, one for each set of cardinality $n$. We can solve this problem by taking the proper class of all such graphs, but I find proper classes ontologically unconscionable. In general, in this vein, we could talk about the isomorphism classes in any category. We could also take a representative of each class, but this is "cheating", and probably difficult, if not generally impossible, at least in $\textrm{ZFC}$. I suspect that while keeping a set-theoretic foundation, then we have to make due with this multiplicity. However, graphs and most other objects we talk about are structured sets, and usually they do have the nice property that if they are isomorphic, then only the underlying sets differ, in a sense I make explicit in the appendix. On the other hand, homotopy types are not structured sets. A point and a line are radically different objects but they have the same homotopy type. And, due to my objections, we can't define a homotopy type as the equivalence class of all its spaces, since that's a proper class, and we can't just take a representative. So, is there a nicer way to define homotopy types?
Appendix: We take an underlying set $U$, and build another set out of it. A set can be thought of as a rooted tree with no infinite branches (and an asymmetry condition corresponding to extensionality), so we can think of building a new set as taking such a rooted tree $T$ (without the asymmetry condition), and attaching members of the underlying set to it. Explicitly, we take a surjective (partial) function $f:L\to U$ where $L$ is the set of leaves of $T$. We can then think of the set we've built as that obtained by taking copies of the trees representing the members of $U$ and attaching their roots to the corresponding members of $L$. Of course, this tree needs to satisfy the asymmetry condition to represent a set, although it doesn't really matter. An isomorphism between $f:L\to U$ with $L$ the leaves of $T$ and $f':L'\to U'$ with $L'$ the leaves of $T'$ is a rooted tree isomorphism $i:T\to T'$ and a bijection $b:U\to U'$ such that $bf=f'i$. In all examples I can think of, an isomorphism in a category of structured sets (e.g. graphs, topological spaces, groups) is an isomorphism in this sense, or at least there is a way of representing the objects of the category so that it is one.
 A: For homotopy types we can do the following.
A minimal Kan complex is a Kan complex $K$ with the following property:

*

*Given morphisms $x_0, x_1 : \Delta^n \to K$, if $x_0$ and $x_1$ are homotopic relative to their boundary, then $x_0 = x_1$.

We have the following fact:
Proposition. Minimal Kan complexes are homotopy equivalent if and only if they are isomorphic.
Furthermore:
Proposition. For every Kan complex $K$, there is a simplicial subset $K' \subseteq K$ such that $K'$ is a minimal Kan complex and $K' \hookrightarrow K$ is a strong deformation retract.
Corollary. Every homotopy type can be realised by a minimal Kan complex uniquely up to isomorphism.
I don't think this is nice per se, but it is nicer than using Scott's trick on the class of topological spaces modulo weak homotopy equivalence.

Since it was bothering me for a while, let me remark why this does not contradict Freyd's theorem on the non-concreteness of the homotopy category.
Although it is true that every connected component of a minimal Kan complex has a unique vertex, and therefore that homotopic morphisms into a minimal Kan complex agree on vertices, it is not true that homotopic morphisms are equal.
Nonetheless the definition is just enough to ensure that any endomorphism of a minimal Kan complex homotopic to the identity is an isomorphism, which ensures that any homotopy equivalence of minimal Kan complexes is an isomorphism.
In short, the quotient functor from the category of minimal Kan complexes to the homotopy category is full and conservative but not faithful.
A: 
On the other hand, homotopy types are not structured sets. A point and a line are radically different objects but they have the same homotopy type.

There is a subtle point here that is worth addressing. It's true that the usual definition of a homotopy type does not produce a definition in terms of structured sets. However, that doesn't preclude the possibility that there is some other definition which does produce a structured set.
But this is known to be impossible in the following precise sense: Freyd showed in Homotopy is Not Concrete that there is no faithful functor from the homotopy category (in fact from any variant of the homotopy category which contains finite-dimensional CW complexes) to $\text{Set}$. In other words, there is no way to describe homotopy types as structured sets in such a way that homotopy classes of maps are exactly the structure-preserving functions.
