Theorems · Definition · category theory
CategoryTheory.ReflPrefunctor.toPrefunctor
{V : Type u₁} →
[inst : CategoryTheory.ReflQuiver V] → {W : Type u₂} → [inst_1 : CategoryTheory.ReflQuiver W] → V ⥤rq W → V ⥤q W- Defined in
- Mathlib.Combinatorics.Quiver.ReflQuiver
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Prefunctorstatement · cited by 116
- CategoryTheory.ReflQuiverstatement and proof · cited by 64
- CategoryTheory.ReflPrefunctorstatement and proof · cited by 30
Cited by41
Results whose statement or proof uses this declaration.
- CategoryTheory.ReflPrefunctor.compproof · cited by 11
- CategoryTheory.Cat.FreeRefl.liftproof · cited by 6
- CategoryTheory.Cat.freeReflMapproof · cited by 5
- CategoryTheory.ReflQuiv.forgetToQuivproof · cited by 4
- CategoryTheory.Cat.FreeRefl.lift_mapstatement and proof · cited by 4
- CategoryTheory.ReflPrefunctor.congr_objstatement and proof · cited by 2
- SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMkproof · cited by 1
- SSet.OneTruncation₂.map_mapstatement and proof · cited by 1
- CategoryTheory.ReflPrefunctor.congr_homstatement and proof · cited by 1
- CategoryTheory.ReflPrefunctor.extstatement and proof · cited by 1
- CategoryTheory.ReflQuiv.adj.homEquiv_naturality_left_symmproof · cited by 0
- CategoryTheory.ReflQuiv.comp_mapstatement · cited by 0