Documentation Verification Report

TwoP

📁 Source: Mathlib/CategoryTheory/Category/TwoP.lean

Statistics

Metric	Count
Definitions `TwoP`, `X`, `concreteCategory`, `hasForgetToBipointed`, `instCoeSortType`, `instInhabited`, `largeCategory`, `of`, `swap`, `swapEquiv`, `toBipointed`, `toTwoPointing`, `TwoP`, `pointedToTwoPFst`, `pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction`, `pointedToTwoPSnd`, `pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction`	17
Theorems `coe_of`, `coe_toBipointed`, `hom_ext`, `hom_ext_iff`, `swapEquiv_counitIso_hom_app_hom_toFun`, `swapEquiv_counitIso_inv_app_hom_toFun`, `swapEquiv_functor_map_hom_toFun`, `swapEquiv_functor_obj_X`, `swapEquiv_functor_obj_toTwoPointing_toProd`, `swapEquiv_inverse_map_hom_toFun`, `swapEquiv_inverse_obj_X`, `swapEquiv_inverse_obj_toTwoPointing_toProd`, `swapEquiv_symm`, `swapEquiv_unitIso_hom_app_hom_toFun`, `swapEquiv_unitIso_inv_app_hom_toFun`, `swap_map`, `swap_obj_X`, `swap_obj_toTwoPointing`, `TwoP_swap_comp_forget_to_Bipointed`, `pointedToTwoPFst_comp_forget_to_bipointed`, `pointedToTwoPFst_comp_swap`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_obj_X`, `pointedToTwoPFst_obj_toTwoPointing_toProd`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `pointedToTwoPSnd_comp_swap`, `pointedToTwoPSnd_map_hom_toFun`, `pointedToTwoPSnd_obj_X`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`	29
Total	46

TwoP

Definitions

Name	Category	Theorems
`X` 📖	CompOp	13 math math: `swapEquiv_functor_map_hom_toFun`, `coe_of`, `swap_obj_toTwoPointing`, `swapEquiv_inverse_obj_X`, `swap_map`, `pointedToTwoPFst_obj_X`, `pointedToTwoPSnd_obj_X`, `swapEquiv_functor_obj_X`, `swapEquiv_functor_obj_toTwoPointing_toProd`, `swapEquiv_inverse_obj_toTwoPointing_toProd`, `swapEquiv_inverse_map_hom_toFun`, `coe_toBipointed`, `swap_obj_X`
`concreteCategory` 📖	CompOp	3 math math: `TwoP_swap_comp_forget_to_Bipointed`, `pointedToTwoPFst_comp_forget_to_bipointed`, `pointedToTwoPSnd_comp_forget_to_bipointed`
`hasForgetToBipointed` 📖	CompOp	3 math math: `TwoP_swap_comp_forget_to_Bipointed`, `pointedToTwoPFst_comp_forget_to_bipointed`, `pointedToTwoPSnd_comp_forget_to_bipointed`
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`largeCategory` 📖	CompOp	25 math math: `pointedToTwoPFst_obj_toTwoPointing_toProd`, `TwoP_swap_comp_forget_to_Bipointed`, `swapEquiv_symm`, `swapEquiv_functor_map_hom_toFun`, `pointedToTwoPFst_comp_swap`, `swap_obj_toTwoPointing`, `swapEquiv_inverse_obj_X`, `swapEquiv_unitIso_hom_app_hom_toFun`, `swap_map`, `pointedToTwoPFst_obj_X`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `swapEquiv_counitIso_inv_app_hom_toFun`, `pointedToTwoPSnd_obj_X`, `swapEquiv_functor_obj_X`, `swapEquiv_functor_obj_toTwoPointing_toProd`, `swapEquiv_inverse_obj_toTwoPointing_toProd`, `swapEquiv_inverse_map_hom_toFun`, `pointedToTwoPSnd_comp_swap`, `swap_obj_X`, `pointedToTwoPSnd_map_hom_toFun`, `swapEquiv_counitIso_hom_app_hom_toFun`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `swapEquiv_unitIso_inv_app_hom_toFun`
`of` 📖	CompOp	1 math math: `coe_of`
`swap` 📖	CompOp	8 math math: `TwoP_swap_comp_forget_to_Bipointed`, `pointedToTwoPFst_comp_swap`, `swap_obj_toTwoPointing`, `swap_map`, `swapEquiv_counitIso_inv_app_hom_toFun`, `pointedToTwoPSnd_comp_swap`, `swap_obj_X`, `swapEquiv_counitIso_hom_app_hom_toFun`
`swapEquiv` 📖	CompOp	11 math math: `swapEquiv_symm`, `swapEquiv_functor_map_hom_toFun`, `swapEquiv_inverse_obj_X`, `swapEquiv_unitIso_hom_app_hom_toFun`, `swapEquiv_counitIso_inv_app_hom_toFun`, `swapEquiv_functor_obj_X`, `swapEquiv_functor_obj_toTwoPointing_toProd`, `swapEquiv_inverse_obj_toTwoPointing_toProd`, `swapEquiv_inverse_map_hom_toFun`, `swapEquiv_counitIso_hom_app_hom_toFun`, `swapEquiv_unitIso_inv_app_hom_toFun`
`toBipointed` 📖	CompOp	14 math math: `hom_ext_iff`, `TwoP_swap_comp_forget_to_Bipointed`, `swapEquiv_functor_map_hom_toFun`, `swapEquiv_unitIso_hom_app_hom_toFun`, `swap_map`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `swapEquiv_counitIso_inv_app_hom_toFun`, `swapEquiv_inverse_map_hom_toFun`, `coe_toBipointed`, `pointedToTwoPSnd_map_hom_toFun`, `swapEquiv_counitIso_hom_app_hom_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `swapEquiv_unitIso_inv_app_hom_toFun`
`toTwoPointing` 📖	CompOp	8 math math: `pointedToTwoPFst_obj_toTwoPointing_toProd`, `swapEquiv_functor_map_hom_toFun`, `swap_obj_toTwoPointing`, `swap_map`, `swapEquiv_functor_obj_toTwoPointing_toProd`, `swapEquiv_inverse_obj_toTwoPointing_toProd`, `swapEquiv_inverse_map_hom_toFun`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`X` `of`	—	—
`coe_toBipointed` 📖	mathematical	—	`Bipointed.X` `toBipointed` `X`	—	—
`hom_ext` 📖	—	`CategoryTheory.InducedCategory.Hom.hom` `TwoP` `Bipointed` `Bipointed.largeCategory` `toBipointed`	—	—	`CategoryTheory.InducedCategory.hom_ext`
`hom_ext_iff` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `TwoP` `Bipointed` `Bipointed.largeCategory` `toBipointed`	—	`hom_ext`
`swapEquiv_counitIso_hom_app_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `toBipointed` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Functor.comp` `swap` `CategoryTheory.InducedCategory.Hom.hom` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `swapEquiv`	—	—
`swapEquiv_counitIso_inv_app_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `toBipointed` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Functor.comp` `swap` `CategoryTheory.InducedCategory.Hom.hom` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `swapEquiv`	—	—
`swapEquiv_functor_map_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `toBipointed` `X` `TwoPointing.swap` `toTwoPointing` `CategoryTheory.InducedCategory.Hom.hom` `TwoP` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.Functor.map` `largeCategory` `CategoryTheory.Equivalence.functor` `swapEquiv` `DFunLike.coe` `Bipointed.HomSubtype` `Bipointed.instFunLikeHomSubtypeX` `CategoryTheory.ConcreteCategory.hom` `Bipointed.X` `Bipointed.hasForget`	—	—
`swapEquiv_functor_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Equivalence.functor` `swapEquiv`	—	—
`swapEquiv_functor_obj_toTwoPointing_toProd` 📖	mathematical	—	`TwoPointing.toProd` `X` `toTwoPointing` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Equivalence.functor` `swapEquiv`	—	—
`swapEquiv_inverse_map_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `toBipointed` `X` `TwoPointing.swap` `toTwoPointing` `CategoryTheory.InducedCategory.Hom.hom` `TwoP` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.Functor.map` `largeCategory` `CategoryTheory.Equivalence.inverse` `swapEquiv` `DFunLike.coe` `Bipointed.HomSubtype` `Bipointed.instFunLikeHomSubtypeX` `CategoryTheory.ConcreteCategory.hom` `Bipointed.X` `Bipointed.hasForget`	—	—
`swapEquiv_inverse_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Equivalence.inverse` `swapEquiv`	—	—
`swapEquiv_inverse_obj_toTwoPointing_toProd` 📖	mathematical	—	`TwoPointing.toProd` `X` `toTwoPointing` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Equivalence.inverse` `swapEquiv`	—	—
`swapEquiv_symm` 📖	mathematical	—	`CategoryTheory.Equivalence.symm` `TwoP` `largeCategory` `swapEquiv`	—	—
`swapEquiv_unitIso_hom_app_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `toBipointed` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.InducedCategory.Hom.hom` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `swapEquiv`	—	—
`swapEquiv_unitIso_inv_app_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `toBipointed` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.InducedCategory.Hom.hom` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `swapEquiv`	—	—
`swap_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `TwoP` `largeCategory` `swap` `CategoryTheory.InducedCategory.homMk` `Bipointed` `Bipointed.largeCategory` `toBipointed` `X` `TwoPointing.swap` `toTwoPointing` `DFunLike.coe` `Bipointed.HomSubtype` `Bipointed.X` `Bipointed.instFunLikeHomSubtypeX` `CategoryTheory.ConcreteCategory.hom` `Bipointed.hasForget` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`swap_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `swap`	—	—
`swap_obj_toTwoPointing` 📖	mathematical	—	`toTwoPointing` `CategoryTheory.Functor.obj` `TwoP` `largeCategory` `swap` `TwoPointing.swap` `X`	—	—

TwoPointing

Definitions

Name	Category	Theorems
`TwoP` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`TwoP` 📖	CompData	26 math math: `pointedToTwoPFst_obj_toTwoPointing_toProd`, `TwoP.hom_ext_iff`, `TwoP_swap_comp_forget_to_Bipointed`, `TwoP.swapEquiv_symm`, `TwoP.swapEquiv_functor_map_hom_toFun`, `pointedToTwoPFst_comp_swap`, `TwoP.swap_obj_toTwoPointing`, `TwoP.swapEquiv_inverse_obj_X`, `TwoP.swapEquiv_unitIso_hom_app_hom_toFun`, `TwoP.swap_map`, `pointedToTwoPFst_obj_X`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `TwoP.swapEquiv_counitIso_inv_app_hom_toFun`, `pointedToTwoPSnd_obj_X`, `TwoP.swapEquiv_functor_obj_X`, `TwoP.swapEquiv_functor_obj_toTwoPointing_toProd`, `TwoP.swapEquiv_inverse_obj_toTwoPointing_toProd`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `pointedToTwoPSnd_comp_swap`, `TwoP.swap_obj_X`, `pointedToTwoPSnd_map_hom_toFun`, `TwoP.swapEquiv_counitIso_hom_app_hom_toFun`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `TwoP.swapEquiv_unitIso_inv_app_hom_toFun`
`pointedToTwoPFst` 📖	CompOp	6 math math: `pointedToTwoPFst_obj_toTwoPointing_toProd`, `pointedToTwoPFst_comp_swap`, `pointedToTwoPFst_obj_X`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `pointedToTwoPSnd_comp_swap`
`pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction` 📖	CompOp	—
`pointedToTwoPSnd` 📖	CompOp	6 math math: `pointedToTwoPFst_comp_swap`, `pointedToTwoPSnd_obj_X`, `pointedToTwoPSnd_comp_swap`, `pointedToTwoPSnd_map_hom_toFun`, `pointedToTwoPSnd_obj_toTwoPointing_toProd`, `pointedToTwoPSnd_comp_forget_to_bipointed`
`pointedToTwoPSndForgetCompBipointedToPointedSndAdjunction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`TwoP_swap_comp_forget_to_Bipointed` 📖	mathematical	—	`CategoryTheory.Functor.comp` `TwoP` `TwoP.largeCategory` `Bipointed` `Bipointed.largeCategory` `TwoP.swap` `CategoryTheory.forget₂` `Bipointed.HomSubtype` `TwoP.toBipointed` `Bipointed.X` `Bipointed.instFunLikeHomSubtypeX` `TwoP.concreteCategory` `Bipointed.hasForget` `TwoP.hasForgetToBipointed` `Bipointed.swap`	—	—
`pointedToTwoPFst_comp_forget_to_bipointed` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `Bipointed` `Bipointed.largeCategory` `pointedToTwoPFst` `CategoryTheory.forget₂` `Bipointed.HomSubtype` `TwoP.toBipointed` `Bipointed.X` `Bipointed.instFunLikeHomSubtypeX` `TwoP.concreteCategory` `Bipointed.hasForget` `TwoP.hasForgetToBipointed` `pointedToBipointedFst`	—	—
`pointedToTwoPFst_comp_swap` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `pointedToTwoPFst` `TwoP.swap` `pointedToTwoPSnd`	—	—
`pointedToTwoPFst_map_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `TwoP.toBipointed` `Pointed.X` `Pointed.point` `CategoryTheory.InducedCategory.Hom.hom` `TwoP` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.Functor.map` `Pointed` `Pointed.largeCategory` `TwoP.largeCategory` `pointedToTwoPFst` `Pointed.Hom.toFun`	—	—
`pointedToTwoPFst_obj_X` 📖	mathematical	—	`TwoP.X` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `pointedToTwoPFst` `Pointed.X`	—	—
`pointedToTwoPFst_obj_toTwoPointing_toProd` 📖	mathematical	—	`TwoPointing.toProd` `Pointed.X` `TwoP.toTwoPointing` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `pointedToTwoPFst` `Pointed.point`	—	—
`pointedToTwoPSnd_comp_forget_to_bipointed` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `Bipointed` `Bipointed.largeCategory` `pointedToTwoPSnd` `CategoryTheory.forget₂` `Bipointed.HomSubtype` `TwoP.toBipointed` `Bipointed.X` `Bipointed.instFunLikeHomSubtypeX` `TwoP.concreteCategory` `Bipointed.hasForget` `TwoP.hasForgetToBipointed` `pointedToBipointedSnd`	—	—
`pointedToTwoPSnd_comp_swap` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `pointedToTwoPSnd` `TwoP.swap` `pointedToTwoPFst`	—	—
`pointedToTwoPSnd_map_hom_toFun` 📖	mathematical	—	`Bipointed.Hom.toFun` `TwoP.toBipointed` `Pointed.X` `Pointed.point` `CategoryTheory.InducedCategory.Hom.hom` `TwoP` `Bipointed` `Bipointed.largeCategory` `CategoryTheory.Functor.map` `Pointed` `Pointed.largeCategory` `TwoP.largeCategory` `pointedToTwoPSnd` `Pointed.Hom.toFun`	—	—
`pointedToTwoPSnd_obj_X` 📖	mathematical	—	`TwoP.X` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `pointedToTwoPSnd` `Pointed.X`	—	—
`pointedToTwoPSnd_obj_toTwoPointing_toProd` 📖	mathematical	—	`TwoPointing.toProd` `Pointed.X` `TwoP.toTwoPointing` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `TwoP` `TwoP.largeCategory` `pointedToTwoPSnd` `Pointed.point`	—	—

---

← Back to Index