Theorems · Theorem · category theory

CategoryTheory.PrelaxFunctor.mkOfHomFunctors_toPrelaxFunctorStruct

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B → C)
  (F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)),
  (CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').toPrelaxFunctorStruct =
    CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F fun a b => (F' a b).toPrefunctor

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory