Theorems · Theorem · category theory

CategoryTheory.StrictPseudofunctor.mk.injEq

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (toStrictlyUnitaryPseudofunctor : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (map_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor.map f)
            (toStrictlyUnitaryPseudofunctor.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam)
  (mapComp_eq_eqToIso :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam)
  (toStrictlyUnitaryPseudofunctor_1 : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (map_comp_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        toStrictlyUnitaryPseudofunctor_1.map (CategoryTheory.CategoryStruct.comp f g) =
          CategoryTheory.CategoryStruct.comp (toStrictlyUnitaryPseudofunctor_1.map f)
            (toStrictlyUnitaryPseudofunctor_1.map g))
      CategoryTheory.StrictPseudofunctor.map_comp._autoParam)
  (mapComp_eq_eqToIso_1 :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), toStrictlyUnitaryPseudofunctor_1.mapComp f g = CategoryTheory.eqToIso ⋯)
      CategoryTheory.StrictPseudofunctor.mapComp_eq_eqToIso._autoParam),
  ({ toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor, map_comp := map_comp,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso } =
      { toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor_1, map_comp := map_comp_1,
        mapComp_eq_eqToIso := mapComp_eq_eqToIso_1 }) =
    (toStrictlyUnitaryPseudofunctor = toStrictlyUnitaryPseudofunctor_1)

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Cited by

0 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory