Core

📁 Source: Mathlib/CategoryTheory/Core.lean

Statistics

Metric	Count
Definitions Core, forgetFunctorToCore, functorToCore, functorToCoreCompLeftIso, functorToCoreCompRightIso, functorToCoreInclusionIso, inclusion, inclusionCompFunctorToCoreIso, isoMk, of, CoreHom, iso, core, core, coreComp, coreCompInclusionIso, coreId, core, coreCategory, coreFunctor, ofEquivFunctor	21
Theorems forgetFunctorToCore_map_app, forgetFunctorToCore_obj_map, forgetFunctorToCore_obj_obj, functorToCore_comp_left, functorToCore_comp_right, functorToCore_inclusion, functorToCore_map_iso_hom, functorToCore_map_iso_inv, functorToCore_obj_of, hom_ext, hom_ext_iff, inclusion_comp_functorToCore, inclusion_map, inclusion_obj, instFaithfulInclusion, isoMk_hom_iso, isoMk_inv_iso, ext, ext_iff, core_counitIso_hom_app_iso_hom, core_counitIso_hom_app_iso_inv, core_counitIso_inv_app_iso_hom, core_counitIso_inv_app_iso_inv, core_functor_map_iso_hom, core_functor_map_iso_inv, core_functor_obj_of, core_inverse_map_iso_hom, core_inverse_map_iso_inv, core_inverse_obj_of, core_unitIso_hom_app_iso_hom, core_unitIso_hom_app_iso_inv, core_unitIso_inv_app_iso_hom, core_unitIso_inv_app_iso_inv, coreCompInclusionIso_hom_app, coreCompInclusionIso_inv_app, coreComp_hom_app_iso_hom, coreComp_hom_app_iso_inv, coreComp_inv_app_iso_hom, coreComp_inv_app_iso_inv, coreId_hom_app_iso_hom, coreId_hom_app_iso_inv, coreId_inv_app_iso_hom, coreId_inv_app_iso_inv, core_comp_inclusion, core_map_iso_hom, core_map_iso_inv, core_obj_of, coreAssociator, coreComp, coreId, coreLeftUnitor, coreRightUnitor, coreWhiskerLeft, coreWhiskerRight, core_hom_app_iso_hom, core_hom_app_iso_inv, core_inv_app_iso_hom, core_inv_app_iso_inv, coreCategory_comp_iso, coreCategory_comp_iso_hom, coreCategory_comp_iso_inv, coreCategory_id_iso_hom, coreCategory_id_iso_inv, coreCategory_inv_iso_hom, coreCategory_inv_iso_inv, coreFunctor_map_app_iso_hom, coreFunctor_map_app_iso_inv, coreFunctor_obj_map_iso_hom, coreFunctor_obj_map_iso_inv, coreFunctor_obj_obj_of	70
Total	91

CategoryTheory

Definitions

Name	Category	Theorems
Core 📖	CompData	80 math math: Functor.coreComp_hom_app_iso_inv, Core.forgetFunctorToCore_map_app, Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso, Iso.core_inv_app_iso_hom, Core.isoMk_hom_iso, Equivalence.core_inverse_map_iso_hom, Functor.coreId_hom_app_iso_hom, Bicategory.Pith.leftUnitor_inv_iso_hom, Equivalence.core_unitIso_hom_app_iso_inv, coreCategory_id_iso_inv, Functor.coreComp_hom_app_iso_hom, Functor.core_obj_of, Core.forgetFunctorToCore_obj_obj, coreCategory_inv_iso_inv, Functor.coreId_inv_app_iso_inv, Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv, coreFunctor_obj_map_iso_inv, Core.functorToCore_comp_right, Functor.coreId_inv_app_iso_hom, Iso.coreId, Iso.coreLeftUnitor, coreCategory_comp_iso_inv, coreFunctor_obj_obj_of, Bicategory.Pith.rightUnitor_hom_iso, Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv, Iso.coreAssociator, Bicategory.Pith.rightUnitor_inv_iso_inv, Functor.coreCompInclusionIso_hom_app, Bicategory.Pith.associator_hom_iso, coreCategory_inv_iso_hom, coreCategory_comp_iso, Functor.core_comp_inclusion, Core.functorToCore_map_iso_hom, coreCategory_id_iso_hom, Functor.coreCompInclusionIso_inv_app, Equivalence.core_functor_obj_of, Equivalence.core_functor_map_iso_inv, Iso.core_hom_app_iso_inv, Equivalence.core_counitIso_hom_app_iso_hom, Equivalence.core_inverse_map_iso_inv, Functor.coreId_hom_app_iso_inv, coreFunctor_map_app_iso_inv, Equivalence.core_inverse_obj_of, Bicategory.Pith.associator_inv_iso_inv, Iso.coreRightUnitor, Core.isoMk_inv_iso, Equivalence.core_counitIso_hom_app_iso_inv, coreFunctor_map_app_iso_hom, Equivalence.core_unitIso_hom_app_iso_hom, Iso.core_inv_app_iso_inv, Core.inclusion_obj, Bicategory.Pith.associator_inv_iso_hom, coreCategory_comp_iso_hom, Functor.core_map_iso_hom, Functor.core_map_iso_inv, Core.inclusion_comp_functorToCore, Bicategory.Pith.leftUnitor_hom_iso, Equivalence.core_counitIso_inv_app_iso_hom, Bicategory.Pith.rightUnitor_inv_iso_hom, Iso.coreComp, Core.forgetFunctorToCore_obj_map, Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom, Equivalence.core_functor_map_iso_hom, Iso.core_hom_app_iso_hom, Core.instFaithfulInclusion, Core.functorToCore_inclusion, Iso.coreWhiskerRight, Equivalence.core_unitIso_inv_app_iso_hom, Core.inclusion_map, Functor.coreComp_inv_app_iso_hom, Equivalence.core_unitIso_inv_app_iso_inv, Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom, coreFunctor_obj_map_iso_hom, Functor.coreComp_inv_app_iso_inv, Core.functorToCore_comp_left, Equivalence.core_counitIso_inv_app_iso_inv, Core.functorToCore_obj_of, Iso.coreWhiskerLeft, Core.functorToCore_map_iso_inv, Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso
CoreHom 📖	CompData	—
coreCategory 📖	CompOp	80 math math: Functor.coreComp_hom_app_iso_inv, Core.forgetFunctorToCore_map_app, Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso, Iso.core_inv_app_iso_hom, Core.isoMk_hom_iso, Equivalence.core_inverse_map_iso_hom, Functor.coreId_hom_app_iso_hom, Bicategory.Pith.leftUnitor_inv_iso_hom, Equivalence.core_unitIso_hom_app_iso_inv, coreCategory_id_iso_inv, Functor.coreComp_hom_app_iso_hom, Functor.core_obj_of, Core.forgetFunctorToCore_obj_obj, coreCategory_inv_iso_inv, Functor.coreId_inv_app_iso_inv, Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv, coreFunctor_obj_map_iso_inv, Core.functorToCore_comp_right, Functor.coreId_inv_app_iso_hom, Iso.coreId, Iso.coreLeftUnitor, coreCategory_comp_iso_inv, coreFunctor_obj_obj_of, Bicategory.Pith.rightUnitor_hom_iso, Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv, Iso.coreAssociator, Bicategory.Pith.rightUnitor_inv_iso_inv, Functor.coreCompInclusionIso_hom_app, Bicategory.Pith.associator_hom_iso, coreCategory_inv_iso_hom, coreCategory_comp_iso, Functor.core_comp_inclusion, Core.functorToCore_map_iso_hom, coreCategory_id_iso_hom, Functor.coreCompInclusionIso_inv_app, Equivalence.core_functor_obj_of, Equivalence.core_functor_map_iso_inv, Iso.core_hom_app_iso_inv, Equivalence.core_counitIso_hom_app_iso_hom, Equivalence.core_inverse_map_iso_inv, Functor.coreId_hom_app_iso_inv, coreFunctor_map_app_iso_inv, Equivalence.core_inverse_obj_of, Bicategory.Pith.associator_inv_iso_inv, Iso.coreRightUnitor, Core.isoMk_inv_iso, Equivalence.core_counitIso_hom_app_iso_inv, coreFunctor_map_app_iso_hom, Equivalence.core_unitIso_hom_app_iso_hom, Iso.core_inv_app_iso_inv, Core.inclusion_obj, Bicategory.Pith.associator_inv_iso_hom, coreCategory_comp_iso_hom, Functor.core_map_iso_hom, Functor.core_map_iso_inv, Core.inclusion_comp_functorToCore, Bicategory.Pith.leftUnitor_hom_iso, Equivalence.core_counitIso_inv_app_iso_hom, Bicategory.Pith.rightUnitor_inv_iso_hom, Iso.coreComp, Core.forgetFunctorToCore_obj_map, Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom, Equivalence.core_functor_map_iso_hom, Iso.core_hom_app_iso_hom, Core.instFaithfulInclusion, Core.functorToCore_inclusion, Iso.coreWhiskerRight, Equivalence.core_unitIso_inv_app_iso_hom, Core.inclusion_map, Functor.coreComp_inv_app_iso_hom, Equivalence.core_unitIso_inv_app_iso_inv, Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom, coreFunctor_obj_map_iso_hom, Functor.coreComp_inv_app_iso_inv, Core.functorToCore_comp_left, Equivalence.core_counitIso_inv_app_iso_inv, Core.functorToCore_obj_of, Iso.coreWhiskerLeft, Core.functorToCore_map_iso_inv, Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso
coreFunctor 📖	CompOp	5 math math: coreFunctor_obj_map_iso_inv, coreFunctor_obj_obj_of, coreFunctor_map_app_iso_inv, coreFunctor_map_app_iso_hom, coreFunctor_obj_map_iso_hom
ofEquivFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreCategory_comp_iso 📖	mathematical	—	CoreHom.iso CategoryStruct.comp Core Category.toCategoryStruct Groupoid.toCategory coreCategory Iso.trans Core.of	—	—
coreCategory_comp_iso_hom 📖	mathematical	—	Iso.hom Core.of CoreHom.iso CategoryStruct.comp Core Category.toCategoryStruct Groupoid.toCategory coreCategory	—	—
coreCategory_comp_iso_inv 📖	mathematical	—	Iso.inv Core.of CoreHom.iso CategoryStruct.comp Core Category.toCategoryStruct Groupoid.toCategory coreCategory	—	—
coreCategory_id_iso_hom 📖	mathematical	—	Iso.hom Core.of CoreHom.iso CategoryStruct.id Core Category.toCategoryStruct Groupoid.toCategory coreCategory	—	—
coreCategory_id_iso_inv 📖	mathematical	—	Iso.inv Core.of CoreHom.iso CategoryStruct.id Core Category.toCategoryStruct Groupoid.toCategory coreCategory	—	—
coreCategory_inv_iso_hom 📖	mathematical	—	Iso.hom Core.of CoreHom.iso Groupoid.inv Core coreCategory Iso.inv	—	—
coreCategory_inv_iso_inv 📖	mathematical	—	Iso.inv Core.of CoreHom.iso Groupoid.inv Core coreCategory Iso.hom	—	—
coreFunctor_map_app_iso_hom 📖	mathematical	—	Iso.hom Functor.obj Core.of Functor CoreHom.iso Core Groupoid.toCategory coreCategory Functor.core NatTrans.app Functor.map Functor.category coreFunctor	—	—
coreFunctor_map_app_iso_inv 📖	mathematical	—	Iso.inv Functor.obj Core.of Functor CoreHom.iso Core Groupoid.toCategory coreCategory Functor.core NatTrans.app Functor.map Functor.category coreFunctor	—	—
coreFunctor_obj_map_iso_hom 📖	mathematical	—	Iso.hom Core.of Functor.obj Core Groupoid.toCategory coreCategory Functor.comp Core.inclusion Functor CoreHom.iso Functor.map Functor.category coreFunctor	—	—
coreFunctor_obj_map_iso_inv 📖	mathematical	—	Iso.inv Core.of Functor.obj Core Groupoid.toCategory coreCategory Functor.comp Core.inclusion Functor CoreHom.iso Functor.map Functor.category coreFunctor	—	—
coreFunctor_obj_obj_of 📖	mathematical	—	Core.of Functor.obj Core Groupoid.toCategory coreCategory Functor Functor.category coreFunctor	—	—

CategoryTheory.Core

Definitions

Name	Category	Theorems
forgetFunctorToCore 📖	CompOp	3 math math: forgetFunctorToCore_map_app, forgetFunctorToCore_obj_obj, forgetFunctorToCore_obj_map
functorToCore 📖	CompOp	7 math math: functorToCore_comp_right, functorToCore_map_iso_hom, inclusion_comp_functorToCore, functorToCore_inclusion, functorToCore_comp_left, functorToCore_obj_of, functorToCore_map_iso_inv
functorToCoreCompLeftIso 📖	CompOp	—
functorToCoreCompRightIso 📖	CompOp	—
functorToCoreInclusionIso 📖	CompOp	—
inclusion 📖	CompOp	17 math math: forgetFunctorToCore_map_app, CategoryTheory.Equivalence.core_inverse_map_iso_hom, CategoryTheory.coreFunctor_obj_map_iso_inv, CategoryTheory.Functor.coreCompInclusionIso_hom_app, CategoryTheory.Functor.core_comp_inclusion, CategoryTheory.Functor.coreCompInclusionIso_inv_app, CategoryTheory.Equivalence.core_functor_map_iso_inv, CategoryTheory.Equivalence.core_inverse_map_iso_inv, inclusion_obj, CategoryTheory.Functor.core_map_iso_hom, CategoryTheory.Functor.core_map_iso_inv, inclusion_comp_functorToCore, CategoryTheory.Equivalence.core_functor_map_iso_hom, instFaithfulInclusion, functorToCore_inclusion, inclusion_map, CategoryTheory.coreFunctor_obj_map_iso_hom
inclusionCompFunctorToCoreIso 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_hom_iso, isoMk_inv_iso
of 📖	CompOp	85 math math: CategoryTheory.Functor.coreComp_hom_app_iso_inv, forgetFunctorToCore_map_app, CategoryTheory.Bicategory.Pith.inclusion_mapComp, CategoryTheory.Iso.core_inv_app_iso_hom, CategoryTheory.Bicategory.Pith.comp_of, CategoryTheory.Equivalence.core_inverse_map_iso_hom, CategoryTheory.Functor.coreId_hom_app_iso_hom, CategoryTheory.Bicategory.Pith.whiskerRight_iso_inv, CategoryTheory.Bicategory.Pith.leftUnitor_inv_iso_hom, CategoryTheory.Equivalence.core_unitIso_hom_app_iso_inv, CategoryTheory.Bicategory.Pith.comp₂_iso_hom_assoc, CategoryTheory.coreCategory_id_iso_inv, CategoryTheory.Functor.coreComp_hom_app_iso_hom, CategoryTheory.Functor.core_obj_of, forgetFunctorToCore_obj_obj, CategoryTheory.coreCategory_inv_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of, CategoryTheory.Functor.coreId_inv_app_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv, CategoryTheory.coreFunctor_obj_map_iso_inv, CategoryTheory.Bicategory.Pith.id₂_iso_inv, CategoryTheory.Functor.coreId_inv_app_iso_hom, CategoryTheory.coreCategory_comp_iso_inv, CategoryTheory.coreFunctor_obj_obj_of, CategoryTheory.Bicategory.Pith.rightUnitor_hom_iso, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv, CategoryTheory.Bicategory.Pith.whiskerRight_iso_hom, CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_inv, CategoryTheory.Functor.coreCompInclusionIso_hom_app, CategoryTheory.Bicategory.Pith.associator_hom_iso, CategoryTheory.Bicategory.Pith.whiskerLeft_iso_hom, CategoryTheory.coreCategory_inv_iso_hom, CategoryTheory.coreCategory_comp_iso, CategoryTheory.Bicategory.Pith.id₂_iso_hom, functorToCore_map_iso_hom, CategoryTheory.coreCategory_id_iso_hom, CategoryTheory.Functor.coreCompInclusionIso_inv_app, CategoryTheory.Equivalence.core_functor_obj_of, CategoryTheory.Bicategory.Pith.id_of, CategoryTheory.Equivalence.core_functor_map_iso_inv, CategoryTheory.Iso.core_hom_app_iso_inv, CategoryTheory.Equivalence.core_counitIso_hom_app_iso_hom, CategoryTheory.Equivalence.core_inverse_map_iso_inv, CategoryTheory.Bicategory.Pith.hom₂_ext_iff, CategoryTheory.Functor.coreId_hom_app_iso_inv, CategoryTheory.coreFunctor_map_app_iso_inv, CategoryTheory.Bicategory.Pith.whiskerLeft_iso_inv, CategoryTheory.Equivalence.core_inverse_obj_of, CategoryTheory.Bicategory.Pith.associator_inv_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, isoMk_inv_iso, CategoryTheory.Equivalence.core_counitIso_hom_app_iso_inv, CategoryTheory.Bicategory.Pith.inclusion_mapId, CategoryTheory.coreFunctor_map_app_iso_hom, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, CategoryTheory.Bicategory.Pith.comp₂_iso_hom, CategoryTheory.Equivalence.core_unitIso_hom_app_iso_hom, CategoryTheory.Iso.core_inv_app_iso_inv, inclusion_obj, CategoryTheory.Bicategory.Pith.associator_inv_iso_hom, CategoryTheory.coreCategory_comp_iso_hom, CategoryTheory.Functor.core_map_iso_hom, CategoryTheory.Functor.core_map_iso_inv, CategoryTheory.Bicategory.Pith.leftUnitor_hom_iso, CategoryTheory.Equivalence.core_counitIso_inv_app_iso_hom, CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_hom, CategoryTheory.Bicategory.Pith.comp₂_iso_inv_assoc, hom_ext_iff, forgetFunctorToCore_obj_map, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom, CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map, CategoryTheory.Equivalence.core_functor_map_iso_hom, CategoryTheory.Iso.core_hom_app_iso_hom, CategoryTheory.Bicategory.Pith.comp₂_iso_inv, CategoryTheory.Equivalence.core_unitIso_inv_app_iso_hom, CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, inclusion_map, CategoryTheory.Functor.coreComp_inv_app_iso_hom, CategoryTheory.Equivalence.core_unitIso_inv_app_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom, CategoryTheory.coreFunctor_obj_map_iso_hom, CategoryTheory.Functor.coreComp_inv_app_iso_inv, CategoryTheory.Equivalence.core_counitIso_inv_app_iso_inv, functorToCore_obj_of, functorToCore_map_iso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forgetFunctorToCore_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Groupoid.toCategory CategoryTheory.Functor.comp CategoryTheory.Core CategoryTheory.coreCategory inclusion CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category forgetFunctorToCore CategoryTheory.Iso.hom of CategoryTheory.Functor.obj CategoryTheory.CoreHom.iso	—	—
forgetFunctorToCore_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Groupoid.toCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Core CategoryTheory.coreCategory CategoryTheory.Functor.category forgetFunctorToCore CategoryTheory.Iso.hom of CategoryTheory.CoreHom.iso	—	—
forgetFunctorToCore_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.Functor CategoryTheory.Core CategoryTheory.coreCategory CategoryTheory.Functor.category forgetFunctorToCore of	—	—
functorToCore_comp_left 📖	mathematical	—	functorToCore CategoryTheory.Functor.comp CategoryTheory.Groupoid.toCategory CategoryTheory.Core CategoryTheory.coreCategory	—	CategoryTheory.Functor.ext_of_iso
functorToCore_comp_right 📖	mathematical	—	functorToCore CategoryTheory.Functor.comp CategoryTheory.Groupoid.toCategory CategoryTheory.Core CategoryTheory.coreCategory CategoryTheory.Functor.core	—	CategoryTheory.Functor.ext_of_iso
functorToCore_inclusion 📖	mathematical	—	functorToCore CategoryTheory.Core CategoryTheory.coreCategory inclusion CategoryTheory.Functor.id CategoryTheory.Groupoid.toCategory	—	CategoryTheory.Functor.ext_of_iso
functorToCore_map_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom of CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.CoreHom.iso CategoryTheory.Functor.map CategoryTheory.Core CategoryTheory.coreCategory functorToCore	—	—
functorToCore_map_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv of CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.CoreHom.iso CategoryTheory.Functor.map CategoryTheory.Core CategoryTheory.coreCategory functorToCore CategoryTheory.inv CategoryTheory.Functor.map_isIso CategoryTheory.IsIso.of_groupoid	—	CategoryTheory.IsIso.of_groupoid CategoryTheory.Functor.map_isIso CategoryTheory.Groupoid.inv_eq_inv CategoryTheory.Functor.map_inv
functorToCore_obj_of 📖	mathematical	—	of CategoryTheory.Functor.obj CategoryTheory.Groupoid.toCategory CategoryTheory.Core CategoryTheory.coreCategory functorToCore	—	—
hom_ext 📖	—	CategoryTheory.Iso.hom of CategoryTheory.CoreHom.iso	—	—	CategoryTheory.CoreHom.ext CategoryTheory.Iso.ext
hom_ext_iff 📖	mathematical	—	CategoryTheory.Iso.hom of CategoryTheory.CoreHom.iso	—	hom_ext
inclusion_comp_functorToCore 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory inclusion functorToCore CategoryTheory.Functor.id	—	CategoryTheory.Functor.ext_of_iso
inclusion_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory inclusion CategoryTheory.Iso.hom of CategoryTheory.CoreHom.iso	—	—
inclusion_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory inclusion of	—	—
instFaithfulInclusion 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory inclusion	—	hom_ext
isoMk_hom_iso 📖	mathematical	—	CategoryTheory.CoreHom.iso CategoryTheory.Iso.hom CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory isoMk	—	—
isoMk_inv_iso 📖	mathematical	—	CategoryTheory.CoreHom.iso CategoryTheory.Iso.inv CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory isoMk CategoryTheory.Iso.symm of	—	—

