Mathlib Map

Theorems · Inductive type · category theory

CategoryTheory.Bundled

(Type u → Type v) → Type (max (u + 1) v)

Bundled is a type bundled with a type class instance for that type. Only the type class is exposed as a parameter.

Defined in
Mathlib.CategoryTheory.ConcreteCategory.Bundled
Cited by
42 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.Cat · cited by 884CategoryTheory.CatCategoryTheory.Bundled.α · cited by 736Bundled.αCategoryTheory.Grpd · cited by 30CategoryTheory.GrpdCategoryTheory.ReflQuiv · cited by 28CategoryTheory.ReflQuivCategoryTheory.Quiv · cited by 21CategoryTheory.QuivFirstOrder.Language.age · cited by 18Language.ageCategoryTheory.Bundled.str · cited by 18Bundled.strFirstOrder.Language.IsFraisse · cited by 11Language.IsFraisseFirstOrder.Language.IsFraisseLimit · cited by 7Language.IsFraisseLimitCategoryTheory.Bundled.of · cited by 6Bundled.ofFirstOrder.Language.Hereditary · cited by 5Language.HereditaryFirstOrder.Language.JointEmbedding · cited by 4Language.JointEmbeddingEquiv.bundledInduced · cited by 3Equiv.bundledInducedCardinal.Categorical.isComplete · cited by 3Categorical.isCompleteFirstOrder.Language.IsFraisseLimit.age · cited by 3IsFraisseLimit.ageCategoryTheory.BundledCITED 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 by68

Results whose statement or proof uses this declaration.