0 | module Control.Category.Records.Comonad
  1 |
  2 | import Control.Category
  3 | import Control.Category.Records.Category
  4 | import Control.Category.Records.Monoidal
  5 | import Control.Category.Records.Functor
  6 | import Control.Category.Records.MonFunctor
  7 |
  8 | %default total
  9 | %prefix_record_projections off
 10 |
 11 | ||| A *comonad* `m` is a comonoid object in the category of
 12 | ||| endofunctors in `cat`, where the tensor product is given by
 13 | ||| composition.
 14 | |||
 15 | ||| See `CatComonad` for required laws.
 16 | public export
 17 | record ComonadR (cat : CategoryR) where
 18 |   constructor MkComonadR
 19 |   fun : cat.obj -> cat.obj
 20 |   {auto impl : CatComonad cat.hom fun}
 21 |
 22 | namespace ComonadR
 23 |   ||| Convert this into a `FunctorR`.
 24 |   public export %inline
 25 |   (.functorR) : (rec : ComonadR cat) -> EndofunctorR cat
 26 |   (.functorR) (MkComonadR {} {fun}) = MkFunctorR fun
 27 |
 28 |   ||| Apply the monad to a morphism in `cat`.
 29 |   public export %inline
 30 |   (.map) : (rec : ComonadR cat) -> {a,b : _} ->
 31 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
 32 |   (.map) rec@(MkComonadR {}) = map' {cat=cat.hom}
 33 |
 34 |
 35 |   ||| Convert this into a `ComonadR`.
 36 |   public export %inline
 37 |   (.comonadR) : (rec : ComonadR cat) -> ComonadR cat
 38 |   (.comonadR) = id
 39 |
 40 |   ||| The cojoin transformation of the comonad.
 41 |   public export %inline
 42 |   (.cojoin) : (rec : ComonadR cat) -> {a : _} ->
 43 |               cat.hom (rec.fun a) (rec.fun (rec.fun a))
 44 |   (.cojoin) rec = cojoin @{rec.impl}
 45 |
 46 |   ||| The counit transformation of the comonad.
 47 |   public export %inline
 48 |   (.counit) : (rec : ComonadR cat) -> {a : _} ->
 49 |               cat.hom (rec.fun a) a
 50 |   (.counit) rec = counit @{rec.impl}
 51 |
 52 |
 53 | ||| A strong comonad is a comonad that is also a costrong functor.
 54 | |||
 55 | ||| See `StrongComonad` for required laws.
 56 | public export
 57 | record StrongComonadR (cat : MonoidalR) where
 58 |   constructor MkStrongComonadR
 59 |   fun : cat.obj -> cat.obj
 60 |   {auto impl : StrongComonad cat.hom cat.tensor fun}
 61 |
 62 | namespace StrongComonadR
 63 |   ||| Convert this into a `FunctorR`.
 64 |   public export %inline
 65 |   (.functorR) : (rec : StrongComonadR cat) -> EndofunctorR cat.categoryR
 66 |   (.functorR) {cat=MkMonoidalR{}} (MkStrongComonadR {} {fun}) = MkFunctorR fun
 67 |
 68 |   ||| Apply the monad to a morphism in `cat`.
 69 |   public export %inline
 70 |   (.map) : (rec : StrongComonadR cat) -> {a,b : _} ->
 71 |            cat.hom a b -> cat.hom (rec.fun a) (rec.fun b)
 72 |   (.map) {cat=MkMonoidalR{}} (MkStrongComonadR {}) = map
 73 |
 74 |
 75 |   ||| Convert this into a `ComonadR`.
 76 |   public export %inline
 77 |   (.comonadR) : (rec : StrongComonadR cat) -> ComonadR cat.categoryR
 78 |   (.comonadR) {cat=MkMonoidalR{}} (MkStrongComonadR {} {fun}) = MkComonadR fun
 79 |
 80 |   ||| The cojoin transformation of the comonad.
 81 |   public export %inline
 82 |   (.cojoin) : (rec : StrongComonadR cat) -> {a : _} ->
 83 |               cat.hom (rec.fun a) (rec.fun (rec.fun a))
 84 |   (.cojoin) {cat=MkMonoidalR{}} (MkStrongComonadR {}) = cojoin
 85 |
 86 |   ||| The counit transformation of the comonad.
 87 |   public export %inline
 88 |   (.counit) : (rec : StrongComonadR cat) -> {a : _} ->
 89 |               cat.hom (rec.fun a) a
 90 |   (.counit) {cat=MkMonoidalR{}} (MkStrongComonadR {}) = counit
 91 |
 92 |
 93 |   ||| Convert this into a `CostrongFunctorR`.
 94 |   public export %inline
 95 |   (.costrongFunctorR) : (rec : StrongComonadR cat) -> CostrongFunctorR cat
 96 |   (.costrongFunctorR) (MkStrongComonadR {} {fun}) = MkCostrongFunctorR fun
 97 |
 98 |   ||| The left tensor costrength.
 99 |   public export %inline
100 |   (.costrongl) : (rec : StrongComonadR cat) -> {a,b : _} ->
101 |                  cat.hom (rec.fun (cat.tensor a b)) (cat.tensor a (rec.fun b))
102 |   (.costrongl) {cat=MkMonoidalR{}} (MkStrongComonadR {}) = costrongl
103 |
104 |   ||| The right tensor costrength.
105 |   public export %inline
106 |   (.costrongr) : (rec : StrongComonadR cat) -> {a,b : _} ->
107 |                  cat.hom (rec.fun (cat.tensor a b)) (cat.tensor (rec.fun a) b)
108 |   (.costrongr) {cat=MkMonoidalR{}} (MkStrongComonadR {}) = costrongr
109 |
110 |
111 |   ||| Convert this into a `StrongComonadR`.
112 |   public export %inline
113 |   (.strongComonadR) : (rec : StrongComonadR cat) -> StrongComonadR cat
114 |   (.strongComonadR) = id
115 |