Theorems · Theorem · category theory

CategoryTheory.ReflPrefunctor.mk.congr_simp

∀ {V : Type u₁} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W]
  (toPrefunctor toPrefunctor_1 : V ⥤q W) (e_toPrefunctor : toPrefunctor = toPrefunctor_1)
  (map_id :
    ∀ (X : V), toPrefunctor.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (toPrefunctor.obj X)),
  { toPrefunctor := toPrefunctor, map_id := map_id } = { toPrefunctor := toPrefunctor_1, map_id := ⋯ }

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver