Mathlib Map

Theorems · Definition · category theory

CategoryTheory.CatEnrichedOrdinary.toBase

{C : Type u} → CategoryTheory.CatEnrichedOrdinary C → CategoryTheory.CatEnriched C

The forgetful map from the type alias associated to EnrichedOrdinaryCategory Cat C and the type alias associated to EnrichedCategory Cat C is the identity on underlying types.

Defined in
Mathlib.CategoryTheory.Bicategory.CatEnriched
Cited by
16 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CategoryTheory.CatEnrichedOrdinary.homEquiv · cited by 18CatEnrichedOrdinary.homEq…CategoryTheory.CatEnrichedOrdinary.Hom.base · cited by 12Hom.baseCategoryTheory.CatEnrichedOrdinary.Hom.mk · cited by 7Hom.mkCategoryTheory.CatEnrichedOrdinary.homEquiv_comp · cited by 5CatEnrichedOrdinary.homEq…CategoryTheory.CatEnrichedOrdinary.Hom.ext · cited by 4Hom.extCategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom · cited by 3Hom.base_eqToHomCategoryTheory.CatEnrichedOrdinary.homEquiv_id · cited by 2CatEnrichedOrdinary.homEq…CategoryTheory.CatEnrichedOrdinary.hComp_id · cited by 1CatEnrichedOrdinary.hComp…CategoryTheory.CatEnrichedOrdinary.id_hComp · cited by 1CatEnrichedOrdinary.id_hC…CategoryTheory.CatEnrichedOrdinary.Hom.mk'.inj · cited by 1mk'.injCategoryTheory.CatEnrichedOrdinary.Hom.mk'.noConfusion · cited by 1mk'.noConfusionCategoryTheory.CatEnrichedOrdinary.Hom.casesOn · cited by 1Hom.casesOnCategoryTheory.CatEnrichedOrdinary.base_mk · cited by 0CatEnrichedOrdinary.base_…CategoryTheory.CatEnrichedOrdinary.Hom.mk'.injEq · cited by 0mk'.injEqCategoryTheory.CatEnrichedOrdinary.Hom.mk'.sizeOf_spec · cited by 0mk'.sizeOf_specCategoryTheory.CatEnriched · cited by 25CategoryTheory.CatEnrichedCategoryTheory.CatEnrichedOrdinary · cited by 24CategoryTheory.CatEnriche…CatEnrichedOrdinary.toBaseCITED BYCITES

Cites2

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

Cited by23

Results whose statement or proof uses this declaration.