1 | module Data.Container.Monad

 3 | import Data.Category.Functor

 5 | import Data.Container.Category

 6 | import Data.Container.Morphism.Eq

 8 | %default total

10 | public export

11 | record ContainerMonad (func : Functor Cont Cont) where

12 |   constructor MkContainerMonad

13 |   pure : (a : Container) -> a =%> func.F a

14 |   join : (a : Container) -> func.F (func.F a) =%> func.F a

15 |   0 assoc : forall a.

16 |           let 0 top : func.F (func.F (func.F a)) =%> func.F (func.F a)

17 |               top = join (func.F a)

18 |               0 left : func.F (func.F (func.F a)) =%> func.F (func.F a)

19 |               left = func.F' _ _ (join a)

20 |           in join (func.F a) ⨾ join a `DepLensEq` left ⨾ join a

22 |   0 idl : (a : Container) ->

23 |           pure (func.F a) ⨾ join a `DepLensEq` identity {a = func.F a}

24 |   0 idr : (a : Container) ->

25 |           func.F' _ _ (pure a) ⨾ (join a) `DepLensEq` identity {a = func.F a}

27 | public export

28 | record ContainerComonad (func : Functor Cont Cont) where

29 |   constructor MkContainerComonad

30 |   counit : (a : Container) -> func.F a =%> a

31 |   comult : (a : Container) -> func.F a =%> func.F (func.F a)

32 |   0 assoc : (a : Container) ->

33 |           let 0 top : func.F (func.F a) =%> func.F (func.F (func.F a))

34 |               top = comult (func.F a)

35 |               0 left : func.F (func.F a) =%> func.F (func.F (func.F a))

36 |               left = func.F' _ _ (comult a)

37 |           in comult a ⨾ left `DepLensEq` comult a ⨾ comult (func.F a)

38 |   0 id1 : (a : Container) ->

39 |              comult a ⨾ counit (func.F a) `DepLensEq` identity {a = func.F a}

40 |   0 id2 : (a : Container) ->

41 |              comult a ⨾ func.F' _ _ (counit a) `DepLensEq` identity {a = func.F a}