CategoryTheory.CoreHom

Definitions

Name	Category	Theorems
iso 📖	CompOp	74 math math: CategoryTheory.Functor.coreComp_hom_app_iso_inv, CategoryTheory.Core.forgetFunctorToCore_map_app, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso, CategoryTheory.Iso.core_inv_app_iso_hom, CategoryTheory.Core.isoMk_hom_iso, CategoryTheory.Equivalence.core_inverse_map_iso_hom, CategoryTheory.Functor.coreId_hom_app_iso_hom, CategoryTheory.Bicategory.Pith.whiskerRight_iso_inv, CategoryTheory.Bicategory.Pith.leftUnitor_inv_iso_hom, CategoryTheory.Equivalence.core_unitIso_hom_app_iso_inv, CategoryTheory.Bicategory.Pith.comp₂_iso_hom_assoc, CategoryTheory.coreCategory_id_iso_inv, CategoryTheory.Functor.coreComp_hom_app_iso_hom, CategoryTheory.coreCategory_inv_iso_inv, CategoryTheory.Functor.coreId_inv_app_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv, CategoryTheory.coreFunctor_obj_map_iso_inv, CategoryTheory.Bicategory.Pith.id₂_iso_inv, CategoryTheory.Functor.coreId_inv_app_iso_hom, CategoryTheory.coreCategory_comp_iso_inv, CategoryTheory.Bicategory.Pith.rightUnitor_hom_iso, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv, ext_iff, CategoryTheory.Bicategory.Pith.whiskerRight_iso_hom, CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_inv, CategoryTheory.Bicategory.Pith.associator_hom_iso, CategoryTheory.Bicategory.Pith.whiskerLeft_iso_hom, CategoryTheory.coreCategory_inv_iso_hom, CategoryTheory.coreCategory_comp_iso, CategoryTheory.Bicategory.Pith.id₂_iso_hom, CategoryTheory.Core.functorToCore_map_iso_hom, CategoryTheory.coreCategory_id_iso_hom, CategoryTheory.Equivalence.core_functor_map_iso_inv, CategoryTheory.Iso.core_hom_app_iso_inv, CategoryTheory.Equivalence.core_counitIso_hom_app_iso_hom, CategoryTheory.Equivalence.core_inverse_map_iso_inv, CategoryTheory.Bicategory.Pith.hom₂_ext_iff, CategoryTheory.Functor.coreId_hom_app_iso_inv, CategoryTheory.coreFunctor_map_app_iso_inv, CategoryTheory.Bicategory.Pith.whiskerLeft_iso_inv, CategoryTheory.Bicategory.Pith.associator_inv_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom, CategoryTheory.Core.isoMk_inv_iso, CategoryTheory.Equivalence.core_counitIso_hom_app_iso_inv, CategoryTheory.coreFunctor_map_app_iso_hom, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv, CategoryTheory.Bicategory.Pith.comp₂_iso_hom, CategoryTheory.Equivalence.core_unitIso_hom_app_iso_hom, CategoryTheory.Iso.core_inv_app_iso_inv, CategoryTheory.Bicategory.Pith.associator_inv_iso_hom, CategoryTheory.coreCategory_comp_iso_hom, CategoryTheory.Functor.core_map_iso_hom, CategoryTheory.Functor.core_map_iso_inv, CategoryTheory.Bicategory.Pith.leftUnitor_hom_iso, CategoryTheory.Equivalence.core_counitIso_inv_app_iso_hom, CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_hom, CategoryTheory.Bicategory.Pith.comp₂_iso_inv_assoc, CategoryTheory.Core.hom_ext_iff, CategoryTheory.Core.forgetFunctorToCore_obj_map, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom, CategoryTheory.Equivalence.core_functor_map_iso_hom, CategoryTheory.Iso.core_hom_app_iso_hom, CategoryTheory.Bicategory.Pith.comp₂_iso_inv, CategoryTheory.Equivalence.core_unitIso_inv_app_iso_hom, CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂, CategoryTheory.Core.inclusion_map, CategoryTheory.Functor.coreComp_inv_app_iso_hom, CategoryTheory.Equivalence.core_unitIso_inv_app_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom, CategoryTheory.coreFunctor_obj_map_iso_hom, CategoryTheory.Functor.coreComp_inv_app_iso_inv, CategoryTheory.Equivalence.core_counitIso_inv_app_iso_inv, CategoryTheory.Core.functorToCore_map_iso_inv, CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	iso	—	—	—
ext_iff 📖	mathematical	—	iso	—	ext

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
core 📖	CompOp	14 math math: core_inverse_map_iso_hom, core_unitIso_hom_app_iso_inv, core_functor_obj_of, core_functor_map_iso_inv, core_counitIso_hom_app_iso_hom, core_inverse_map_iso_inv, core_inverse_obj_of, core_counitIso_hom_app_iso_inv, core_unitIso_hom_app_iso_hom, core_counitIso_inv_app_iso_hom, core_functor_map_iso_hom, core_unitIso_inv_app_iso_hom, core_unitIso_inv_app_iso_inv, core_counitIso_inv_app_iso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
core_counitIso_hom_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Functor.comp inverse functor CategoryTheory.Core.of CategoryTheory.Functor.id CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category counitIso core	—	—
core_counitIso_hom_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Functor.comp inverse functor CategoryTheory.Core.of CategoryTheory.Functor.id CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso core	—	—
core_counitIso_inv_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso core	—	—
core_counitIso_inv_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse functor CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category counitIso core CategoryTheory.Iso.hom	—	—
core_functor_map_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.comp CategoryTheory.Core.inclusion functor CategoryTheory.CoreHom.iso CategoryTheory.Functor.map core	—	—
core_functor_map_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.comp CategoryTheory.Core.inclusion functor CategoryTheory.CoreHom.iso CategoryTheory.Functor.map core	—	—
core_functor_obj_of 📖	mathematical	—	CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory functor core	—	—
core_inverse_map_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.comp CategoryTheory.Core.inclusion inverse CategoryTheory.CoreHom.iso CategoryTheory.Functor.map core	—	—
core_inverse_map_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.comp CategoryTheory.Core.inclusion inverse CategoryTheory.CoreHom.iso CategoryTheory.Functor.map core	—	—
core_inverse_obj_of 📖	mathematical	—	CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory inverse core	—	—
core_unitIso_hom_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Core.of CategoryTheory.Functor.comp functor inverse CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category unitIso core	—	—
core_unitIso_hom_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Core.of CategoryTheory.Functor.comp functor inverse CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso core	—	—
core_unitIso_inv_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.id CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso core	—	—
core_unitIso_inv_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.Functor.comp functor inverse CategoryTheory.Functor.id CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category unitIso core CategoryTheory.Iso.hom	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
core 📖	CompOp	36 math math: coreComp_hom_app_iso_inv, CategoryTheory.Iso.core_inv_app_iso_hom, coreId_hom_app_iso_hom, CategoryTheory.Equivalence.core_unitIso_hom_app_iso_inv, coreComp_hom_app_iso_hom, core_obj_of, coreId_inv_app_iso_inv, CategoryTheory.Core.functorToCore_comp_right, coreId_inv_app_iso_hom, CategoryTheory.Iso.coreId, CategoryTheory.Iso.coreLeftUnitor, CategoryTheory.Iso.coreAssociator, coreCompInclusionIso_hom_app, core_comp_inclusion, coreCompInclusionIso_inv_app, CategoryTheory.Iso.core_hom_app_iso_inv, CategoryTheory.Equivalence.core_counitIso_hom_app_iso_hom, coreId_hom_app_iso_inv, CategoryTheory.coreFunctor_map_app_iso_inv, CategoryTheory.Iso.coreRightUnitor, CategoryTheory.Equivalence.core_counitIso_hom_app_iso_inv, CategoryTheory.coreFunctor_map_app_iso_hom, CategoryTheory.Equivalence.core_unitIso_hom_app_iso_hom, CategoryTheory.Iso.core_inv_app_iso_inv, core_map_iso_hom, core_map_iso_inv, CategoryTheory.Equivalence.core_counitIso_inv_app_iso_hom, CategoryTheory.Iso.coreComp, CategoryTheory.Iso.core_hom_app_iso_hom, CategoryTheory.Iso.coreWhiskerRight, CategoryTheory.Equivalence.core_unitIso_inv_app_iso_hom, coreComp_inv_app_iso_hom, CategoryTheory.Equivalence.core_unitIso_inv_app_iso_inv, coreComp_inv_app_iso_inv, CategoryTheory.Equivalence.core_counitIso_inv_app_iso_inv, CategoryTheory.Iso.coreWhiskerLeft
coreComp 📖	CompOp	9 math math: coreComp_hom_app_iso_inv, coreComp_hom_app_iso_hom, CategoryTheory.Iso.coreLeftUnitor, CategoryTheory.Iso.coreAssociator, CategoryTheory.Iso.coreRightUnitor, CategoryTheory.Iso.coreWhiskerRight, coreComp_inv_app_iso_hom, coreComp_inv_app_iso_inv, CategoryTheory.Iso.coreWhiskerLeft
coreCompInclusionIso 📖	CompOp	2 math math: coreCompInclusionIso_hom_app, coreCompInclusionIso_inv_app
coreId 📖	CompOp	6 math math: coreId_hom_app_iso_hom, coreId_inv_app_iso_inv, coreId_inv_app_iso_hom, CategoryTheory.Iso.coreLeftUnitor, coreId_hom_app_iso_inv, CategoryTheory.Iso.coreRightUnitor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreCompInclusionIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory comp core CategoryTheory.Core.inclusion CategoryTheory.Iso.hom CategoryTheory.Functor category coreCompInclusionIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Core.of	—	—
coreCompInclusionIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory comp core CategoryTheory.Core.inclusion CategoryTheory.Iso.inv CategoryTheory.Functor category coreCompInclusionIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Core.of	—	—
coreComp_hom_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core comp CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor category coreComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreComp_hom_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core comp CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category coreComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreComp_inv_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core comp CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category coreComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreComp_inv_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core comp CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor category coreComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreId_hom_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core id CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor category coreId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreId_hom_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core id CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category coreId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreId_inv_app_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core id CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category coreId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coreId_inv_app_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core id CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor category coreId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
core_comp_inclusion 📖	mathematical	—	comp CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core CategoryTheory.Core.inclusion	—	ext_of_iso
core_map_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory comp CategoryTheory.Core.inclusion CategoryTheory.CoreHom.iso map core	—	—
core_map_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory comp CategoryTheory.Core.inclusion CategoryTheory.CoreHom.iso map core	—	—
core_obj_of 📖	mathematical	—	CategoryTheory.Core.of obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory core	—	—

