Documentation Verification Report

CatEnriched

📁 Source: Mathlib/CategoryTheory/Bicategory/CatEnriched.lean

Statistics

Metric	Count
Definitions `CatEnriched`, `hComp`, `instBicategory`, `instCategory`, `instCategoryHom`, `instCategoryStruct`, `instEnrichedCategoryCat`, `instEnrichedOrdinaryCategoryCat`, `CatEnrichedOrdinary`, `base`, `base'`, `mk`, `hComp`, `homEquiv`, `instBicategory`, `instCategory`, `instCategoryHom`, `instCategoryStructHom`, `instEnrichedCategoryCat`, `instEnrichedOrdinaryCategoryCat`, `instQuiverHom`, `toBase`	22
Theorems `comp_eq`, `eqToHom_hComp_eqToHom`, `hComp_assoc`, `hComp_assoc_heq`, `hComp_comp`, `hComp_id`, `hComp_id_heq`, `id_eq`, `id_hComp`, `id_hComp_heq`, `id_hComp_id`, `instStrict`, `base_comp`, `base_eqToHom`, `base_id`, `comp_eq`, `ext`, `ext_iff`, `id_eq`, `mk_comp`, `base_mk`, `eqToHom_hComp_eqToHom`, `hComp_assoc`, `hComp_assoc_heq`, `hComp_comp`, `hComp_id`, `hComp_id_heq`, `homEquiv_comp`, `homEquiv_id`, `id_eq_eqToHom`, `id_hComp`, `id_hComp_heq`, `id_hComp_id`, `instStrict`, `mk_base`	35
Total	57

CategoryTheory

Definitions

Name	Category	Theorems
`CatEnriched` 📖	CompOp	20 math math: `CatEnriched.id_hComp`, `CatEnriched.id_hComp_id`, `CatEnriched.id_hComp_heq`, `CatEnriched.hComp_id_heq`, `CatEnrichedOrdinary.Hom.mk_comp`, `CatEnriched.hComp_assoc`, `CatEnrichedOrdinary.Hom.id_eq`, `CatEnrichedOrdinary.Hom.base_comp`, `CatEnriched.hComp_assoc_heq`, `CatEnrichedOrdinary.Hom.comp_eq`, `CatEnriched.comp_eq`, `CatEnrichedOrdinary.homEquiv_comp`, `CatEnriched.id_eq`, `CatEnriched.eqToHom_hComp_eqToHom`, `CatEnriched.hComp_comp`, `CatEnrichedOrdinary.homEquiv_id`, `CatEnriched.hComp_id`, `CatEnrichedOrdinary.Hom.base_eqToHom`, `CatEnriched.instStrict`, `CatEnrichedOrdinary.Hom.base_id`
`CatEnrichedOrdinary` 📖	CompOp	18 math math: `CatEnrichedOrdinary.id_hComp_heq`, `CatEnrichedOrdinary.hComp_id`, `CatEnrichedOrdinary.hComp_comp`, `CatEnrichedOrdinary.Hom.mk_comp`, `CatEnrichedOrdinary.Hom.id_eq`, `CatEnrichedOrdinary.Hom.base_comp`, `CatEnrichedOrdinary.id_hComp`, `CatEnrichedOrdinary.Hom.comp_eq`, `CatEnrichedOrdinary.instStrict`, `CatEnrichedOrdinary.homEquiv_comp`, `CatEnrichedOrdinary.hComp_id_heq`, `CatEnrichedOrdinary.hComp_assoc`, `CatEnrichedOrdinary.id_hComp_id`, `CatEnrichedOrdinary.eqToHom_hComp_eqToHom`, `CatEnrichedOrdinary.hComp_assoc_heq`, `CatEnrichedOrdinary.homEquiv_id`, `CatEnrichedOrdinary.Hom.base_eqToHom`, `CatEnrichedOrdinary.Hom.base_id`

CategoryTheory.CatEnriched

Definitions

Name	Category	Theorems
`hComp` 📖	CompOp	9 math math: `id_hComp`, `id_hComp_id`, `id_hComp_heq`, `hComp_id_heq`, `hComp_assoc`, `hComp_assoc_heq`, `eqToHom_hComp_eqToHom`, `hComp_comp`, `hComp_id`
`instBicategory` 📖	CompOp	1 math math: `instStrict`
`instCategory` 📖	CompOp	3 math math: `id_hComp`, `hComp_assoc`, `hComp_id`
`instCategoryHom` 📖	CompOp	15 math math: `id_hComp`, `id_hComp_id`, `id_hComp_heq`, `hComp_id_heq`, `CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp`, `hComp_assoc`, `CategoryTheory.CatEnrichedOrdinary.Hom.id_eq`, `CategoryTheory.CatEnrichedOrdinary.Hom.base_comp`, `hComp_assoc_heq`, `CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq`, `eqToHom_hComp_eqToHom`, `hComp_comp`, `hComp_id`, `CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom`, `CategoryTheory.CatEnrichedOrdinary.Hom.base_id`
`instCategoryStruct` 📖	CompOp	19 math math: `id_hComp`, `id_hComp_id`, `id_hComp_heq`, `hComp_id_heq`, `CategoryTheory.CatEnrichedOrdinary.Hom.mk_comp`, `hComp_assoc`, `CategoryTheory.CatEnrichedOrdinary.Hom.id_eq`, `CategoryTheory.CatEnrichedOrdinary.Hom.base_comp`, `hComp_assoc_heq`, `CategoryTheory.CatEnrichedOrdinary.Hom.comp_eq`, `comp_eq`, `CategoryTheory.CatEnrichedOrdinary.homEquiv_comp`, `id_eq`, `eqToHom_hComp_eqToHom`, `hComp_comp`, `CategoryTheory.CatEnrichedOrdinary.homEquiv_id`, `hComp_id`, `CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom`, `CategoryTheory.CatEnrichedOrdinary.Hom.base_id`
`instEnrichedCategoryCat` 📖	CompOp	2 math math: `comp_eq`, `id_eq`
`instEnrichedOrdinaryCategoryCat` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.CatEnriched` `instCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.EnrichedCategory.Hom` `instEnrichedCategoryCat` `CategoryTheory.Cat.str` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.eComp`	—	—
`eqToHom_hComp_eqToHom` 📖	mathematical	—	`hComp` `CategoryTheory.eqToHom` `Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp`	—	`id_hComp_id`
`hComp_assoc` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CatEnriched` `instCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instCategoryHom` `CategoryTheory.eqToHom` `CategoryTheory.Category.assoc`	—	`CategoryTheory.Category.assoc`
`hComp_assoc_heq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp` `hComp`	—	`congr_arg_heq` `CategoryTheory.e_assoc`
`hComp_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `hComp`	—	`CategoryTheory.Functor.map_comp`
`hComp_id` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CatEnriched` `instCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp` `instCategory` `CategoryTheory.eqToHom` `CategoryTheory.Category.comp_id`	—	`CategoryTheory.Category.comp_id`
`hComp_id_heq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `hComp`	—	`id_eq` `CategoryTheory.Functor.map_id` `congr_arg_heq` `CategoryTheory.e_comp_id`
`id_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.CatEnriched` `instCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Bundled.α` `CategoryTheory.Category` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.Cat.str` `CategoryTheory.EnrichedCategory.Hom` `instEnrichedCategoryCat` `CategoryTheory.Cat.Hom.toFunctor` `CategoryTheory.eId` `CategoryTheory.ULiftHom` `CategoryTheory.Discrete`	—	—
`id_hComp` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CatEnriched` `instCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp` `instCategory` `CategoryTheory.eqToHom` `CategoryTheory.Category.id_comp`	—	`CategoryTheory.Category.id_comp`
`id_hComp_heq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `hComp`	—	`id_eq` `CategoryTheory.Functor.map_id` `congr_arg_heq` `CategoryTheory.e_id_comp`
`id_hComp_id` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStruct` `CategoryTheory.Category.toCategoryStruct` `instCategoryHom` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.Functor.map_id`
`instStrict` 📖	mathematical	—	`CategoryTheory.Bicategory.Strict` `CategoryTheory.CatEnriched` `instBicategory`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`

