∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (e : CategoryTheory.Bicategory.Equivalence a b),
  CategoryTheory.Bicategory.leftZigzag e.unit.hom e.counit.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor e.hom).hom
      (CategoryTheory.Bicategory.rightUnitor e.hom).inv