0 | module Control.Category.Comonad
 1 |
 2 | import Control.Category.Core
 3 | import Control.Category.Functor
 4 | import Control.Category.Monoidal
 5 | import Control.Category.MonFunctor
 6 | import Data.Morphisms
 7 |
 8 | %default total
 9 |
10 | ------------------------------------------------------------
11 | -- Interface
12 | ------------------------------------------------------------
13 |
14 | ||| A *comonad* `w` is a comonoid object in the category of
15 | ||| endofunctors in `cat`, where the tensor product is given by
16 | ||| composition. Generally, `cat` is a category, though this is not
17 | ||| enforced by the interface.
18 | |||
19 | ||| This is the interface-style definition of a comonad. For the
20 | ||| record-style definition, see `Control.Category.Records.ComonadR`.
21 | |||
22 | ||| Laws (when `cat` is a category):
23 | ||| * `counit . cojoin = id`
24 | ||| * `map counit . cojoin = id`
25 | ||| * `cojoin . cojoin = map cojoin . cojoin`
26 | public export
27 | interface CatFunctor cat cat w => CatComonad
28 |     (0 cat : Hom obj)
29 |     (0 w : obj -> obj) | cat,w where
30 |   constructor MkCatComonad
31 |   ||| The cojoin transformation of the comonad.
32 |   cojoin : {a : _} -> cat (w a) (w (w a))
33 |   ||| The counit transformation of the comonad.
34 |   counit : {a : _} -> cat (w a) a
35 |
36 | ||| A strong comonad is a comonad that is also a costrong functor,
37 | ||| with additional compatibility laws.
38 | |||
39 | ||| Laws:
40 | ||| * `mapr counit . costrongl = counit`
41 | ||| * `mapl counit . costrongr = counit`
42 | ||| * `costrongl . map costrongl . cojoin = mapr cojoin . costrongl`
43 | ||| * `costrongr . map costrongr . cojoin = mapl cojoin . costrongr`
44 | public export
45 | StrongComonad : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (w : obj -> obj) -> Type
46 | StrongComonad cat ten w = (CatComonad cat w, CostrongFunctor cat ten w)
47 |
48 |
49 | ------------------------------------------------------------
50 | -- Existing Instances
51 | ------------------------------------------------------------
52 |
53 | namespace CatComonad
54 |   public export
55 |   [Id] Category cat => CatComonad cat Prelude.id
56 |       using CatFunctor.Id where
57 |     cojoin = id
58 |     counit = id
59 |
60 | namespace StrongComonad
61 |   public export
62 |   Id : {ten : _} -> Category cat => StrongComonad cat ten Prelude.id
63 |   Id = (Id, Id)
64 |