EnrichedCat

📁 Source: Mathlib/CategoryTheory/Enriched/EnrichedCat.lean

Statistics

Metric	Count
Definitions EnrichedCat, associator, bicategory, instCoeSortType, leftUnitor, of, rightUnitor, str, whiskerLeft, whiskerRight	10
Theorems associator_hom_out_app, associator_inv_out_app, comp_whiskerRight, leftUnitor_hom_out_app, leftUnitor_inv_out_app, rightUnitor_hom_out_app, rightUnitor_inv_out_app, whiskerLeft_out_app, whiskerRight_out_app, whisker_exchange	10
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
EnrichedCat 📖	CompOp	—

CategoryTheory.EnrichedCat

Definitions

Name	Category	Theorems
associator 📖	CompOp	2 math math: associator_inv_out_app, associator_hom_out_app
bicategory 📖	CompOp	—
instCoeSortType 📖	CompOp	—
leftUnitor 📖	CompOp	2 math math: leftUnitor_hom_out_app, leftUnitor_inv_out_app
of 📖	CompOp	—
rightUnitor 📖	CompOp	2 math math: rightUnitor_hom_out_app, rightUnitor_inv_out_app
str 📖	CompOp	—
whiskerLeft 📖	CompOp	2 math math: whisker_exchange, whiskerLeft_out_app
whiskerRight 📖	CompOp	3 math math: comp_whiskerRight, whisker_exchange, whiskerRight_out_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.hom CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category associator CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.ForgetEnrichment.homTo_id CategoryTheory.EnrichedFunctor.map_id CategoryTheory.ForgetEnrichment.homOf_eId CategoryTheory.Category.comp_id
associator_inv_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.inv CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category associator CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.Category.comp_id CategoryTheory.ForgetEnrichment.homTo_id CategoryTheory.EnrichedFunctor.map_id CategoryTheory.ForgetEnrichment.homOf_eId
comp_whiskerRight 📖	mathematical	—	whiskerRight CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedNatTrans.out CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category CategoryTheory.EnrichedFunctor.comp	—	CategoryTheory.EnrichedFunctor.hom_ext whiskerRight_out_app CategoryTheory.Category.assoc CategoryTheory.EnrichedFunctor.map_comp CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc
leftUnitor_hom_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedFunctor.id CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.hom CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category leftUnitor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.ForgetEnrichment.homTo_id CategoryTheory.EnrichedFunctor.map_id CategoryTheory.ForgetEnrichment.homOf_eId CategoryTheory.Category.comp_id
leftUnitor_inv_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedFunctor.id CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.inv CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category leftUnitor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.ForgetEnrichment.homTo_id CategoryTheory.EnrichedFunctor.map_id CategoryTheory.ForgetEnrichment.homOf_eId CategoryTheory.Category.comp_id
rightUnitor_hom_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedFunctor.id CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.hom CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category rightUnitor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.Category.comp_id
rightUnitor_inv_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedFunctor.id CategoryTheory.EnrichedNatTrans.out CategoryTheory.Iso.inv CategoryTheory.EnrichedFunctor CategoryTheory.EnrichedFunctor.category rightUnitor CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.Category.comp_id
whiskerLeft_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedNatTrans.out whiskerLeft CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
whiskerRight_out_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ForgetEnrichment CategoryTheory.categoryForgetEnrichment CategoryTheory.EnrichedFunctor.forget CategoryTheory.EnrichedFunctor.comp CategoryTheory.EnrichedNatTrans.out whiskerRight CategoryTheory.ForgetEnrichment.homOf CategoryTheory.EnrichedFunctor.obj CategoryTheory.ForgetEnrichment.to CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.EnrichedCategory.Hom CategoryTheory.ForgetEnrichment.homTo CategoryTheory.ForgetEnrichment.of CategoryTheory.EnrichedFunctor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
whisker_exchange 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.EnrichedFunctor CategoryTheory.Category.toCategoryStruct CategoryTheory.EnrichedFunctor.category CategoryTheory.EnrichedFunctor.comp whiskerLeft whiskerRight	—	CategoryTheory.EnrichedFunctor.hom_ext whiskerLeft_out_app whiskerRight_out_app CategoryTheory.NatTrans.naturality

---

← Back to Index