Structures · Category theory
CategoryTheory.BimonObj
A bimonoid object in a braided category C is an object that is simultaneously monoid and comonoid
objects, and structure morphisms of them satisfy appropriate consistency conditions.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Bimon_
- Shape
- One type argument · adds mul_comul, one_comul, mul_counit, one_counit
Extends2
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by20
- CategoryTheory.BimonObj.one_comul
- CategoryTheory.Bimon.compatibility
- CategoryTheory.Bimon.mk'X
- CategoryTheory.BimonObj.mul_comul
- CategoryTheory.BimonObj.one_counit
- CategoryTheory.BimonObj.mul_counit
- CategoryTheory.Bimon.mul_counit
- CategoryTheory.BimonObj.mul_counit_assoc
- CategoryTheory.BimonObj.one_counit_assoc
- CategoryTheory.Bimon.one_comul
- CategoryTheory.Bimon.compatibility_assoc
- CategoryTheory.Bimon.one_comul_assoc
- CategoryTheory.Bimon.mk'
- CategoryTheory.BimonObj.toMonObj
- CategoryTheory.BimonObj.one_comul_assoc
- CategoryTheory.BimonObj.mul_comul_assoc
- CategoryTheory.Bimon.mk'X_X
- CategoryTheory.Bimon.mul_counit_assoc
- CategoryTheory.BimonObj.toComonObj
- CategoryTheory.Bimon.mk'_X