Theorems · Definition · category theory

CategoryTheory.StrictPseudofunctor.mk.noConfusion

{B : Type u₁} →
  {inst : CategoryTheory.Bicategory B} →
    {C : Type u₂} →
      {inst_1 : CategoryTheory.Bicategory C} →
        {P : Sort u} →
          {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' : 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 := toStrictlyUnitaryPseudofunctor, map_comp := map_comp,
                            mapComp_eq_eqToIso := mapComp_eq_eqToIso } =
                          { toStrictlyUnitaryPseudofunctor := toStrictlyUnitaryPseudofunctor', map_comp := map_comp',
                            mapComp_eq_eqToIso := mapComp_eq_eqToIso' } →
                        (toStrictlyUnitaryPseudofunctor ≍ toStrictlyUnitaryPseudofunctor' → P) → P

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Cited by

1 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext