Add more well-known categories

[ScriptRaccoon]

While CatDat already has a couple of well-known categories, some are currently missing. Here are some suggestions. Done categories are moved to the bottom.

Notation	Category	Links	Done
$Grp_{fg}$	finitely-generated groups		❌
$Grp_{fp}$	finitely-presented groups		❌
$Ab_{c}$	countable abelian groups		❌
$grMod_R$	Graded modules		❌
$CGWH$	compactly generated weak Hausdorff spaces		❌
$hTop$	Homotopy category of Top		❌
$TopGrp$	Topological groups		❌
$LCH$	locally compact hausdorff spaces		❌
$Ban_c$	Banach spaces with continuous linear maps	MSE/1424777	❌
$TopVect$	Topological vector spaces		❌
$NormVect$	Normed vector spaces	WIP, #127	❌
$CompMet$	Compact metric spaces	MSE	❌
$C^*-Alg$	C*-algebras		❌
$LawMet$	Lawvere metric spaces		❌
$Mod(O_X)$	Modules over a sheaf of rings		❌
$RS$	Ringed spaces		❌
$Qcoh(X)$	Quasi-coherent sheaves	Thesis	❌
$Alg(O_X)$	Algebras over a sheaf of rings		❌
$Unif$	uniform spaces*	MO	❌
$Stoch$	measurable spaces with Markov kernels	nlab	❌
$\Pi_1(X)$	fundamental groupoid of a (specific) space, say $X = S^1$		❌
$Born$	bornological sets / spaces		❌
$Grp_{c}$	countable groups		✅
$CompHaus$	Compact Hausdorff spaces		✅
$Haus$	Hausdorff spaces		✅
$\Delta$	Simplex category		✅
$SemiGrp$	semigroups		✅
$TorsAb$	torsion abelian groups		✅

*either with continuous or uniform maps, not sure yet

Also:

1. Add the categories from https://math.stackexchange.com/questions/4481902/locally-presentable-vs-compactly-presentable-categories
2. Add the categories from https://mathoverflow.net/questions/258269/cocomplete-topoi-that-are-not-grothendieck
3. Add the categories from https://math.stackexchange.com/questions/2864916/ (two locally cartesian closed categories that are not cartesian closed)

IMPORTANT. Adding these categories to the categories table is easy, but not sufficient, since (see CONTRIBUTING.md) one should also try to fill in the properties and non-properties (in case they are not deduced already). So this is actually a quite big task. Maybe one can make one commit (or PR) per category.

[diracdeltafunk]

I assume by hTop you mean the "StrØm homotopy category", i.e. take the category of (all, or maybe just CGWH) topological spaces and identify any two parallel morphisms which happen to be homotopic (this is also the homotopy category of the StrØm model structure).

There is also Ho(Top), the homotopy category of spaces with respect to the "Quillen" model structure (weak equivalences = weak homotopy equivalences). Would be nice to see both in CatDat!

---

More suggestions:

• Span(FinSet) nlab link
• Pro(FinSet) nlab link
• Cond(Set) nlab link
• Pyk(Set) nlab link

---

If I find some time I'll try to learn how the database looks and add these myself.