Documentation Verification Report

Bipointed

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

Statistics

Metric	Count
Definitions `Bipointed`, `comp`, `id`, `instInhabited`, `toFun`, `HomSubtype`, `X`, `hasForget`, `instCoeSortType`, `instFunLikeHomSubtypeX`, `instInhabited`, `largeCategory`, `of`, `swap`, `swapEquiv`, `toProd`, `Bipointed`, `bipointedToPointedFst`, `bipointedToPointedSnd`, `pointedToBipointed`, `pointedToBipointedCompBipointedToPointedFst`, `pointedToBipointedCompBipointedToPointedSnd`, `pointedToBipointedFst`, `pointedToBipointedFstBipointedToPointedFstAdjunction`, `pointedToBipointedSnd`, `pointedToBipointedSndBipointedToPointedSndAdjunction`	26
Theorems `comp_toFun`, `ext`, `ext_iff`, `id_toFun`, `map_fst`, `map_snd`, `coe_of`, `swapEquiv_counitIso_hom_app_toFun`, `swapEquiv_counitIso_inv_app_toFun`, `swapEquiv_functor_map_toFun`, `swapEquiv_functor_obj_X`, `swapEquiv_functor_obj_toProd`, `swapEquiv_inverse_map_toFun`, `swapEquiv_inverse_obj_X`, `swapEquiv_inverse_obj_toProd`, `swapEquiv_symm`, `swapEquiv_unitIso_hom_app_toFun`, `swapEquiv_unitIso_inv_app_toFun`, `swap_map_toFun`, `swap_obj_X`, `swap_obj_toProd`, `bipointedToPointedFst_comp_forget`, `bipointedToPointedSnd_comp_forget`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `pointedToBipointedFst_comp_swap`, `pointedToBipointedSnd_comp_swap`, `swap_comp_bipointedToPointedFst`, `swap_comp_bipointedToPointedSnd`	31
Total	57

Bipointed

Definitions

