Add sifted and cosifted categories

[peabrainiac]

Add sifted / cosifted categories and show that filtered categories are sifted, that sifted categories are connected and that categories with finite coproducts are sifted.

These implications were enough to settle siftedness of all but 8 of the categories in the database and cosiftedness of all but 4. I've decided siftedness for most of these remaining examples manually; the only example I didn't decide is the delooping of the additive monoid of ordinal numbers, because I'm a bit confused about the order of composition that is used. The definition of left_cancellative seems to indicate that the composition of $X\overset f\to Y\overset g\to Z$ is denoted $f\circ g$ instead of $g\circ f$; is that a typo, or is that indeed the convention used here?

[ScriptRaccoon]

Thank you for the contribution! I will have a look at it.

I have fixed the typos in the definition of left and right cancellative categories: a58d2bf

You can rebase your PR on main.

[ScriptRaccoon]

Remark: I have added a commit that adds related properties (115ebd4). Maybe I should add this to CONTRIBUTING.md.

[peabrainiac]

I've rewritten the code using your suggestions now - that sifted + left cancellative => thin implication is a great one, it decided siftedness for all remaining categories but walking_span.

Thanks for your review, and more generally for starting this project; I'm excited to see where it will go.

[ScriptRaccoon]

I've rewritten the code using your suggestions now - that sifted + left cancellative => thin implication is a great one, it decided siftedness for all remaining categories but walking_span.

Great!

I love it when adding a property and a few implication decides it for nearly all categories. This is the best case scenario. It happened a few times already.

Thanks for your review, and more generally for starting this project; I'm excited to see where it will go.

Thank you for the contribution!

I have added a few minor commits and will merge the PR now.