CategoryTheory.Iso

Definitions

Name	Category	Theorems
core 📖	CompOp	11 math math: core_inv_app_iso_hom, coreId, coreLeftUnitor, coreAssociator, core_hom_app_iso_inv, coreRightUnitor, core_inv_app_iso_inv, coreComp, core_hom_app_iso_hom, coreWhiskerRight, coreWhiskerLeft

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coreAssociator 📖	mathematical	—	core CategoryTheory.Functor.comp CategoryTheory.Functor.associator trans CategoryTheory.Functor CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.category CategoryTheory.Functor.core CategoryTheory.Functor.coreComp CategoryTheory.Functor.isoWhiskerRight symm CategoryTheory.Functor.isoWhiskerLeft	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.Core.hom_ext CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
coreComp 📖	mathematical	—	core trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core	—	—
coreId 📖	mathematical	—	core refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core	—	—
coreLeftUnitor 📖	mathematical	—	core CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.leftUnitor trans CategoryTheory.Functor CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.category CategoryTheory.Functor.core CategoryTheory.Functor.coreComp CategoryTheory.Functor.isoWhiskerRight CategoryTheory.Functor.coreId	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.Core.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id
coreRightUnitor 📖	mathematical	—	core CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.Functor.rightUnitor trans CategoryTheory.Functor CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.category CategoryTheory.Functor.core CategoryTheory.Functor.coreComp CategoryTheory.Functor.isoWhiskerLeft CategoryTheory.Functor.coreId	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.Core.hom_ext CategoryTheory.Category.comp_id
coreWhiskerLeft 📖	mathematical	—	core CategoryTheory.Functor.comp CategoryTheory.Functor.isoWhiskerLeft trans CategoryTheory.Functor CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.category CategoryTheory.Functor.core CategoryTheory.Functor.coreComp symm	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.Core.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
coreWhiskerRight 📖	mathematical	—	core CategoryTheory.Functor.comp CategoryTheory.Functor.isoWhiskerRight trans CategoryTheory.Functor CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.category CategoryTheory.Functor.core CategoryTheory.Functor.coreComp symm	—	ext CategoryTheory.NatTrans.ext' CategoryTheory.Core.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
core_hom_app_iso_hom 📖	mathematical	—	hom CategoryTheory.Functor.obj CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category core	—	—
core_hom_app_iso_inv 📖	mathematical	—	inv CategoryTheory.Functor.obj CategoryTheory.Core.of CategoryTheory.CoreHom.iso CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.NatTrans.app hom CategoryTheory.Functor CategoryTheory.Functor.category core	—	—
core_inv_app_iso_hom 📖	mathematical	—	hom CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app inv CategoryTheory.Functor CategoryTheory.Functor.category core	—	—
core_inv_app_iso_inv 📖	mathematical	—	inv CategoryTheory.Core.of CategoryTheory.Functor.obj CategoryTheory.Core CategoryTheory.Groupoid.toCategory CategoryTheory.coreCategory CategoryTheory.Functor.core CategoryTheory.CoreHom.iso CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category core hom	—	—

---

← Back to Index