0 | module Data.Category.Monad
 1 |
 2 | import Data.Category
 3 | import Data.Category.NaturalTransformation
 4 | import Data.Category.Functor
 5 |
 6 | %hide Prelude.Ops.infixl.(*>)
 7 | %hide Prelude.Monad
 8 |
 9 | public export
10 | record Monad (c : Category o) where
11 |   constructor MkMonad
12 |   endo : Functor c c
13 |   η : idF c ==>> endo
14 |   μ : (endo *> endo) ==>> endo
15 |
16 |   --             F join
17 |   -- F (F (F x)) ───────> F (F x)
18 |   --    │                   │
19 |   --    │ join (F x)        │ join
20 |   --    │                   │
21 |   --    V                   V
22 |   --  F (F x)  ──────────> F x
23 |   --              join
24 |   0 square : (x : o) -> let
25 |       top : endo.F (endo.F (endo.F x)) ~> endo.F (endo.F x)
26 |       top = endo.F' _ _ (comp μ x)
27 |       bot, right : endo.F (endo.F x) ~> endo.F x
28 |       right = comp μ x
29 |       bot = comp μ x
30 |       left : endo.F (endo.F (endo.F x)) ~> endo.F (endo.F x)
31 |       left = comp μ (endo.F x)
32 |       0 arm2, arm1 : endo.F (endo.F (endo.F x)) ~> endo.F x
33 |       arm1 = (top |> right) {cat = c}
34 |       arm2 = left |> bot
35 |       in arm1 === arm2
36 |
37 |   -- identity triangles
38 |   --         η (F x)
39 |   --      F x ──> F (F x)
40 |   --       │  ╲     │
41 |   --       │   ╲    │
42 |   --   F η │    =   │ μ
43 |   --       │     ╲  │
44 |   --       V      ╲ V
45 |   --    F (F x) ──> F x
46 |   --            μ
47 |   0 identityLeft : (x : o) -> let
48 |       0 compose : endo.F x ~> endo.F x
49 |       compose = (comp η (endo.F x) |> comp μ x) {cat = c}
50 |       0 straight : endo.F x ~> endo.F x
51 |       straight = c.id (endo.F x)
52 |       in compose === straight
53 |
54 |   0 identityRight : (x : o) -> let
55 |       0 compose : endo.F x ~> endo.F x
56 |       compose = (endo.F' _ _ (comp η x) |> comp μ x) {cat = c}
57 |       0 straight : endo.F x ~> endo.F x
58 |       straight = c.id (endo.F x)
59 |       in compose === straight
60 |
61 |