∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {X Y Z : CategoryTheory.Bicategory.Adj B}
  (f : CategoryTheory.Bicategory.Adj.Hom X.obj Y.obj) (g : CategoryTheory.Bicategory.Adj.Hom Y.obj Z.obj),
  (CategoryTheory.CategoryStruct.comp f g).r = CategoryTheory.CategoryStruct.comp g.r f.r