Theorems · Definition · category theory

CategoryTheory.ReflQuiv.adj.homEquiv

{V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_1, u_3} C] →
        CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) C ≃ V ⥤rq C

Given a reflexive quiver V and a category C, this is the bijection between functors Cat.FreeRefl V ⥤ C and refl functors V ⥤rq C.

Defined in

Mathlib.CategoryTheory.Category.ReflQuiv

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.ReflQuiverCategoryTheory.Category