Documentation Verification Report

Bicones

📁 Source: Mathlib/CategoryTheory/Limits/Bicones.lean

Statistics

Metric	Count
Definitions `Bicone`, `BiconeHom`, `decidableEq`, `biconeCategory`, `biconeCategoryStruct`, `biconeFinCategory`, `biconeMk`, `biconeSmallCategory`, `finBicone`, `finBiconeHom`, `instDecidableEqBicone`, `decEq`, `instInhabitedBicone`, `instInhabitedBiconeHomLeft`	14
Theorems `biconeCategoryStruct_comp`, `biconeCategoryStruct_id`, `biconeMk_map`, `biconeMk_obj`	4
Total	18

CategoryTheory

Definitions

Name	Category	Theorems
`Bicone` 📖	CompData	4 math math: `biconeCategoryStruct_comp`, `biconeMk_obj`, `biconeCategoryStruct_id`, `biconeMk_map`
`BiconeHom` 📖	CompData	1 math math: `biconeCategoryStruct_id`
`biconeCategory` 📖	CompOp	2 math math: `biconeMk_obj`, `biconeMk_map`
`biconeCategoryStruct` 📖	CompOp	2 math math: `biconeCategoryStruct_comp`, `biconeCategoryStruct_id`
`biconeFinCategory` 📖	CompOp	—
`biconeMk` 📖	CompOp	2 math math: `biconeMk_obj`, `biconeMk_map`
`biconeSmallCategory` 📖	CompOp	—
`finBicone` 📖	CompOp	—
`finBiconeHom` 📖	CompOp	—
`instDecidableEqBicone` 📖	CompOp	—
`instInhabitedBicone` 📖	CompOp	—
`instInhabitedBiconeHomLeft` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biconeCategoryStruct_comp` 📖	mathematical	—	`CategoryStruct.comp` `Bicone` `biconeCategoryStruct` `Bicone.left` `Bicone.right` `Bicone.diagram` `BiconeHom.left` `BiconeHom.right` `BiconeHom.diagram` `Category.toCategoryStruct`	—	—
`biconeCategoryStruct_id` 📖	mathematical	—	`CategoryStruct.id` `Bicone` `biconeCategoryStruct` `BiconeHom` `BiconeHom.left_id` `BiconeHom.right_id` `BiconeHom.diagram` `Category.toCategoryStruct`	—	—
`biconeMk_map` 📖	mathematical	—	`Functor.map` `Bicone` `biconeCategory` `biconeMk` `Bicone.left` `CategoryStruct.id` `Category.toCategoryStruct` `Limits.Cone.pt` `Functor.obj` `Bicone.right` `Bicone.diagram` `NatTrans.app` `Functor` `Functor.category` `Functor.const` `Limits.Cone.π`	—	—
`biconeMk_obj` 📖	mathematical	—	`Functor.obj` `Bicone` `biconeCategory` `biconeMk` `Limits.Cone.pt`	—	—

CategoryTheory.BiconeHom

Definitions

Name	Category	Theorems
`decidableEq` 📖	CompOp	—

CategoryTheory.instDecidableEqBicone

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

---

← Back to Index