Theorems · Theorem · category theory

CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right

∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] {C : Type u_3} {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{v_1, u_3} C] [inst_2 : CategoryTheory.Category.{v_2, u_4} D]
  (F : CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) C) (G : CategoryTheory.Functor C D),
  CategoryTheory.ReflQuiv.adj.homEquiv (F.comp G) = CategoryTheory.ReflQuiv.adj.homEquiv F ⋙rq G.toReflPrefunctor

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.ReflQuiverCategoryTheory.CategoryCategoryTheory.Category