Theorems · Theorem · category theory

CategoryTheory.Quiv.adj_homEquiv

∀ {V C : Type u} [inst : Quiver V] [inst_1 : CategoryTheory.Category.{max u v, u} C],
  CategoryTheory.Quiv.adj.homEquiv (CategoryTheory.Quiv.of V) (CategoryTheory.Cat.of C) =
    (CategoryTheory.Cat.Hom.equivFunctor (CategoryTheory.Cat.of (CategoryTheory.Paths V))
          (CategoryTheory.Cat.of C)).trans
      CategoryTheory.Quiv.pathsEquiv

Defined in

Mathlib.CategoryTheory.Category.Quiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

QuiverCategoryTheory.Category