Thin categories, prosets as categories, and poset/toset/lattice (#4248)

* Move moel to main; add ThinCat and indiscrete category

* add thincc

* Add catcone0 to main; add catprs, prsthinc and related theorems

* remove ax-un dependency in f1omo

* remove ax-un for 2oexw and prsthinc

* remove ax-un and ax-pow for indthinc

* shorten 2oexw

* add mo0sn

* add mofasn2 and related

* add mofsn3 and rename theorems xxfa* -> xxf*

* add setcthin and setc2othin

* shorten proof by mof02

* rename mofsn3 -> mofmo; and fix description

* Add ProsetToCat defining and important properties

* added two redundant hypotheses to prstchom for explicitness

* add prstchom2ALT

* add thincn0eu and prstchom2

* revive ALT theorems

* prevent basendx usage

* shorten prstchomval

* sylibda->sylbida

* Add idmon and idepi

* add MndToCat

* add grptcmon and grptcepi

* add dtrucor3

* add monepilem, thincid, thincmon, thincepi; shorten grptcmon and grptcepi

* add mndtcbas2

* revise mndtcco2; add thinccic and related; add thinccd to shorten proofs

* move biadanid to main

* update changes-set.txt

* add postcpos and postc

* add catmnd

* add theorems from joindm2 to meetdm3; change chapter structure

* shorten postcpos

* add lubeldm2 and lubsscl and others

* add glbpr and lubpr

* split lubpr into 3; same for glbpr; shorten glbpr (now glbprlem)

* add toslat; move tospos, tleile, tltnle to main

* mention setcid and thincid to show how to prove (/) is the identity morphism of (/) in setc2o

* monepilem -> mpbiran3d; add mpbiran4d

* rename: catmnd -> endmndlem

* add posjidm and posmidm; fix latjidm and latmidm

* add ipolubdm and related

* prove ipolub

* prove ipoglb and ipoglbdm

* add oppcthin

* fix descriptions

* add mreclat, mrelatlubALT, and mrelatglbALT

* Add topclat

* Add ipolub00, ipoglb0; toplatlub/toplatglb/toplatglb0

* add topdlat and related

* add subthinc

* Add fullthinc

* revise fullthinc; add fullthinc2

* add thincfth

* move theorems related to functions to its right place

* Add functhinc; functhinclem1 -> mofeu

* detailed descriptions

* revert: set -> poset

* change tleile description based on BJ's suggestion

* change tltnle description based on BJ's suggestion

* change latjidm and latmidm description based on BJ's suggestion

* revert changes to mreclat.i and rename new mreclat.i to mreclatGOOD.i

---------

Co-authored-by: Benoit <[email protected]>