Mathlib Map

Theorems · Inductive type · category theory

CategoryTheory.Discrete

Type u₁ → Type u₁

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

Defined in
Mathlib.CategoryTheory.Discrete.Basic
Cited by
2,447 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.

CategoryTheory.Functor.fromPUnit · cited by 769Functor.fromPUnitCategoryTheory.Discrete.functor · cited by 633Discrete.functorCategoryTheory.Limits.pair · cited by 536Limits.pairCategoryTheory.Discrete.as · cited by 269Discrete.asCategoryTheory.Limits.HasInitial · cited by 185Limits.HasInitialCategoryTheory.Limits.Cofan.inj · cited by 170Cofan.injCategoryTheory.Limits.HasTerminal · cited by 142Limits.HasTerminalCategoryTheory.Limits.HasCoproducts · cited by 119Limits.HasCoproductsCategoryTheory.Limits.BinaryFan.mk · cited by 112BinaryFan.mkCategoryTheory.Limits.Cofan.mk · cited by 105Cofan.mkCategoryTheory.Limits.HasProducts · cited by 103Limits.HasProductsCategoryTheory.Functor.empty · cited by 103Functor.emptyCategoryTheory.Limits.HasBinaryCoproducts · cited by 98Limits.HasBinaryCoproductsCategoryTheory.Over.map · cited by 97Over.mapCategoryTheory.Discrete.casesOn · cited by 90Discrete.casesOnCategoryTheory.DiscreteCITED 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 by3,309

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 3,309.