feat(CategoryTheory/Presentable): the uniformization theorem

[joelriou]

sorry free WIP

---

• depends on: feat(CategoryTheory/Presentable): equivalence between the various definitions of sharply smaller regular cardinals #41232
• depends on: [Merged by Bors] - feat(CategoryTheory/Presentable): sharply smaller regular cardinals #40937
• depends on: [Merged by Bors] - feat(CategoryTheory): the category of κ-directed posets #39669
• depends on: [Merged by Bors] - feat(CategoryTheory): the κ-accessible category of κ-directed posets #39655
• depends on: [Merged by Bors] - feat(CategoryTheory/Presentable): presentable objects in Type #30727
• depends on: [Merged by Bors] - feat(CategoryTheory): a category with a terminal object is κ-filtered #31767
• depends on: [Merged by Bors] - feat(CategoryTheory): strong generators #29519
• depends on: [Merged by Bors] - feat(CategoryTheory): a property of objects is a strong generator if any object is a colimit of objects satisfying the property #29543
• depends on: [Merged by Bors] - feat(CategoryTheory): dense functors #29565
• depends on: [Merged by Bors] - feat(CategoryTheory/ObjectProperty): closure of a property under certain limits #29854
• depends on: [Merged by Bors] - refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) #30459
• depends on: [Merged by Bors] - feat(CategoryTheory): for any filtered category, there exists a final functor from a directed poset #30605
• depends on: [Merged by Bors] - feat(CategoryTheory): DiagramWithUniqueTerminal #31426
• depends on: [Merged by Bors] - feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty #31421
• depends on: [Merged by Bors] - feat(SetTheory): more API for HasCardinalLT #30633
• depends on: [Merged by Bors] - feat(CategoryTheory): κ-filtered categories are stable under products #30634
• depends on: [Merged by Bors] - feat(Order/Category): partial orders with order embeddings as morphisms #30693
• depends on: [Merged by Bors] - feat(Order/Category): PartOrdEmb has filtered colimits #30696
• depends on: [Merged by Bors] - feat(CategoryTheory): characterization of κ-filtered categories #30781

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.