Commit 2020-09-11 17:48 5509a30a

feat(category_theory/skeleton): add skeletal categories and construct a special case (#3929) I'm interested in the quotient construction of the skeleton for a thin category in particular for topos and sheafification PRs, but of course the general construction is useful too, so I've marked that as TODO and I'll make a followup PR so that this one doesn't get too big. The advantage of handling this special case separately is that the skeleton of a thin category is a partial order, and so lattice constructions can be used (which is needed for my application), and also there are nice definitional equalities.