Bicategories

This is the repository extension root for bicategorical mathematics. The underlying notion is Mathlib's CategoryTheory.Bicategory; repository code must extend that hierarchy rather than introduce a parallel notion of a 2-category.