Structures · Category theory
CategoryTheory.EnrichedOrdinaryCategory
An enriched ordinary category is a category C that is also enriched
over a category V in such a way that morphisms X ⟶ Y in C identify
to morphisms 𝟙_ V ⟶ (X ⟶[V] Y) in V.
- Shape
- 2 explicit arguments · adds homEquiv, homEquiv_id, homEquiv_comp
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.Cat
How is a type an instance?
Loading the hierarchy index…
Assumed by159
- CategoryTheory.Enriched.FunctorCategory.enrichedHom
- CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom
- CategoryTheory.eHomWhiskerLeft
- CategoryTheory.eHomEquiv
- CategoryTheory.eHomWhiskerRight
- CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom
- CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom
- CategoryTheory.CatEnrichedOrdinary.homEquiv
- CategoryTheory.Enriched.FunctorCategory.diagram
- CategoryTheory.Enriched.FunctorCategory.enrichedComp
- CategoryTheory.Enriched.FunctorCategory.enrichedHomπ
- CategoryTheory.CatEnrichedOrdinary.Hom.base
- CategoryTheory.Iso.eHomCongr
- CategoryTheory.CatEnrichedOrdinary.hComp
- CategoryTheory.Enriched.FunctorCategory.enrichedId
- CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp
- CategoryTheory.Enriched.FunctorCategory.homEquiv
- CategoryTheory.Enriched.FunctorCategory.enrichedComp_π
- CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom
- CategoryTheory.Enriched.FunctorCategory.functorEnrichedId
- CategoryTheory.eHomWhiskerLeft_id
- CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π
- CategoryTheory.Enriched.FunctorCategory.functorHomEquiv
- CategoryTheory.eHomFunctor
- CategoryTheory.CatEnrichedOrdinary.homEquiv_comp
- CategoryTheory.eHomWhiskerRight_id
- CategoryTheory.ForgetEnrichment.equivInverse
- CategoryTheory.eHomEquiv_comp
- CategoryTheory.ForgetEnrichment.equivFunctor
- CategoryTheory.Enriched.FunctorCategory.enrichedId_π
- CategoryTheory.ForgetEnrichment.equiv
- CategoryTheory.eHomEquiv_id
- CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom
- CategoryTheory.EnrichedOrdinaryCategory.homEquiv
- CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom
- CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom'
- CategoryTheory.Iso.eHomCongr_hom
- CategoryTheory.eComp_eHomWhiskerLeft
- CategoryTheory.CatEnrichedOrdinary.homEquiv_id
- CategoryTheory.eHomWhiskerRight_comp
- CategoryTheory.Iso.eHomCongr_comp
- CategoryTheory.eHom_whisker_cancel
- CategoryTheory.Enriched.FunctorCategory.enriched_assoc
- CategoryTheory.Enriched.FunctorCategory.homEquiv_comp
- CategoryTheory.Enriched.FunctorCategory.enriched_comp_id
- CategoryTheory.eHomWhiskerLeft_comp
- CategoryTheory.Enriched.FunctorCategory.enriched_id_comp
- CategoryTheory.eHom_whisker_cancel_assoc
- CategoryTheory.eCoyoneda
- CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift