∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (hom : a ⟶ b) (inv : b ⟶ a)
  (unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom inv)
  (counit : CategoryTheory.CategoryStruct.comp inv hom ≅ CategoryTheory.CategoryStruct.id b)
  (left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit counit =
        CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam)
  (hom_1 : a ⟶ b) (inv_1 : b ⟶ a)
  (unit_1 : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom_1 inv_1)
  (counit_1 : CategoryTheory.CategoryStruct.comp inv_1 hom_1 ≅ CategoryTheory.CategoryStruct.id b)
  (left_triangle_1 :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit_1 counit_1 =
        CategoryTheory.Bicategory.leftUnitor hom_1 ≪≫ (CategoryTheory.Bicategory.rightUnitor hom_1).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam),
  ({ hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle } =
      { hom := hom_1, inv := inv_1, unit := unit_1, counit := counit_1, left_triangle := left_triangle_1 }) =
    (hom = hom_1 ∧ inv = inv_1 ∧ unit ≍ unit_1 ∧ counit ≍ counit_1)