Mathlib Map

Theorems · Inductive type · category theory

CategoryTheory.LocallyDiscrete

Type u → Type u

A wrapper for promoting any category to a bicategory, with the only 2-morphisms being equalities.

Defined in
Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
Cited by
318 results in Mathlib
Foundations
Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Quiver.Hom.toLoc · cited by 150Hom.toLocCategoryTheory.Pseudofunctor.DescentData · cited by 74Pseudofunctor.DescentDataCategoryTheory.LocallyDiscrete.as · cited by 61LocallyDiscrete.asCategoryTheory.Pseudofunctor.DescentData.obj · cited by 44DescentData.objCategoryTheory.Pseudofunctor.DescentDataAsCoalgebra · cited by 39Pseudofunctor.DescentData…CategoryTheory.Pseudofunctor.DescentData' · cited by 38Pseudofunctor.DescentData'CategoryTheory.Pseudofunctor.CoGrothendieck · cited by 34Pseudofunctor.CoGrothendi…CategoryTheory.Pseudofunctor.DescentData'.obj · cited by 31DescentData'.objCategoryTheory.Pseudofunctor.DescentData'.pullHom' · cited by 29DescentData'.pullHom'CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.obj · cited by 29DescentDataAsCoalgebra.objCategoryTheory.Pseudofunctor.DescentData.hom · cited by 28DescentData.homCategoryTheory.Pseudofunctor.Grothendieck · cited by 25Pseudofunctor.GrothendieckCategoryTheory.Pseudofunctor.CoGrothendieck.base · cited by 25CoGrothendieck.baseCategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom · cited by 23LocallyDiscreteOpToCat.pu…CategoryTheory.Pseudofunctor.DescentData.Hom.hom · cited by 23Hom.homCategoryTheory.LocallyDiscreteCITED 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 by493

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 493.