-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {X Y : B} → (X ⟶ Y) → (obj X ⟶ obj Y))
  (map_id :
    autoParam (∀ (X : B), map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj X))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map_id._autoParam)
  (map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map f ⟶ map g))
  (map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b), map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (map f))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_id._autoParam)
  (map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (map₂ η) (map₂ θ))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_comp._autoParam)
  (mapComp :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) → map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_whisker_left :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
        map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (mapComp f g).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (map₂ η))
              (mapComp f h).inv))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_left._autoParam)
  (map₂_whisker_right :
    autoParam
      (∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
        map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
          CategoryTheory.CategoryStruct.comp (mapComp f h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (map₂ η) (map h))
              (mapComp g h).inv))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_right._autoParam)
  (map₂_left_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id a) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_left_unitor._autoParam)
  (map₂_right_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_right_unitor._autoParam)
  (map₂_associator :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        map₂ (CategoryTheory.Bicategory.associator f g h).hom =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_associator._autoParam)
  (obj_1 : B → C) (map_1 : {X Y : B} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y))
  (map_id_1 :
    autoParam (∀ (X : B), map_1 (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (obj_1 X))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map_id._autoParam)
  (map₂_1 : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (map_1 f ⟶ map_1 g))
  (map₂_id_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂_1 (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (map_1 f))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_id._autoParam)
  (map₂_comp_1 :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        map₂_1 (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (map₂_1 η) (map₂_1 θ))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_comp._autoParam)
  (mapComp_1 :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          map_1 (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map_1 f) (map_1 g))
  (map₂_whisker_left_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
        map₂_1 (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (mapComp_1 f g).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map_1 f) (map₂_1 η))
              (mapComp_1 f h).inv))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_left._autoParam)
  (map₂_whisker_right_1 :
    autoParam
      (∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
        map₂_1 (CategoryTheory.Bicategory.whiskerRight η h) =
          CategoryTheory.CategoryStruct.comp (mapComp_1 f h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (map₂_1 η) (map_1 h))
              (mapComp_1 g h).inv))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_right._autoParam)
  (map₂_left_unitor_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂_1 (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp_1 (CategoryTheory.CategoryStruct.id a) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (CategoryTheory.Bicategory.leftUnitor (map_1 f)).hom))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_left_unitor._autoParam)
  (map₂_right_unitor_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        map₂_1 (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp_1 f (CategoryTheory.CategoryStruct.id b)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (CategoryTheory.Bicategory.rightUnitor (map_1 f)).hom))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_right_unitor._autoParam)
  (map₂_associator_1 :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        map₂_1 (CategoryTheory.Bicategory.associator f g h).hom =
          CategoryTheory.CategoryStruct.comp (mapComp_1 (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp_1 f g).hom (map_1 h))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (map_1 f) (map_1 g) (map_1 h)).hom
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerLeft (map_1 f) (mapComp_1 g h).inv)
                  (mapComp_1 f (CategoryTheory.CategoryStruct.comp g h)).inv))))
      CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_associator._autoParam),
  ({ obj := obj, map := map, map_id := map_id, map₂ := map₂, map₂_id := map₂_id, map₂_comp := map₂_comp,
        mapComp := mapComp, map₂_whisker_left := map₂_whisker_left, map₂_whisker_right := map₂_whisker_right,
        map₂_left_unitor := map₂_left_unitor, map₂_right_unitor := map₂_right_unitor,
        map₂_associator := map₂_associator } =
      { obj := obj_1, map := map_1, map_id := map_id_1, map₂ := map₂_1, map₂_id := map₂_id_1, map₂_comp := map₂_comp_1,
        mapComp := mapComp_1, map₂_whisker_left := map₂_whisker_left_1, map₂_whisker_right := map₂_whisker_right_1,
        map₂_left_unitor := map₂_left_unitor_1, map₂_right_unitor := map₂_right_unitor_1,
        map₂_associator := map₂_associator_1 }) =
    (obj = obj_1 ∧ map ≍ map_1 ∧ map₂ ≍ map₂_1 ∧ mapComp ≍ mapComp_1)