module Cat.Diagram.Comonad {o β„“} (C : Precategory o β„“) where


A comonad on a category is dual to a monad on instead of a unit and multiplication we have a counit and comultiplication

record Comonad : Type (o βŠ” β„“) where
    W : Functor C C
    counit : W => Id
    comult : W => (W F∘ W)

We also have equations governing the counit and comultiplication. Unsurprisingly, these are dual to the equations of a monad.

    left-ident : βˆ€ {x} β†’ W₁ (counit.Ξ΅ x) ∘ comult.Ξ· x ≑ id
    right-ident : βˆ€ {x} β†’ counit.Ξ΅ (Wβ‚€ x) ∘ comult.Ξ· x ≑ id
    comult-assoc : βˆ€ {x} β†’ W₁ (comult.Ξ· x) ∘ comult.Ξ· x ≑ comult.Ξ· (Wβ‚€ x) ∘ comult.Ξ· x