Add category of compact Hausdorff spaces

[dschepler]

I thought I'd like to take a break from the properties side of things, and add a category example of the category Comp of compact Hausdorff spaces. Among the properties which are interesting to me:

• It's a pretopos, but it doesn't have a subobject classifier, nor is it cartesian closed.
• In contrast to the example of Set_c of a non-topos pretopos, it is both complete and cocomplete.
• It has a cogenerator $[0,1]$ by Urysohn's lemma.
• It is monadic over Set, but (presumably) not finitary algebraic. (At the very least, the canonical forgetful functor is monadic, but it does not preserve sequential colimits.)
• It is extensive and cocomplete but not infinitary extensive. (I think the latter will be automatically deduced using the Girard's theorem based implication.)
• The implications will auto-deduce that it's balanced, thus automatically proving the interesting theorem that a bijective continuous function between compact Hausdorff spaces is a homeomorphism.

[ScriptRaccoon]

This is a very interesting example we should definitely add. Do you want to work on this?

In my experience, adding a category is much easier and faster than adding a property.

[dschepler]

Do you want to work on this?

Yes, that was my intention.

I notice in the parent issue you used CompHaus which I also like better than Comp. (I was just choosing the latter to match what nLab called it.)

[ScriptRaccoon]

Yes, longer names tend to be better, because they tell the reader exactly what it is, and also they are more future-proof. When we want to add the category of compact abelian groups (which should also happen at some point), CompAb is the obvious candidate, and then having Comp and CompAb at the same time looks weird, but CompHaus and CompAb (and CompTop, CompMet, CompCRing, etc.) look nice together. For this reason I also went for SemiNormVect.

[dschepler]

I have questions about the proof that Haus does not have filtered-colimit-stable monomorphisms, which I was considering trying to adapt to CompHaus. The main point is: did you mean to make $X_n$ be the double line with $(\infty, -\frac{1}{n}]$ and $[\frac{1}{n}, \infty)$ identified? That would make more sense in the construction of surjective continuous maps $X_n \to X_{n+1}$, and in the colimit in Top being the line with doubled origin.

[ScriptRaccoon]

This sounds correct. I would appreciate if you fix the proof for Haus then. I'm glad it's just a "notation bug".