# Why “modding out the homeomorphism” in the category Top makes no rigorous sense?

We can rigorously talk about Top, the category of all topological space, and also FTop, the category of all finite topological space. So I thought, we can define a category FTop', where we “mod out by homeomorphism” between objects in FTop. i.e. define the equivalence relation ~ in FTop as X ~ Y if they are homeomorphic and define FTop’ as FTop/~. But recently I am told that this “makes no rigorous sense”. Why is that?

• What do you want to use as the morphisms from one homeomorphism-class of spaces to another? – Andreas Blass Jul 31 '18 at 17:16
• It does make rigorous sense. its just that it is a bad idea: the resulting category is a very weird object (the hom set in the resulting category are verry different from the hom set in the category of spaces) – Simon Henry Jul 31 '18 at 17:58
• What is true on the other hand is that there is an equivalence from any category to its skeleton, which identifies objects of the skeleton with isomorphism classes of objects. There is however no canonical choice of values of such equivalence on morphisms, just as there is no canonical choice of objects for the skeleton itself. – მამუკა ჯიბლაძე Jul 31 '18 at 18:28
• Composition of such "morphisms" (I mean, as in JASON's comment of 58 mins ago) is not well defined. – Tom Goodwillie Jul 31 '18 at 18:29
• 15 upvotes on an answer to a question with 0 upvotes? Provoking a meaningful answer is only possible with a meaningful question; I think both should be supported. – Alec Rhea Aug 1 '18 at 5:48

There are a couple of things to watch out for.

First, the collection of all spaces which are homeomorphic to a given space $X$ forms a proper class, and so we cannot just naively use set theory to form it. Nevertheless this is not a true obstacle, since we can employ Scott's trick.

Second, two spaces can be homeomorphic in many ways, which presents a problem when we try to define morphisms between equivalence classes. Writing $[X]$ for the homeomorphism class of $X$, what could the morphisms $[X] \to [Y]$ be? One might naively try to answer with "equivalence classes of continuous maps $f : X \to Y$ of some sort". However, this will not work so easily. Here's an obvious attemp that does not work. Given $X \cong X'$ and $Y \cong Y'$ and $f : X \to Y$ and $f' : X' \to Y'$, say that $f \cong f'$ if there are homeomorphisms $p : X \to X'$ and $q : Y \to Y'$ such that $f' \circ p = q \circ f$ (as suggested in the comments). Then composition of functions is not a congruence and so composition of morphisms is unclear (as noted in the comments).

As far as I can tell, the problem persists with finite spaces as well. If fact, the problem is not specific to topological spaces at all. As soon as there can be multiple isomorphisms between two objects, we'll have a problem.

One possible solution (which I initially called "standard" but people in the comments questioned it) is not to quotient the category but to pass to its skeleton, i.e., we form the full subcategory on chosen representatives of homeomorphism classes. In general this may require some form of the axiom of choice, but let's not worry about that today.

Supplemental: The discussion in the comments veered in the direction of homotopy type theory, so it might be worth looking at what happens there. If we take topological spaces to live at the level of 0-types (also known as h-sets), then by the structure identity principle homeomorphic spaces are going to be equal. This may seem mistifying at first, for does such a statement not suffer from the same defect regarding morphisms, as above? No, because HoTT is proof-relevant. Concretely, suppose $h : X' \to X$ is a homeomorphism and $f : X \to Y$ is a continuous map. The following does not work in HoTT:

Faulty HoTT reasoning: Because $X'$ and $X$ are homeomorphic, by the structure identity principle $X' = X$, and since $f : X \to Y$ then also $f : X' \to Y$.

We must pay attention to why $X' = X$ (that's what proof relevance is about, proofs are mathematical objects, they're not just published stories and logicians' fetishes):

Because $h : X' \to X$ is a homeomorphism, by the structure identity principle $\mathsf{sip}(h)$ proves $X = X'$. We may therefore transport any construction involving $X$ to one on $X'$ along $\mathsf{sip}(h)$. In particular, given $f : X \to Y$, there is $\mathsf{transport}_{\mathsf{sip}(h)}(f) : X' \to Y$. A little calculation reveals that $\mathsf{transport}_{\mathsf{sip}(h)}(f) = f \circ h$.

Note how instead of saying "isomorphic things are equal" we make things proof-relevant by saying "every isomorphism begets a proof of equality".

• Great answer most of the way, but I’d quibble with the last claim, “The standard solution is not to quotient the category but to pass to its skeleton.” That may be the naïve solution that people come up with when first encountering this situation — but surely the standard solution, in the sense of the solution followed by most workers and most of the literature, is to accept that one doesn’t really want the property “isomorphic objects are equal” after all, and be happy with the category Top. [cont’d] – Peter LeFanu Lumsdaine Jul 31 '18 at 21:36
• The issue underlying this is that while “isomorphic objects are equal” sounds appealing, it doesn’t really give anything useful. What does have payoffs is the stronger “isomorphisms correspond to equalities” (or similar properties), but these have the significant cost of needing to move away classical category theory to a richer setting — e.g. to something like ∞-toposes or HoTT. So these aren’t the “standard solution” either, at least not yet… – Peter LeFanu Lumsdaine Jul 31 '18 at 21:41
• Is there a useful HoTT answer here? There should be (I am thinking of the structure identity principle). – Andrej Bauer Jul 31 '18 at 21:55
• Let me just point out the simplest example showing that composition of isomorphism classes of functions is not defined. If $A$ and $B$ are respectively a two-element set and a three-element set then there are two classes of maps $A\to B$ (constant map and injection) and two classes of maps $B\to A$ (constant map and surjection). Surjection composed with injection is a map $A\to A$ that may be constant or bijection, depending on choices of representatives. – Tom Goodwillie Jul 31 '18 at 22:32
• (...) there are terms for various things a,b, and for every a,b there is a term for the "isom set" Isom(a,b), and the theory treats things like a and b on an equal footing as things like a=b. I think HoTT would look less "mystic" if the "identity terms" a=b were just denoted Isom(a,b) or just $a\cong b$. – Qfwfq Jul 31 '18 at 22:32