Theorems · Theorem · category theory

CategoryTheory.StrictPseudofunctorCore.mk.injEq

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (toStrictPseudofunctorPreCore : CategoryTheory.StrictPseudofunctorPreCore B C)
  (map₂_left_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.Bicategory.leftUnitor (toStrictPseudofunctorPreCore.map f)).hom)
      CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor._autoParam)
  (map₂_right_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.Bicategory.rightUnitor (toStrictPseudofunctorPreCore.map f)).hom)
      CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor._autoParam)
  (map₂_associator :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (toStrictPseudofunctorPreCore.map f)
                  (toStrictPseudofunctorPreCore.map g) (toStrictPseudofunctorPreCore.map h)).hom
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorCore.map₂_associator._autoParam)
  (toStrictPseudofunctorPreCore_1 : CategoryTheory.StrictPseudofunctorPreCore B C)
  (map₂_left_unitor_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toStrictPseudofunctorPreCore_1.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.Bicategory.leftUnitor (toStrictPseudofunctorPreCore_1.map f)).hom)
      CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor._autoParam)
  (map₂_right_unitor_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toStrictPseudofunctorPreCore_1.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.Bicategory.rightUnitor (toStrictPseudofunctorPreCore_1.map f)).hom)
      CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor._autoParam)
  (map₂_associator_1 :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        toStrictPseudofunctorPreCore_1.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (toStrictPseudofunctorPreCore_1.map f)
                  (toStrictPseudofunctorPreCore_1.map g) (toStrictPseudofunctorPreCore_1.map h)).hom
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorCore.map₂_associator._autoParam),
  ({ toStrictPseudofunctorPreCore := toStrictPseudofunctorPreCore, map₂_left_unitor := map₂_left_unitor,
        map₂_right_unitor := map₂_right_unitor, map₂_associator := map₂_associator } =
      { toStrictPseudofunctorPreCore := toStrictPseudofunctorPreCore_1, map₂_left_unitor := map₂_left_unitor_1,
        map₂_right_unitor := map₂_right_unitor_1, map₂_associator := map₂_associator_1 }) =
    (toStrictPseudofunctorPreCore = toStrictPseudofunctorPreCore_1)

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory