Theorems · Theorem · category theory

CategoryTheory.PrelaxFunctor.mk.inj

∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {toPrelaxFunctorStruct : CategoryTheory.PrelaxFunctorStruct B C}
  {map₂_id :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam}
  {map₂_comp :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct.map₂ η) (toPrelaxFunctorStruct.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam}
  {toPrelaxFunctorStruct_1 : CategoryTheory.PrelaxFunctorStruct B C}
  {map₂_id_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toPrelaxFunctorStruct_1.map₂ (CategoryTheory.CategoryStruct.id f) =
          CategoryTheory.CategoryStruct.id (toPrelaxFunctorStruct_1.map f))
      CategoryTheory.PrelaxFunctor.map₂_id._autoParam}
  {map₂_comp_1 :
    autoParam
      (∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
        toPrelaxFunctorStruct_1.map₂ (CategoryTheory.CategoryStruct.comp η θ) =
          CategoryTheory.CategoryStruct.comp (toPrelaxFunctorStruct_1.map₂ η) (toPrelaxFunctorStruct_1.map₂ θ))
      CategoryTheory.PrelaxFunctor.map₂_comp._autoParam},
  { toPrelaxFunctorStruct := toPrelaxFunctorStruct, map₂_id := map₂_id, map₂_comp := map₂_comp } =
      { toPrelaxFunctorStruct := toPrelaxFunctorStruct_1, map₂_id := map₂_id_1, map₂_comp := map₂_comp_1 } →
    toPrelaxFunctorStruct = toPrelaxFunctorStruct_1

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms