mathlib3

cd001b2d - feat(category_theory/bicategory/free): define free bicategories (#11998)