Commit 2024-05-09 16:03 fa33d89f

View on Github →

feat: basic definition of comonoid objects (#10091)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Comon_.lean

added structure Comon_.Hom

added def Comon_.comp

added theorem Comon_.comp_hom'

added theorem Comon_.comul_assoc_flip

added theorem Comon_.comul_counit_hom

added theorem Comon_.counit_comul_hom

added theorem Comon_.ext

added def Comon_.forget

added def Comon_.id

added theorem Comon_.id_hom'

added def Comon_.mkIso

added def Comon_.trivial

added structure Comon_