Theorems · Theorem · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.mk.inj

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toLaxFunctor : CategoryTheory.LaxFunctor B C}
  {map_id :
    autoParam
      (∀ (X : B),
        toLaxFunctor.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (toLaxFunctor.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam}
  {mapId_eq_eqToHom :
    autoParam (∀ (X : B), toLaxFunctor.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam}
  {toLaxFunctor_1 : CategoryTheory.LaxFunctor B C}
  {map_id_1 :
    autoParam
      (∀ (X : B),
        toLaxFunctor_1.map (CategoryTheory.CategoryStruct.id X) =
          CategoryTheory.CategoryStruct.id (toLaxFunctor_1.obj X))
      CategoryTheory.StrictlyUnitaryLaxFunctor.map_id._autoParam}
  {mapId_eq_eqToHom_1 :
    autoParam (∀ (X : B), toLaxFunctor_1.mapId X = CategoryTheory.eqToHom ⋯)
      CategoryTheory.StrictlyUnitaryLaxFunctor.mapId_eq_eqToHom._autoParam},
  { toLaxFunctor := toLaxFunctor, map_id := map_id, mapId_eq_eqToHom := mapId_eq_eqToHom } =
      { toLaxFunctor := toLaxFunctor_1, map_id := map_id_1, mapId_eq_eqToHom := mapId_eq_eqToHom_1 } →
    toLaxFunctor = toLaxFunctor_1

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms