Bicategorical foundations

Higher-categorical constructions currently formalized by the repository begin with Mathlib's bicategory hierarchy. In particular, adjunctions and adjoint equivalences belong here; ordinary adjoint functors are recovered through the Cat specialization.