Theorems · Theorem · category theory

CategoryTheory.PrelaxFunctorStruct.mk.inj

∀ {B : Type u₁} {inst : Quiver B} {inst_1 : (a b : B) → Quiver (a ⟶ b)} {C : Type u₂} {inst_2 : Quiver C}
  {inst_3 : (a b : C) → Quiver (a ⟶ b)} {toPrefunctor : B ⥤q C}
  {map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)} {toPrefunctor_1 : B ⥤q C}
  {map₂_1 : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor_1.map f ⟶ toPrefunctor_1.map g)},
  { toPrefunctor := toPrefunctor, map₂ := map₂ } = { toPrefunctor := toPrefunctor_1, map₂ := map₂_1 } →
    toPrefunctor = toPrefunctor_1 ∧ map₂ ≍ map₂_1

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms