0 | module Control.Category.Cocartesian
  1 |
  2 | import Control.Category.Core
  3 | import Control.Category.Functor
  4 | import Control.Category.Monoidal
  5 | import Control.Category.Braided
  6 | import Data.Either
  7 | import Data.Fin
  8 | import Data.List
  9 | import Data.Morphisms
 10 |
 11 | %default total
 12 |
 13 | ------------------------------------------------------------
 14 | -- Interface
 15 | ------------------------------------------------------------
 16 |
 17 | ||| A monoidal category is *cocartesian* if its tensor product
 18 | ||| coincides with the categorical coproduct. This automatically
 19 | ||| implies that it is symmetric (see `Braided`).
 20 | |||
 21 | ||| This interface may be implemented in two equivalent ways: by giving
 22 | ||| a categorical coproduct structure (`injl`, `injr`, `coprod`) or a
 23 | ||| universal monoid structure (`merge`, `intro`). Each set of methods
 24 | ||| has a default definition in terms of the others.
 25 | |||
 26 | ||| This is the interface-style definition of a cocartesian monoidal category.
 27 | ||| For the record-style definition, see `Control.Category.Records.CocartesianR`.
 28 | |||
 29 | ||| Laws for `injl`, `injr`, `coprod`:
 30 | ||| * `coprod f g . injl = f`
 31 | ||| * `coprod f g . injr = g`
 32 | |||
 33 | ||| Laws for `merge`, `intro`:
 34 | ||| * `merge . mapl intro . unitl' = id`
 35 | ||| * `merge . mapr intro . unitr' = id`
 36 | public export
 37 | interface Monoidal cat ten i =>
 38 |     Cocartesian (0 cat : Hom obj) (ten : obj -> obj -> obj) (i : obj) | cat,ten where
 39 |   constructor MkCocartesian
 40 |   -- NOTE: If these default definitions look weird, it's because
 41 |   -- Idris's interface elaboration really doesn't like these methods,
 42 |   -- so I'm giving it as much help as possible.
 43 |
 44 |   ||| The left injection of the coproduct.
 45 |   injl : {a,b : _} -> cat a (a `ten` b)
 46 |   injl = Core.(.) {cat} (mapr' {cat,f=ten} $ intro {ten}) (unitr' {cat,ten,i})
 47 |
 48 |   ||| The right injection of the coproduct.
 49 |   injr : {a,b : _} -> cat b (a `ten` b)
 50 |   injr = Core.(.) {cat} (mapl' {cat,f=ten} $ intro {ten}) (unitl' {cat,ten,i})
 51 |
 52 |   ||| The universal property of the coproduct.
 53 |   coprod : {a,a',b : _} -> cat a b -> cat a' b -> cat (a `ten` a') b
 54 |   coprod f g = Core.(.) merge (bimap' {f=ten} f g)
 55 |
 56 |   ||| The join of the universal monoid structure.
 57 |   merge : {a : _} -> cat (a `ten` a) a
 58 |   merge = Cocartesian.coprod {ten} Core.id Core.id
 59 |
 60 |   ||| The unit of the universal monoid structure.
 61 |   intro : {a : _} -> cat i a
 62 |   intro = Core.(.) (unitl {ten}) injl
 63 |
 64 | export infixr 6 \|/
 65 |
 66 | ||| An operator synonym for `coprod`, the universal property of a
 67 | ||| cocartesian monoidal category's coproduct structure.
 68 | public export %inline %tcinline
 69 | (\|/) : {ten,i : _} -> Cocartesian cat ten i => {a,a',b : _} ->
 70 |         cat a b -> cat a' b -> cat (a `ten` a') b
 71 | (\|/) = coprod
 72 |
 73 | ||| See `PreMonoidal`.
 74 | public export
 75 | PreCocartesian : (cat : Hom obj) -> (ten : obj -> obj -> obj) -> (i : obj) -> Type
 76 | PreCocartesian = Cocartesian
 77 |
 78 |
 79 | ------------------------------------------------------------
 80 | -- Characterization
 81 | ------------------------------------------------------------
 82 |
 83 | public export
 84 | inj : Cocartesian cat ten i => {xs : _} -> (x : Fin (length xs)) -> cat (index' xs x) (TenSeq ten i xs)
 85 | inj @{c@(MkCocartesian{})} {xs=[_]} FZ = id
 86 | inj @{c@(MkCocartesian{})} {xs=[_,_]} (FS FZ) = injr
 87 | inj @{c@(MkCocartesian{})} {xs=_::_::_} FZ = injl
 88 | inj @{c@(MkCocartesian{})} {xs=_::_::_} (FS x) = injr . inj x
 89 |
 90 |
 91 | ------------------------------------------------------------
 92 | -- Existing Instances
 93 | ------------------------------------------------------------
 94 |
 95 | namespace Braided
 96 |   ||| Convert a cocartesian monoidal category into a
 97 |   ||| symmetric monoidal category.
 98 |   public export
 99 |   [FromCocartesian] {ten,i : _} -> Cocartesian cat ten i => Braided cat ten i where
100 |     braid = coprod injr injl
101 |
102 |
103 | -- These instances should not be used unless necessary, as they have
104 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
105 | -- and `Kleisli` over base's `Kleislimorphism`.
106 |
107 | public export
108 | Cocartesian Morphism Either Void where
109 |   injl = Mor Left
110 |   injr = Mor Right
111 |   coprod (Mor f) (Mor g) = Mor $ either f g
112 |   merge = Mor fromEither
113 |   intro = Mor absurd
114 |
115 | namespace Cocartesian
116 |   public export
117 |   [Function] Cocartesian (~~>) Either Void
118 |       using Braided.FuncEither where
119 |     injl = Left
120 |     injr = Right
121 |     coprod f g = either f g
122 |     merge = fromEither
123 |     intro = absurd
124 |
125 | public export
126 | Monad m => Cocartesian (Kleislimorphism m) Either Void where
127 |   injl = Kleisli $ pure . Left
128 |   injr = Kleisli $ pure . Right
129 |   coprod (Kleisli f) (Kleisli g) = Kleisli $ either f g
130 |   merge = Kleisli $ pure . fromEither
131 |   intro = Kleisli $ pure . absurd
132 |
133 |