Structures · Combinatorics
CategoryTheory.ReflQuiver
A reflexive quiver extends a quiver with a specified arrow id X : X ⟶ X for each X in its
type of objects. We denote these arrows by id since categories can be understood as an extension
of refl quivers.
- Defined in
- Mathlib.Combinatorics.Quiver.ReflQuiver
- Shape
- One type argument · adds id
Extends1
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Discrete
- CategoryTheory.Bundled.α
- SSet.OneTruncation₂
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by69
- CategoryTheory.ReflPrefunctor.toPrefunctor
- CategoryTheory.Cat.FreeRefl
- CategoryTheory.ReflQuiver.id
- CategoryTheory.Cat.FreeRefl.homMk
- CategoryTheory.ReflPrefunctor.comp
- CategoryTheory.Cat.FreeRefl.quotientFunctor
- CategoryTheory.ReflPrefunctor.id
- CategoryTheory.Cat.FreeRefl.lift
- CategoryTheory.ReflQuiv.of
- CategoryTheory.ReflQuiv.adj.homEquiv
- CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk
- CategoryTheory.Cat.toFreeRefl
- CategoryTheory.Cat.freeReflMap
- CategoryTheory.Cat.FreeRefl.lift_map
- CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk
- CategoryTheory.Cat.FreeRefl.homMk_id
- CategoryTheory.ReflPrefunctor.congr_obj
- CategoryTheory.Cat.FreeRefl.lift'
- CategoryTheory.Cat.FreeRefl.functor_ext
- CategoryTheory.ReflPrefunctor.congr_hom
- CategoryTheory.Cat.FreeRefl.lift_unique'
- CategoryTheory.Cat.FreeRefl.hom_induction
- CategoryTheory.Cat.FreeRefl.induction
- CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMk
- CategoryTheory.ReflPrefunctor.comp_assoc
- CategoryTheory.ReflQuiv.adj.homEquiv_naturality_right
- CategoryTheory.Cat.freeReflMap_naturality
- CategoryTheory.ReflPrefunctor.id_obj
- CategoryTheory.Cat.freeReflMap_obj
- CategoryTheory.ReflPrefunctor.id_comp
- CategoryTheory.Cat.freeReflMap_map
- CategoryTheory.Cat.FreeRefl.lift'_map
- CategoryTheory.ReflQuiv.adj.unit.map_app_eq
- CategoryTheory.Cat.toFreeRefl_map
- CategoryTheory.Cat.FreeRefl.quotientFunctor_map_nil
- CategoryTheory.ReflQuiv.adj_homEquiv
- CategoryTheory.Cat.FreeRefl.instUniqueHom
- CategoryTheory.Cat.FreeRefl.lift'_obj
- CategoryTheory.ReflQuiv.isoOfQuivIso
- CategoryTheory.ReflPrefunctor.instInhabited
- CategoryTheory.ReflPrefunctor.congr_map
- CategoryTheory.Cat.FreeRefl.lift_obj
- CategoryTheory.Cat.FreeRefl.instSubsingletonHomOfUnique
- CategoryTheory.ReflPrefunctor.ext'
- CategoryTheory.ReflPrefunctor.comp_obj
- CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id
- CategoryTheory.Cat.FreeRefl.instFullPathsQuotientFunctor
- CategoryTheory.ReflPrefunctor.map_id
- CategoryTheory.ReflPrefunctor.mk.congr_simp
- CategoryTheory.ReflQuiver.opposite