-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.mk : {B : Type u} →
  [toCategoryStruct : CategoryTheory.CategoryStruct.{v, u} B] →
    (homCategory :
        autoParam ((a b : B) → CategoryTheory.Category.{w, v} (a ⟶ b))
          CategoryTheory.Bicategory.homCategory._autoParam) →
      (whiskerLeft :
          {a b c : B} →
            (f : a ⟶ b) →
              {g h : b ⟶ c} →
                (g ⟶ h) → (CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f h)) →
        (whiskerRight :
            {a b c : B} →
              {f g : a ⟶ b} →
                (f ⟶ g) →
                  (h : b ⟶ c) → CategoryTheory.CategoryStruct.comp f h ⟶ CategoryTheory.CategoryStruct.comp g h) →
          (associator :
              {a b c d : B} →
                (f : a ⟶ b) →
                  (g : b ⟶ c) →
                    (h : c ⟶ d) →
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ≅
                        CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) →
            (leftUnitor :
                {a b : B} →
                  (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f) →
              (rightUnitor :
                  {a b : B} →
                    (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) ≅ f) →
                autoParam
                    (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                      whiskerLeft f (CategoryTheory.CategoryStruct.id g) =
                        CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
                    CategoryTheory.Bicategory.whiskerLeft_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
                        whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ) =
                          CategoryTheory.CategoryStruct.comp (whiskerLeft f η) (whiskerLeft f θ))
                      CategoryTheory.Bicategory.whiskerLeft_comp._autoParam →
                    autoParam
                        (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                          whiskerLeft (CategoryTheory.CategoryStruct.id a) η =
                            CategoryTheory.CategoryStruct.comp (leftUnitor f).hom
                              (CategoryTheory.CategoryStruct.comp η (leftUnitor g).inv))
                        CategoryTheory.Bicategory.id_whiskerLeft._autoParam →
                      autoParam
                          (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
                            whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η =
                              CategoryTheory.CategoryStruct.comp (associator f g h).hom
                                (CategoryTheory.CategoryStruct.comp (whiskerLeft f (whiskerLeft g η))
                                  (associator f g h').inv))
                          CategoryTheory.Bicategory.comp_whiskerLeft._autoParam →
                        autoParam
                            (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                              whiskerRight (CategoryTheory.CategoryStruct.id f) g =
                                CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g))
                            CategoryTheory.Bicategory.id_whiskerRight._autoParam →
                          autoParam
                              (∀ {a b c : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
                                whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i =
                                  CategoryTheory.CategoryStruct.comp (whiskerRight η i) (whiskerRight θ i))
                              CategoryTheory.Bicategory.comp_whiskerRight._autoParam →
                            autoParam
                                (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                                  whiskerRight η (CategoryTheory.CategoryStruct.id b) =
                                    CategoryTheory.CategoryStruct.comp (rightUnitor f).hom
                                      (CategoryTheory.CategoryStruct.comp η (rightUnitor g).inv))
                                CategoryTheory.Bicategory.whiskerRight_id._autoParam →
                              autoParam
                                  (∀ {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
                                    whiskerRight η (CategoryTheory.CategoryStruct.comp g h) =
                                      CategoryTheory.CategoryStruct.comp (associator f g h).inv
                                        (CategoryTheory.CategoryStruct.comp (whiskerRight (whiskerRight η g) h)
                                          (associator f' g h).hom))
                                  CategoryTheory.Bicategory.whiskerRight_comp._autoParam →
                                autoParam
                                    (∀ {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
                                      whiskerRight (whiskerLeft f η) h =
                                        CategoryTheory.CategoryStruct.comp (associator f g h).hom
                                          (CategoryTheory.CategoryStruct.comp (whiskerLeft f (whiskerRight η h))
                                            (associator f g' h).inv))
                                    CategoryTheory.Bicategory.whisker_assoc._autoParam →
                                  autoParam
                                      (∀ {a b c : B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
                                        CategoryTheory.CategoryStruct.comp (whiskerLeft f θ) (whiskerRight η i) =
                                          CategoryTheory.CategoryStruct.comp (whiskerRight η h) (whiskerLeft g θ))
                                      CategoryTheory.Bicategory.whisker_exchange._autoParam →
                                    autoParam
                                        (∀ {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
                                          CategoryTheory.CategoryStruct.comp (whiskerRight (associator f g h).hom i)
                                              (CategoryTheory.CategoryStruct.comp
                                                (associator f (CategoryTheory.CategoryStruct.comp g h) i).hom
                                                (whiskerLeft f (associator g h i).hom)) =
                                            CategoryTheory.CategoryStruct.comp
                                              (associator (CategoryTheory.CategoryStruct.comp f g) h i).hom
                                              (associator f g (CategoryTheory.CategoryStruct.comp h i)).hom)
                                        CategoryTheory.Bicategory.pentagon._autoParam →
                                      autoParam
                                          (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                                            CategoryTheory.CategoryStruct.comp
                                                (associator f (CategoryTheory.CategoryStruct.id b) g).hom
                                                (whiskerLeft f (leftUnitor g).hom) =
                                              whiskerRight (rightUnitor f).hom g)
                                          CategoryTheory.Bicategory.triangle._autoParam →
                                        CategoryTheory.Bicategory B