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