Commit 2025-04-18 20:06 1e71a028

feat(CategoryTheory): joins of categories (#23412) Define the join of two categories C, D as the category C ⋆ D characterized by the existence of fully faithful functors Join.inclLeft C D : C ⥤ C ⋆ D and Join.inclRight C D: D ⥤ C ⋆ D that are jointly surjective on objects, and such that there is a unique map edge c d : (inclLeft C D).obj c ⟶ (inclRight C D).obj d for every c : C and d : D. We also provide constructors for functors out of joins, and natural transforms between such functors. The main reference is Kerodon: section 1.4.3.2.