CategoryTheory.CatEnrichedOrdinary

Definitions

Name	Category	Theorems
`hComp` 📖	CompOp	9 math math: `id_hComp_heq`, `hComp_id`, `hComp_comp`, `id_hComp`, `hComp_id_heq`, `hComp_assoc`, `id_hComp_id`, `eqToHom_hComp_eqToHom`, `hComp_assoc_heq`
`homEquiv` 📖	CompOp	8 math math: `Hom.mk_comp`, `Hom.id_eq`, `Hom.base_comp`, `Hom.comp_eq`, `homEquiv_comp`, `homEquiv_id`, `Hom.base_eqToHom`, `Hom.base_id`
`instBicategory` 📖	CompOp	1 math math: `instStrict`
`instCategory` 📖	CompOp	17 math math: `id_hComp_heq`, `hComp_id`, `hComp_comp`, `Hom.mk_comp`, `Hom.id_eq`, `Hom.base_comp`, `id_hComp`, `Hom.comp_eq`, `homEquiv_comp`, `hComp_id_heq`, `hComp_assoc`, `id_hComp_id`, `eqToHom_hComp_eqToHom`, `hComp_assoc_heq`, `homEquiv_id`, `Hom.base_eqToHom`, `Hom.base_id`
`instCategoryHom` 📖	CompOp	—
`instCategoryStructHom` 📖	CompOp	14 math math: `id_hComp_heq`, `hComp_id`, `hComp_comp`, `Hom.mk_comp`, `Hom.id_eq`, `Hom.base_comp`, `id_hComp`, `Hom.comp_eq`, `hComp_id_heq`, `hComp_assoc`, `id_hComp_id`, `eqToHom_hComp_eqToHom`, `Hom.base_eqToHom`, `Hom.base_id`
`instEnrichedCategoryCat` 📖	CompOp	—
`instEnrichedOrdinaryCategoryCat` 📖	CompOp	—
`instQuiverHom` 📖	CompOp	3 math math: `id_hComp_heq`, `hComp_id_heq`, `hComp_assoc_heq`
`toBase` 📖	CompOp	8 math math: `Hom.mk_comp`, `Hom.id_eq`, `Hom.base_comp`, `Hom.comp_eq`, `homEquiv_comp`, `homEquiv_id`, `Hom.base_eqToHom`, `Hom.base_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_mk` 📖	mathematical	—	`Hom.base`	—	—
`eqToHom_hComp_eqToHom` 📖	mathematical	—	`hComp` `CategoryTheory.eqToHom` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instCategoryStructHom` `CategoryTheory.CategoryStruct.comp`	—	`id_hComp_id`
`hComp_assoc` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructHom` `CategoryTheory.eqToHom` `CategoryTheory.Category.assoc`	—	`Hom.ext` `CategoryTheory.Category.assoc` `homEquiv_comp` `Hom.base_eqToHom` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.CatEnriched.hComp_comp` `id_eq_eqToHom` `CategoryTheory.CatEnriched.eqToHom_hComp_eqToHom`
`hComp_assoc_heq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instQuiverHom` `CategoryTheory.CategoryStruct.comp` `hComp`	—	`CategoryTheory.Category.assoc` `hComp_assoc`
`hComp_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instCategoryStructHom` `hComp`	—	`homEquiv_comp` `CategoryTheory.Category.assoc` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.Category.id_comp`
`hComp_id` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.eqToHom` `CategoryTheory.Category.comp_id`	—	`Hom.ext` `CategoryTheory.Category.comp_id` `homEquiv_comp` `homEquiv_id` `Hom.base_eqToHom`
`hComp_id_heq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instQuiverHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `hComp` `instCategoryStructHom`	—	`CategoryTheory.Category.comp_id` `hComp_id`
`homEquiv_comp` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `toBase` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.eHomEquiv_comp`
`homEquiv_id` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `toBase` `EquivLike.toFunLike` `Equiv.instEquivLike` `homEquiv` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.eHomEquiv_id`
`id_eq_eqToHom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.eqToHom`	—	—
`id_hComp` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.Category.toCategoryStruct` `instCategory` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `instCategoryStructHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.eqToHom` `CategoryTheory.Category.id_comp`	—	`Hom.ext` `CategoryTheory.Category.id_comp` `homEquiv_comp` `homEquiv_id` `Hom.base_eqToHom`
`id_hComp_heq` 📖	mathematical	—	`Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instQuiverHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.CategoryStruct.id` `hComp` `instCategoryStructHom`	—	`CategoryTheory.Category.id_comp` `id_hComp`
`id_hComp_id` 📖	mathematical	—	`hComp` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instCategoryStructHom` `CategoryTheory.CategoryStruct.comp`	—	`homEquiv_comp` `CategoryTheory.CatEnriched.id_hComp_id` `CategoryTheory.Category.id_comp` `CategoryTheory.eqToHom_trans`
`instStrict` 📖	mathematical	—	`CategoryTheory.Bicategory.Strict` `CategoryTheory.CatEnrichedOrdinary` `instBicategory`	—	`CategoryTheory.Category.id_comp` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.assoc`
`mk_base` 📖	mathematical	—	`Hom.base`	—	—

CategoryTheory.CatEnrichedOrdinary.Hom

Definitions

Name	Category	Theorems
`base` 📖	CompOp	7 math math: `CategoryTheory.CatEnrichedOrdinary.mk_base`, `ext_iff`, `base_comp`, `CategoryTheory.CatEnrichedOrdinary.base_mk`, `comp_eq`, `base_eqToHom`, `base_id`
`base'` 📖	CompOp	—
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_comp` 📖	mathematical	—	`base` `CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CatEnrichedOrdinary.instCategory` `CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.CatEnrichedOrdinary.toBase` `CategoryTheory.CatEnriched.instCategoryHom` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.CatEnrichedOrdinary.homEquiv`	—	—
`base_eqToHom` 📖	mathematical	—	`base` `CategoryTheory.eqToHom` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CatEnrichedOrdinary.instCategory` `CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.CatEnrichedOrdinary.toBase` `CategoryTheory.CatEnriched.instCategoryHom` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.CatEnrichedOrdinary.homEquiv`	—	—
`base_id` 📖	mathematical	—	`base` `CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CatEnrichedOrdinary.instCategory` `CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.CatEnrichedOrdinary.toBase` `CategoryTheory.CatEnriched.instCategoryHom` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.CatEnrichedOrdinary.homEquiv`	—	—
`comp_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CatEnrichedOrdinary.instCategory` `CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.CatEnrichedOrdinary.toBase` `CategoryTheory.CatEnriched.instCategoryHom` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.CatEnrichedOrdinary.homEquiv` `base`	—	—
`ext` 📖	—	`base`	—	—	—
`ext_iff` 📖	mathematical	—	`base`	—	`ext`
`id_eq` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `Quiver.Hom` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CatEnrichedOrdinary.instCategory` `CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom` `CategoryTheory.CatEnriched` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.CatEnrichedOrdinary.toBase` `CategoryTheory.CatEnriched.instCategoryHom` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.CatEnrichedOrdinary.homEquiv`	—	—
`mk_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `Quiver.Hom` `CategoryTheory.CatEnriched` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.CatEnriched.instCategoryStruct` `CategoryTheory.EnrichedOrdinaryCategory.toEnrichedCategory` `CategoryTheory.Cat` `CategoryTheory.Cat.category` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Cat.instCartesianMonoidalCategory` `CategoryTheory.CatEnrichedOrdinary.toBase` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CatEnriched.instCategoryHom` `DFunLike.coe` `Equiv` `CategoryTheory.CatEnrichedOrdinary` `CategoryTheory.CatEnrichedOrdinary.instCategory` `EquivLike.toFunLike` `Equiv.instEquivLike` `CategoryTheory.CatEnrichedOrdinary.homEquiv` `CategoryTheory.CatEnrichedOrdinary.instCategoryStructHom`	—	—

---

← Back to Index