Name	Category	Theorems
`HomSubtype` 📖	CompOp	9 math math: `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `TwoP.swapEquiv_functor_map_hom_toFun`, `TwoP.swap_map`, `pointedToTwoPFst_comp_forget_to_bipointed`, `bipointedToPointedSnd_comp_forget`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `bipointedToPointedFst_comp_forget`
`X` 📖	CompOp	24 math math: `swapEquiv_functor_obj_toProd`, `swapEquiv_inverse_obj_toProd`, `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `TwoP.swapEquiv_functor_map_hom_toFun`, `swap_obj_X`, `swapEquiv_inverse_map_toFun`, `swapEquiv_inverse_obj_X`, `Hom.comp_toFun`, `Hom.map_snd`, `TwoP.swap_map`, `pointedToTwoPFst_comp_forget_to_bipointed`, `swapEquiv_functor_map_toFun`, `swap_obj_toProd`, `swapEquiv_functor_obj_X`, `coe_of`, `bipointedToPointedSnd_comp_forget`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `TwoP.coe_toBipointed`, `Hom.id_toFun`, `Hom.map_fst`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `swap_map_toFun`, `bipointedToPointedFst_comp_forget`
`hasForget` 📖	CompOp	9 math math: `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `TwoP.swapEquiv_functor_map_hom_toFun`, `TwoP.swap_map`, `pointedToTwoPFst_comp_forget_to_bipointed`, `bipointedToPointedSnd_comp_forget`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `bipointedToPointedFst_comp_forget`
`instCoeSortType` 📖	CompOp	—
`instFunLikeHomSubtypeX` 📖	CompOp	9 math math: `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `TwoP.swapEquiv_functor_map_hom_toFun`, `TwoP.swap_map`, `pointedToTwoPFst_comp_forget_to_bipointed`, `bipointedToPointedSnd_comp_forget`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `bipointedToPointedFst_comp_forget`
`instInhabited` 📖	CompOp	—
`largeCategory` 📖	CompOp	38 math math: `swapEquiv_functor_obj_toProd`, `pointedToBipointedFst_comp_swap`, `swapEquiv_inverse_obj_toProd`, `TwoP.hom_ext_iff`, `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `TwoP.swapEquiv_functor_map_hom_toFun`, `swap_comp_bipointedToPointedFst`, `swapEquiv_counitIso_hom_app_toFun`, `swap_obj_X`, `swapEquiv_inverse_map_toFun`, `swapEquiv_inverse_obj_X`, `swapEquiv_unitIso_inv_app_toFun`, `TwoP.swapEquiv_unitIso_hom_app_hom_toFun`, `TwoP.swap_map`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `TwoP.swapEquiv_counitIso_inv_app_hom_toFun`, `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `swapEquiv_functor_map_toFun`, `swap_obj_toProd`, `swapEquiv_functor_obj_X`, `swapEquiv_counitIso_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`, `bipointedToPointedSnd_comp_forget`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `swap_comp_bipointedToPointedSnd`, `pointedToTwoPSnd_map_hom_toFun`, `TwoP.swapEquiv_counitIso_hom_app_hom_toFun`, `swapEquiv_unitIso_hom_app_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `swapEquiv_symm`, `swap_map_toFun`, `pointedToBipointedSnd_comp_swap`, `TwoP.swapEquiv_unitIso_inv_app_hom_toFun`, `bipointedToPointedFst_comp_forget`
`of` 📖	CompOp	1 math math: `coe_of`
`swap` 📖	CompOp	11 math math: `pointedToBipointedFst_comp_swap`, `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `swap_comp_bipointedToPointedFst`, `swapEquiv_counitIso_hom_app_toFun`, `swap_obj_X`, `swap_obj_toProd`, `swapEquiv_counitIso_inv_app_toFun`, `swap_comp_bipointedToPointedSnd`, `swap_map_toFun`, `pointedToBipointedSnd_comp_swap`
`swapEquiv` 📖	CompOp	11 math math: `swapEquiv_functor_obj_toProd`, `swapEquiv_inverse_obj_toProd`, `swapEquiv_counitIso_hom_app_toFun`, `swapEquiv_inverse_map_toFun`, `swapEquiv_inverse_obj_X`, `swapEquiv_unitIso_inv_app_toFun`, `swapEquiv_functor_map_toFun`, `swapEquiv_functor_obj_X`, `swapEquiv_counitIso_inv_app_toFun`, `swapEquiv_unitIso_hom_app_toFun`, `swapEquiv_symm`
`toProd` 📖	CompOp	8 math math: `swapEquiv_functor_obj_toProd`, `swapEquiv_inverse_obj_toProd`, `swapEquiv_inverse_map_toFun`, `Hom.map_snd`, `swapEquiv_functor_map_toFun`, `swap_obj_toProd`, `Hom.map_fst`, `swap_map_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`X` `of`	—	—
`swapEquiv_counitIso_hom_app_toFun` 📖	mathematical	—	`Hom.toFun` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Functor.comp` `swap` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `swapEquiv`	—	—
`swapEquiv_counitIso_inv_app_toFun` 📖	mathematical	—	`Hom.toFun` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Functor.comp` `swap` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.counitIso` `swapEquiv`	—	—
`swapEquiv_functor_map_toFun` 📖	mathematical	—	`Hom.toFun` `X` `toProd` `CategoryTheory.Functor.map` `Bipointed` `largeCategory` `CategoryTheory.Equivalence.functor` `swapEquiv`	—	—
`swapEquiv_functor_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Equivalence.functor` `swapEquiv`	—	—
`swapEquiv_functor_obj_toProd` 📖	mathematical	—	`toProd` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Equivalence.functor` `swapEquiv` `X`	—	—
`swapEquiv_inverse_map_toFun` 📖	mathematical	—	`Hom.toFun` `X` `toProd` `CategoryTheory.Functor.map` `Bipointed` `largeCategory` `CategoryTheory.Equivalence.inverse` `swapEquiv`	—	—
`swapEquiv_inverse_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Equivalence.inverse` `swapEquiv`	—	—
`swapEquiv_inverse_obj_toProd` 📖	mathematical	—	`toProd` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Equivalence.inverse` `swapEquiv` `X`	—	—
`swapEquiv_symm` 📖	mathematical	—	`CategoryTheory.Equivalence.symm` `Bipointed` `largeCategory` `swapEquiv`	—	—
`swapEquiv_unitIso_hom_app_toFun` 📖	mathematical	—	`Hom.toFun` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `swapEquiv`	—	—
`swapEquiv_unitIso_inv_app_toFun` 📖	mathematical	—	`Hom.toFun` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Equivalence.unitIso` `swapEquiv`	—	—
`swap_map_toFun` 📖	mathematical	—	`Hom.toFun` `X` `toProd` `CategoryTheory.Functor.map` `Bipointed` `largeCategory` `swap`	—	—
`swap_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `swap`	—	—
`swap_obj_toProd` 📖	mathematical	—	`toProd` `CategoryTheory.Functor.obj` `Bipointed` `largeCategory` `swap` `X`	—	—

Bipointed.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	1 math math: `comp_toFun`
`id` 📖	CompOp	1 math math: `id_toFun`
`instInhabited` 📖	CompOp	—
`toFun` 📖	CompOp	20 math math: `TwoP.swapEquiv_functor_map_hom_toFun`, `Bipointed.swapEquiv_counitIso_hom_app_toFun`, `Bipointed.swapEquiv_inverse_map_toFun`, `Bipointed.swapEquiv_unitIso_inv_app_toFun`, `comp_toFun`, `map_snd`, `TwoP.swapEquiv_unitIso_hom_app_hom_toFun`, `pointedToTwoPFst_map_hom_toFun`, `TwoP.swapEquiv_counitIso_inv_app_hom_toFun`, `Bipointed.swapEquiv_functor_map_toFun`, `Bipointed.swapEquiv_counitIso_inv_app_toFun`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `ext_iff`, `pointedToTwoPSnd_map_hom_toFun`, `TwoP.swapEquiv_counitIso_hom_app_hom_toFun`, `id_toFun`, `map_fst`, `Bipointed.swapEquiv_unitIso_hom_app_toFun`, `Bipointed.swap_map_toFun`, `TwoP.swapEquiv_unitIso_inv_app_hom_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_toFun` 📖	mathematical	—	`toFun` `comp` `Bipointed.X`	—	—
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`id_toFun` 📖	mathematical	—	`toFun` `id` `Bipointed.X`	—	—
`map_fst` 📖	mathematical	—	`toFun` `Bipointed.X` `Bipointed.toProd`	—	—
`map_snd` 📖	mathematical	—	`toFun` `Bipointed.X` `Bipointed.toProd`	—	—

Prod

Definitions

Name	Category	Theorems
`Bipointed` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`Bipointed` 📖	CompData	38 math math: `Bipointed.swapEquiv_functor_obj_toProd`, `pointedToBipointedFst_comp_swap`, `Bipointed.swapEquiv_inverse_obj_toProd`, `TwoP.hom_ext_iff`, `TwoP_swap_comp_forget_to_Bipointed`, `bddOrd_dual_comp_forget_to_bipointed`, `TwoP.swapEquiv_functor_map_hom_toFun`, `swap_comp_bipointedToPointedFst`, `Bipointed.swapEquiv_counitIso_hom_app_toFun`, `Bipointed.swap_obj_X`, `Bipointed.swapEquiv_inverse_map_toFun`, `Bipointed.swapEquiv_inverse_obj_X`, `Bipointed.swapEquiv_unitIso_inv_app_toFun`, `TwoP.swapEquiv_unitIso_hom_app_hom_toFun`, `TwoP.swap_map`, `pointedToTwoPFst_map_hom_toFun`, `pointedToTwoPFst_comp_forget_to_bipointed`, `TwoP.swapEquiv_counitIso_inv_app_hom_toFun`, `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `Bipointed.swapEquiv_functor_map_toFun`, `Bipointed.swap_obj_toProd`, `Bipointed.swapEquiv_functor_obj_X`, `Bipointed.swapEquiv_counitIso_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`, `bipointedToPointedSnd_comp_forget`, `TwoP.swapEquiv_inverse_map_hom_toFun`, `swap_comp_bipointedToPointedSnd`, `pointedToTwoPSnd_map_hom_toFun`, `TwoP.swapEquiv_counitIso_hom_app_hom_toFun`, `Bipointed.swapEquiv_unitIso_hom_app_toFun`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `Bipointed.swapEquiv_symm`, `Bipointed.swap_map_toFun`, `pointedToBipointedSnd_comp_swap`, `TwoP.swapEquiv_unitIso_inv_app_hom_toFun`, `bipointedToPointedFst_comp_forget`
`bipointedToPointedFst` 📖	CompOp	5 math math: `swap_comp_bipointedToPointedFst`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`, `swap_comp_bipointedToPointedSnd`, `bipointedToPointedFst_comp_forget`
`bipointedToPointedSnd` 📖	CompOp	5 math math: `swap_comp_bipointedToPointedFst`, `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `bipointedToPointedSnd_comp_forget`, `swap_comp_bipointedToPointedSnd`
`pointedToBipointed` 📖	CompOp	4 math math: `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`
`pointedToBipointedCompBipointedToPointedFst` 📖	CompOp	2 math math: `pointedToBipointedCompBipointedToPointedFst_inv_app_toFun`, `pointedToBipointedCompBipointedToPointedFst_hom_app_toFun`
`pointedToBipointedCompBipointedToPointedSnd` 📖	CompOp	2 math math: `pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun`, `pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun`
`pointedToBipointedFst` 📖	CompOp	3 math math: `pointedToBipointedFst_comp_swap`, `pointedToTwoPFst_comp_forget_to_bipointed`, `pointedToBipointedSnd_comp_swap`
`pointedToBipointedFstBipointedToPointedFstAdjunction` 📖	CompOp	—
`pointedToBipointedSnd` 📖	CompOp	3 math math: `pointedToBipointedFst_comp_swap`, `pointedToTwoPSnd_comp_forget_to_bipointed`, `pointedToBipointedSnd_comp_swap`
`pointedToBipointedSndBipointedToPointedSndAdjunction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bipointedToPointedFst_comp_forget` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `Pointed` `Pointed.largeCategory` `CategoryTheory.types` `bipointedToPointedFst` `CategoryTheory.forget` `Pointed.X` `Pointed.point` `Pointed.instFunLikeSubtypeForallXEqPoint` `Pointed.hasForget` `Bipointed.HomSubtype` `Bipointed.X` `Bipointed.instFunLikeHomSubtypeX` `Bipointed.hasForget`	—	—
`bipointedToPointedSnd_comp_forget` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `Pointed` `Pointed.largeCategory` `CategoryTheory.types` `bipointedToPointedSnd` `CategoryTheory.forget` `Pointed.X` `Pointed.point` `Pointed.instFunLikeSubtypeForallXEqPoint` `Pointed.hasForget` `Bipointed.HomSubtype` `Bipointed.X` `Bipointed.instFunLikeHomSubtypeX` `Bipointed.hasForget`	—	—
`pointedToBipointedCompBipointedToPointedFst_hom_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `pointedToBipointed` `bipointedToPointedFst` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `pointedToBipointedCompBipointedToPointedFst`	—	—
`pointedToBipointedCompBipointedToPointedFst_inv_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `pointedToBipointed` `bipointedToPointedFst` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `pointedToBipointedCompBipointedToPointedFst`	—	—
`pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `pointedToBipointed` `bipointedToPointedSnd` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `pointedToBipointedCompBipointedToPointedSnd`	—	—
`pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun` 📖	mathematical	—	`Pointed.Hom.toFun` `CategoryTheory.Functor.obj` `Pointed` `Pointed.largeCategory` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `pointedToBipointed` `bipointedToPointedSnd` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `pointedToBipointedCompBipointedToPointedSnd`	—	—
`pointedToBipointedFst_comp_swap` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `Bipointed` `Bipointed.largeCategory` `pointedToBipointedFst` `Bipointed.swap` `pointedToBipointedSnd`	—	—
`pointedToBipointedSnd_comp_swap` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Pointed` `Pointed.largeCategory` `Bipointed` `Bipointed.largeCategory` `pointedToBipointedSnd` `Bipointed.swap` `pointedToBipointedFst`	—	—
`swap_comp_bipointedToPointedFst` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `Pointed` `Pointed.largeCategory` `Bipointed.swap` `bipointedToPointedFst` `bipointedToPointedSnd`	—	—
`swap_comp_bipointedToPointedSnd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `Bipointed` `Bipointed.largeCategory` `Pointed` `Pointed.largeCategory` `Bipointed.swap` `bipointedToPointedSnd` `bipointedToPointedFst`	—	—

---

← Back to Index