Basic

📁 Source: Mathlib/CategoryTheory/Bicategory/Monad/Basic.lean

Statistics

Metric	Count
Definitions Comonad, comul, counit, instId, ofOplaxFromUnit, toOplax, ComonadBicat, hom, inst, instComonadHom, mkOfComonad, obj, toOplax, termΔ, termε, «termΔ[_]», «termε[_]»	17
Theorems comul_assoc, comul_assoc_assoc, comul_assoc_flip, comul_assoc_flip_assoc, comul_counit, comul_counit_assoc, counit_comul, counit_comul_assoc, counit_def, mkOfComonad_comul, mkOfComonad_counit, mkOfComonad_hom	12
Total	29

CategoryTheory.Bicategory

Definitions

Name	Category	Theorems
Comonad 📖	CompOp	—
termΔ 📖	CompOp	—
termε 📖	CompOp	—
«termΔ[_]» 📖	CompOp	—
«termε[_]» 📖	CompOp	—

CategoryTheory.Bicategory.Comonad

Definitions

Name	Category	Theorems
comul 📖	CompOp	9 math math: comul_assoc_flip, comul_assoc_flip_assoc, counit_comul_assoc, comul_assoc, comul_counit_assoc, CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_comul, comul_assoc_assoc, counit_comul, comul_counit
counit 📖	CompOp	5 math math: counit_comul_assoc, comul_counit_assoc, counit_comul, comul_counit, CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_counit
instId 📖	CompOp	1 math math: counit_def
ofOplaxFromUnit 📖	CompOp	—
toOplax 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal comul CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Bicategory.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator	—	CategoryTheory.ComonObj.comul_assoc
comul_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal comul CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Bicategory.whiskerRight CategoryTheory.Iso.hom CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_assoc
comul_assoc_flip 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal comul CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator	—	CategoryTheory.ComonObj.comul_assoc_flip
comul_assoc_flip_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal comul CategoryTheory.Bicategory.whiskerRight CategoryTheory.Bicategory.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_assoc_flip
comul_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal CategoryTheory.CategoryStruct.id comul CategoryTheory.Bicategory.whiskerLeft counit CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor	—	CategoryTheory.ComonObj.comul_counit
comul_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal comul CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.whiskerLeft counit CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_counit
counit_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal CategoryTheory.CategoryStruct.id comul CategoryTheory.Bicategory.whiskerRight counit CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor	—	CategoryTheory.ComonObj.counit_comul
counit_comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.Category.toCategoryStruct CategoryTheory.instCategoryEndMonoidal comul CategoryTheory.CategoryStruct.id CategoryTheory.Bicategory.whiskerRight counit CategoryTheory.Iso.inv CategoryTheory.Bicategory.homCategory CategoryTheory.Bicategory.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_comul
counit_def 📖	mathematical	—	CategoryTheory.ComonObj.counit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Bicategory.toCategoryStruct CategoryTheory.instCategoryEndMonoidal CategoryTheory.instMonoidalCategoryHom CategoryTheory.CategoryStruct.id instId CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Bicategory.OplaxTrans

Definitions

Name	Category	Theorems
ComonadBicat 📖	CompOp	—

CategoryTheory.Bicategory.OplaxTrans.ComonadBicat

Definitions

Name	Category	Theorems
hom 📖	CompOp	3 math math: mkOfComonad_hom, mkOfComonad_comul, mkOfComonad_counit
inst 📖	CompOp	—
instComonadHom 📖	CompOp	2 math math: mkOfComonad_comul, mkOfComonad_counit
mkOfComonad 📖	CompOp	3 math math: mkOfComonad_hom, mkOfComonad_comul, mkOfComonad_counit
obj 📖	CompOp	2 math math: mkOfComonad_comul, mkOfComonad_counit
toOplax 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mkOfComonad_comul 📖	mathematical	—	CategoryTheory.Bicategory.Comonad.comul obj mkOfComonad hom instComonadHom	—	CategoryTheory.Category.id_comp
mkOfComonad_counit 📖	mathematical	—	CategoryTheory.Bicategory.Comonad.counit obj mkOfComonad hom instComonadHom	—	—
mkOfComonad_hom 📖	mathematical	—	hom mkOfComonad	—	—

---

← Back to Index