Theorems · Theorem · category theory

CategoryTheory.ReflQuiv.adj_homEquiv

∀ (V : Type u) [inst : CategoryTheory.ReflQuiver V] (C : Type u) [inst_1 : CategoryTheory.Category.{max u v, u} C],
  CategoryTheory.ReflQuiv.adj.homEquiv (CategoryTheory.ReflQuiv.of V) (CategoryTheory.Cat.of C) =
    (CategoryTheory.Cat.Hom.equivFunctor (CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of V))
          (CategoryTheory.Cat.of C)).trans
      CategoryTheory.ReflQuiv.adj.homEquiv

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.Category