Theorems · Theorem · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.ext_iff

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {x y : CategoryTheory.StrictlyUnitaryLaxFunctor B C},
  x = y ↔
    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

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms