Theorems · Definition · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.mk.noConfusion

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

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms