Theorems · Theorem · category theory

CategoryTheory.PrelaxFunctorStruct.mk.injEq

∀ {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

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

QuiverQuiverQuiverQuiver