-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toPrelaxFunctor : CategoryTheory.PrelaxFunctor B C}
  {mapId :
    (a : B) →
      toPrelaxFunctor.map (CategoryTheory.CategoryStruct.id a) ≅
        CategoryTheory.CategoryStruct.id (toPrelaxFunctor.obj a)}
  {mapComp :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          toPrelaxFunctor.map (CategoryTheory.CategoryStruct.comp f g) ≅
            CategoryTheory.CategoryStruct.comp (toPrelaxFunctor.map f) (toPrelaxFunctor.map g)}
  {map₂_whisker_left :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (mapComp f g).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (toPrelaxFunctor.map₂ η))
              (mapComp f h).inv))
      CategoryTheory.Pseudofunctor.map₂_whisker_left._autoParam}
  {map₂_whisker_right :
    autoParam
      (∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
          CategoryTheory.CategoryStruct.comp (mapComp f h).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor.map₂ η) (toPrelaxFunctor.map h))
              (mapComp g h).inv))
      CategoryTheory.Pseudofunctor.map₂_whisker_right._autoParam}
  {map₂_associator :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        toPrelaxFunctor.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 (toPrelaxFunctor.map h))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (toPrelaxFunctor.map f) (toPrelaxFunctor.map g)
                    (toPrelaxFunctor.map h)).hom
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))))
      CategoryTheory.Pseudofunctor.map₂_associator._autoParam}
  {map₂_left_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id a) f).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (mapId a).hom (toPrelaxFunctor.map f))
              (CategoryTheory.Bicategory.leftUnitor (toPrelaxFunctor.map f)).hom))
      CategoryTheory.Pseudofunctor.map₂_left_unitor._autoParam}
  {map₂_right_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctor.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b)).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor.map f) (mapId b).hom)
              (CategoryTheory.Bicategory.rightUnitor (toPrelaxFunctor.map f)).hom))
      CategoryTheory.Pseudofunctor.map₂_right_unitor._autoParam}
  {toPrelaxFunctor_1 : CategoryTheory.PrelaxFunctor B C}
  {mapId_1 :
    (a : B) →
      toPrelaxFunctor_1.map (CategoryTheory.CategoryStruct.id a) ≅
        CategoryTheory.CategoryStruct.id (toPrelaxFunctor_1.obj a)}
  {mapComp_1 :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          toPrelaxFunctor_1.map (CategoryTheory.CategoryStruct.comp f g) ≅
            CategoryTheory.CategoryStruct.comp (toPrelaxFunctor_1.map f) (toPrelaxFunctor_1.map g)}
  {map₂_whisker_left_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
        toPrelaxFunctor_1.map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
          CategoryTheory.CategoryStruct.comp (mapComp_1 f g).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor_1.map f) (toPrelaxFunctor_1.map₂ η))
              (mapComp_1 f h).inv))
      CategoryTheory.Pseudofunctor.map₂_whisker_left._autoParam}
  {map₂_whisker_right_1 :
    autoParam
      (∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
        toPrelaxFunctor_1.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
          CategoryTheory.CategoryStruct.comp (mapComp_1 f h).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (toPrelaxFunctor_1.map₂ η) (toPrelaxFunctor_1.map h))
              (mapComp_1 g h).inv))
      CategoryTheory.Pseudofunctor.map₂_whisker_right._autoParam}
  {map₂_associator_1 :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        toPrelaxFunctor_1.map₂ (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 (toPrelaxFunctor_1.map h))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (toPrelaxFunctor_1.map f) (toPrelaxFunctor_1.map g)
                    (toPrelaxFunctor_1.map h)).hom
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor_1.map f) (mapComp_1 g h).inv)
                  (mapComp_1 f (CategoryTheory.CategoryStruct.comp g h)).inv))))
      CategoryTheory.Pseudofunctor.map₂_associator._autoParam}
  {map₂_left_unitor_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctor_1.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp_1 (CategoryTheory.CategoryStruct.id a) f).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (mapId_1 a).hom (toPrelaxFunctor_1.map f))
              (CategoryTheory.Bicategory.leftUnitor (toPrelaxFunctor_1.map f)).hom))
      CategoryTheory.Pseudofunctor.map₂_left_unitor._autoParam}
  {map₂_right_unitor_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctor_1.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (mapComp_1 f (CategoryTheory.CategoryStruct.id b)).hom
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft (toPrelaxFunctor_1.map f) (mapId_1 b).hom)
              (CategoryTheory.Bicategory.rightUnitor (toPrelaxFunctor_1.map f)).hom))
      CategoryTheory.Pseudofunctor.map₂_right_unitor._autoParam},
  { toPrelaxFunctor := toPrelaxFunctor, mapId := mapId, mapComp := mapComp, map₂_whisker_left := map₂_whisker_left,
        map₂_whisker_right := map₂_whisker_right, map₂_associator := map₂_associator,
        map₂_left_unitor := map₂_left_unitor, map₂_right_unitor := map₂_right_unitor } =
      { toPrelaxFunctor := toPrelaxFunctor_1, mapId := mapId_1, mapComp := mapComp_1,
        map₂_whisker_left := map₂_whisker_left_1, map₂_whisker_right := map₂_whisker_right_1,
        map₂_associator := map₂_associator_1, map₂_left_unitor := map₂_left_unitor_1,
        map₂_right_unitor := map₂_right_unitor_1 } →
    toPrelaxFunctor = toPrelaxFunctor_1 ∧ mapId ≍ mapId_1 ∧ mapComp ≍ mapComp_1