Define the category of posets

[anshwad10]

This is part of my project to formalize Hadzihasanovic's work (#1218). The PR #1219 had a lot of different things and it was getting to big, so I'm splitting it.

[maxsnew]

Should this be called POSET or PosetCategory or PosetsCategory? I think the library is inconsistent about this now, i.e., we have SET and we have PresheafCategory but I don't think anything follows the structure of PosetsCategory.

[anshwad10]

I was following the naming convention of CommRingsCategory, LatticesCategory etc. PosetCategory is already used for the construction of a thin category from a poset.

[maxsnew]

Oh lord, it's even worse than I realized. We should try to get a bit more consistency with that. Personally I think singular would be better (for the same reason we call the type Poset and not Posets) but I'll move that discussion elsewhere.