Theorems · Definition · category theory
CategoryTheory.Cat.toFreeRefl
(V : Type u_1) → [inst : CategoryTheory.ReflQuiver V] → V ⥤rq CategoryTheory.Cat.FreeRefl V
Given a refl quiver V, this is the refl functor V ⥤rq FreeRefl V which
is the counit of the adjunction between reflexive quivers and categories.
- Defined in
- Mathlib.CategoryTheory.Category.ReflQuiv
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
- Assumes
- CategoryTheory.ReflQuiver
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.ReflQuiverstatement and proof · cited by 64
- CategoryTheory.Cat.FreeReflstatement · cited by 34
- CategoryTheory.ReflPrefunctorstatement · cited by 30
- CategoryTheory.Cat.FreeRefl.mkproof · cited by 17
- CategoryTheory.Cat.FreeRefl.homMkproof · cited by 13
Cited by6
Results whose statement or proof uses this declaration.
- CategoryTheory.ReflQuiv.adj.homEquivproof · cited by 5
- CategoryTheory.Cat.FreeRefl.lift_specstatement · cited by 0
- CategoryTheory.ReflQuiv.adj_unit_appstatement · cited by 0
- CategoryTheory.ReflQuiv.adj.homEquiv_applystatement · cited by 0
- CategoryTheory.Cat.toFreeRefl_mapstatement and proof · cited by 0
- CategoryTheory.Cat.toFreeRefl_objstatement and proof · cited by 0