Theorems · Theorem · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.ext

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {x y : CategoryTheory.StrictlyUnitaryLaxFunctor B C},
  x.obj = y.obj →
    @Prefunctor.map B inst.toQuiver C inst_1.toQuiver x.toPrefunctor ≍
        @Prefunctor.map B inst.toQuiver C inst_1.toQuiver y.toPrefunctor →
      @CategoryTheory.PrelaxFunctorStruct.map₂ B inst.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) C inst_1.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) x.toPrelaxFunctorStruct ≍
          @CategoryTheory.PrelaxFunctorStruct.map₂ B inst.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) C inst_1.toQuiver
            (fun a b => (CategoryTheory.Bicategory.homCategory a b).toQuiver) y.toPrelaxFunctorStruct →
        x.mapId ≍ y.mapId →
          @CategoryTheory.LaxFunctor.mapComp B inst C inst_1 x.toLaxFunctor ≍
              @CategoryTheory.LaxFunctor.mapComp B inst C inst_1 y.toLaxFunctor →
            x = y

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Cited by

4 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms