0 | ||| This module defines a co-Kleisli category construction on an
  1 | ||| arbitrary comonad in an arbitrary premonoidal category.
  2 | module Control.Category.Instances.Cokleisli
  3 |
  4 | import Control.Category
  5 | import Control.Category.Records
  6 | import Data.Wrap0
  7 |
  8 | %default total
  9 |
 10 | ||| The co-Kleisli category of a category `cat` with comonad `w`. This
 11 | ||| forms another category with the same objects. In addition, if
 12 | ||| `cat` is a premonoidal category and `w` has tensorial costrength,
 13 | ||| then this category inherits its premonoidal structure.
 14 | ||| (Note that this is NOT the case for monoidal structure.)
 15 | public export
 16 | record Cokleisli (cat : Hom obj) (w : obj -> obj) (a,b : obj) where
 17 |   constructor MkCokleisli
 18 |   runCokleisli : cat (w a) b
 19 |
 20 |
 21 | ------------------------------------------------------------
 22 | -- Interface Style
 23 | ------------------------------------------------------------
 24 |
 25 | public export
 26 | {w : _} -> Category cat => CatComonad cat w => Category (Cokleisli cat w) where
 27 |   id = MkCokleisli counit
 28 |   MkCokleisli f . MkCokleisli g = MkCokleisli (f . map g . cojoin)
 29 |
 30 | public export
 31 | [CokleisliInj] {w : _} -> Category cat => CatComonad cat w => CatFunctor cat (Cokleisli cat w) Prelude.id where
 32 |   map f = MkCokleisli $ f . counit
 33 |
 34 | public export
 35 | {w : _} -> Promonad0 cat => CatComonad cat w => Promonad0 (Cokleisli cat w) where
 36 |   fromFuncW f = MkCokleisli (fromFuncW f . counit)
 37 |
 38 | ||| WARNING: This is typically a binoidal functor, not a true bifunctor.
 39 | ||| It is only a bifunctor if the comonad `m` is commutative over `ten`.
 40 | public export %hint
 41 | CokleisliBinoidal : {ten,w : _} -> Category cat => StrongComonad cat ten w =>
 42 |                     EndoBinoidal cat ten => EndoBinoidal (Cokleisli cat w) ten
 43 | CokleisliBinoidal = Impl
 44 |   where
 45 |     [Impl] CatBifunctor (Cokleisli cat w) (Cokleisli cat w) (Cokleisli cat w) ten where
 46 |       bimap (MkCokleisli f) (MkCokleisli g) =
 47 |         MkCokleisli (mapr' g . costrongl) . -- mapr
 48 |         MkCokleisli (mapl' f . costrongr)   -- mapl
 49 |
 50 | ||| WARNING: This is typically a premonoidal category, not truly monoidal.
 51 | ||| It is only monoidal if the comonad `m` is commutative over `ten`.
 52 | public export %hint
 53 | CokleisliPreMonoidal : {w,ten,i : _} -> PreMonoidal cat ten i => StrongComonad cat ten w =>
 54 |                        PreMonoidal (Cokleisli cat w) ten i
 55 | CokleisliPreMonoidal =
 56 |   MkMonoidal (MkCokleisli $ assoc . counit)
 57 |              (MkCokleisli $ assoc' . counit)
 58 |              (MkCokleisli $ unitl . counit)
 59 |              (MkCokleisli $ unitl' . counit)
 60 |              (MkCokleisli $ unitr . counit)
 61 |              (MkCokleisli $ unitr' . counit)
 62 |
 63 | public export %hint
 64 | CokleisliPreBraided : {w,ten,i : _} -> PreBraided cat ten i => StrongComonad cat ten w =>
 65 |                       PreBraided (Cokleisli cat w) ten i
 66 | CokleisliPreBraided =
 67 |   MkBraided (MkCokleisli $ braid . counit)
 68 |             (MkCokleisli $ braid' . counit)
 69 |
 70 | public export %hint
 71 | CokleisliPreSymmetric : {w,ten,i : _} -> PreSymmetric cat ten i => StrongComonad cat ten w =>
 72 |                         PreSymmetric (Cokleisli cat w) ten i
 73 | CokleisliPreSymmetric =
 74 |   MkMonSymmetric (\p => MkCokleisli $ Core.(.) (permute p) counit)
 75 |
 76 | public export %hint
 77 | CokleisliPreCartesian : {w,ten,i : _} -> PreCartesian cat ten i => StrongComonad cat ten w =>
 78 |                         PreCartesian (Cokleisli cat w) ten i
 79 | CokleisliPreCartesian =
 80 |   MkCartesian (MkCokleisli $ projl . counit)
 81 |               (MkCokleisli $ projr . counit)
 82 |               (\f,g => bimap' f g . (MkCokleisli $ split . counit))
 83 |               (MkCokleisli $ split . counit)
 84 |               (MkCokleisli $ elim {ten} . counit)
 85 |
 86 | public export %hint
 87 | CokleisliPreCocartesian : {w,ten,i : _} -> PreCocartesian cat ten i => StrongComonad cat ten w =>
 88 |                           PreCocartesian (Cokleisli cat w) ten i
 89 | CokleisliPreCocartesian =
 90 |   MkCocartesian (MkCokleisli $ injl . counit)
 91 |                 (MkCokleisli $ injr . counit)
 92 |                 (\f,g => (MkCokleisli $ merge . counit) . bimap' f g)
 93 |                 (MkCokleisli $ merge . counit)
 94 |                 (MkCokleisli $ intro {ten} . counit)
 95 |
 96 | public export %hint
 97 | CokleisliPreBimonoidal : {w,add,mul,z,i : _} -> PreBimonoidal cat add mul z i =>
 98 |                          (StrongComonad cat add w, StrongComonad cat mul w) =>
 99 |                          PreBimonoidal (Cokleisli cat w) add mul z i
100 | CokleisliPreBimonoidal @{_} @{(c@(impl,_),_)} =
101 |   MkBimonoidal (MkCokleisli $ distribl . counit @{impl})
102 |                (MkCokleisli $ distribl' . counit @{impl})
103 |                (MkCokleisli $ distribr . counit @{impl})
104 |                (MkCokleisli $ distribr' . counit @{impl})
105 |                (MkCokleisli $ absorbl {add,mul} . counit @{impl})
106 |                (MkCokleisli $ absorbl' {add,mul} . counit @{impl})
107 |                (MkCokleisli $ absorbr {add,mul} . counit @{impl})
108 |                (MkCokleisli $ absorbr' {add,mul} . counit @{impl})
109 |
110 |
111 | ------------------------------------------------------------
112 | -- Record Style
113 | ------------------------------------------------------------
114 |
115 | namespace CategoryR
116 |   public export
117 |   Cokleisli : (cat : CategoryR) -> (w : ComonadR cat) -> CategoryR
118 |   Cokleisli (MkCategoryR cat) (MkComonadR w) = MkCategoryR (Cokleisli cat w)
119 |
120 | namespace FunctorR
121 |   public export
122 |   CokleisliInj : {cat,w : _} -> FunctorR cat (Cokleisli cat w)
123 |   CokleisliInj {cat=MkCategoryR{}} {w=MkComonadR{}} = MkFunctorR Prelude.id {impl = CokleisliInj}
124 |
125 | namespace MonoidalR
126 |   public export
127 |   Cokleisli : (cat : PreMonoidalR) -> (w : StrongComonadR cat) -> PreMonoidalR
128 |   Cokleisli (MkMonoidalR cat ten i) (MkStrongComonadR w) = MkMonoidalR (Cokleisli cat w) ten i
129 |
130 | namespace BraidedR
131 |   public export
132 |   Cokleisli : (cat : PreBraidedR) -> (w : StrongComonadR cat.monoidalR) -> PreBraidedR
133 |   Cokleisli (MkBraidedR cat ten i) (MkStrongComonadR w) = MkBraidedR (Cokleisli cat w) ten i
134 |
135 | namespace SymmetricR
136 |   public export
137 |   Cokleisli : (cat : PreSymmetricR) -> (w : StrongComonadR cat.monoidalR) -> PreSymmetricR
138 |   Cokleisli (MkSymmetricR cat ten i) (MkStrongComonadR w) = MkSymmetricR (Cokleisli cat w) ten i
139 |
140 | namespace CartesianR
141 |   public export
142 |   Cokleisli : (cat : PreCartesianR) -> (w : StrongComonadR cat.monoidalR) -> PreCartesianR
143 |   Cokleisli (MkCartesianR cat ten i) (MkStrongComonadR w) = MkCartesianR (Cokleisli cat w) ten i
144 |
145 | namespace CocartesianR
146 |   public export
147 |   Cokleisli : (cat : PreCocartesianR) -> (w : StrongComonadR cat.monoidalR) -> PreCocartesianR
148 |   Cokleisli (MkCocartesianR cat ten i) (MkStrongComonadR w) = MkCocartesianR (Cokleisli cat w) ten i
149 |