Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Paths

Type u₁ → Type u₁

A type synonym for the category of paths in a quiver.

Defined in
Mathlib.CategoryTheory.PathCategory.Basic
Cited by
82 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Paths.of · cited by 20Paths.ofCategoryTheory.Cat.freeMap · cited by 13Cat.freeMapCategoryTheory.MorphismProperty.paths · cited by 13MorphismProperty.pathsCategoryTheory.pathComposition · cited by 9CategoryTheory.pathCompos…CategoryTheory.Cat.FreeRefl.quotientFunctor · cited by 8FreeRefl.quotientFunctorFreeSimplexQuiver.homRel · cited by 7FreeSimplexQuiver.homRelCategoryTheory.Localization.Construction.relations · cited by 7Construction.relationsCategoryTheory.Paths.lift · cited by 7Paths.liftQuiver.FreeGroupoid.redStep · cited by 7FreeGroupoid.redStepCategoryTheory.FreeBicategory.preinclusion · cited by 6FreeBicategory.preinclusi…SimplexCategoryGenRel.len · cited by 6SimplexCategoryGenRel.lenCategoryTheory.Paths.ext_functor · cited by 6Paths.ext_functorCategoryTheory.Cat.FreeReflRel · cited by 4Cat.FreeReflRelCategoryTheory.Cat.free · cited by 4Cat.freeCategoryTheory.FreeBicategory.normalizeIso · cited by 4FreeBicategory.normalizeI…CategoryTheory.PathsCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by128

Results whose statement or proof uses this declaration.