0 | module Control.Category.Bimonoidal
  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 Control.Category.Cocartesian
  8 | import Data.Morphisms
  9 |
 10 | %default total
 11 |
 12 | ------------------------------------------------------------
 13 | -- Interface
 14 | ------------------------------------------------------------
 15 |
 16 | private infixl 8 `add`
 17 | private infixl 9 `mul`
 18 |
 19 | ||| A *bimonoidal category* is a category with two monoidal structures,
 20 | ||| one additive and one multiplicative, that are compatible with each
 21 | ||| other in a similar way to elementary algebra.
 22 | |||
 23 | ||| This is the interface-style definition of a bimonoidal category.
 24 | ||| For the record-style definition, see `Control.Category.Records.BimonoidalR`.
 25 | |||
 26 | ||| As for coherence laws: they do exist, but they are so numerous as
 27 | ||| to be impractical to write here. (You wouldn't check them anyway.)
 28 | ||| If you do wish to be fully rigorous, here's a textbook on
 29 | ||| bimonoidal categories to read:
 30 | ||| * https://nilesjohnson.net/En-monoidal.html
 31 | public export
 32 | interface (Monoidal cat add z, Monoidal cat mul i) =>
 33 |     Bimonoidal (0 cat : Hom obj) (add,mul : obj -> obj -> obj) (z,i : obj) | cat,add,mul where
 34 |   constructor MkBimonoidal
 35 |   ||| The left distributor.
 36 |   distribl : {a,b,c : _} -> cat (a `mul` (b `add` c)) (a `mul` b `add` a `mul` c)
 37 |   ||| The inverse of `distribl`, the left distributor.
 38 |   distribl' : {a,b,c : _} -> cat (a `mul` b `add` a `mul` c) (a `mul` (b `add` c))
 39 |
 40 |   ||| The right distributor.
 41 |   distribr : {a,b,c : _} -> cat ((a `add` b) `mul` c) (a `mul` c `add` b `mul` c)
 42 |   ||| The inverse of `distribr`, the right distributor.
 43 |   distribr' : {a,b,c : _} -> cat (a `mul` c `add` b `mul` c) ((a `add` b) `mul` c)
 44 |
 45 |   ||| The left absorbor.
 46 |   absorbl : {a : _} -> cat (a `mul` z) z
 47 |   ||| The inverse of `absorbl`, the left absorbor.
 48 |   absorbl' : {a : _} -> cat z (a `mul` z)
 49 |
 50 |   ||| The right absorbor.
 51 |   absorbr : {a : _} -> cat (z `mul` a) z
 52 |   ||| The inverse of `absorbr`, the right absorbor.
 53 |   absorbr' : {a : _} -> cat z (z `mul` a)
 54 |
 55 | ||| A pre-bimonoidal category has a multiplicative structure that is
 56 | ||| premonoidal. See `PreMonoidal`.
 57 | public export
 58 | PreBimonoidal : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
 59 | PreBimonoidal = Bimonoidal
 60 |
 61 | ||| A rig category is a bimonoidal category whose additive structure
 62 | ||| is symmetric. The name "rig" comes from the algebraic structure
 63 | ||| the definition is based on (a ring without negatives).
 64 | |||
 65 | ||| This is the interface-style definition of a rig category. For the
 66 | ||| record-style definition, see `Control.Category.Records.RigCategoryR`.
 67 | public export
 68 | RigCategory : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
 69 | RigCategory cat add mul z i = (Bimonoidal cat add mul z i, Braided cat add z)
 70 |
 71 | ||| A pre-bimonoidal category has a multiplicative structure that is
 72 | ||| premonoidal. See `PreMonoidal`.
 73 | public export
 74 | PreRigCategory : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
 75 | PreRigCategory = RigCategory
 76 |
 77 | ||| A symmetric rig category is a bimonoidal category where both the
 78 | ||| additive and multiplicative structures are symmetric.
 79 | |||
 80 | ||| This is the interface-style definition of a symmetric rig category.
 81 | ||| For the record-style definition, see `Control.Category.Records.SymRigCategoryR`.
 82 | public export
 83 | SymRigCategory : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
 84 | SymRigCategory cat add mul z i = (RigCategory cat add mul z i, Braided cat mul i)
 85 |
 86 | ||| A pre-bimonoidal category has a multiplicative structure that is
 87 | ||| premonoidal. See `PreMonoidal`.
 88 | public export
 89 | PreSymRigCategory : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
 90 | PreSymRigCategory = SymRigCategory
 91 |
 92 | ||| A distributive category is a bimonoidal category whose
 93 | ||| multiplicative and additive structures are cartesian and
 94 | ||| cocartesian respectively.
 95 | |||
 96 | ||| This is the interface-style definition of a distributuve category.
 97 | ||| For the record-style definition, see `Control.Category.Records.DistributiveR`.
 98 | public export
 99 | Distributive : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
100 | Distributive cat add mul z i =
101 |   (SymRigCategory cat add mul z i, Cartesian cat mul i, Cocartesian cat add z)
102 |
103 | ||| A pre-bimonoidal category has a multiplicative structure that is
104 | ||| premonoidal. See `PreMonoidal`.
105 | public export
106 | PreDistributive : (cat : Hom obj) -> (add,mul : obj -> obj -> obj) -> (z,i : obj) -> Type
107 | PreDistributive = Distributive
108 |
109 |
110 | ------------------------------------------------------------
111 | -- Existing Instances
112 | ------------------------------------------------------------
113 |
114 | -- These instances should not be used unless necessary, as they have
115 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
116 | -- and `Kleisli` over base's `Kleislimorphism`.
117 |
118 | public export
119 | Bimonoidal Morphism Either Pair Void () where
120 |   distribl = Mor $ \(x,y) => bimap (x,) (x,) y
121 |   distribl' = Mor $ either (mapSnd Left) (mapSnd Right)
122 |   distribr = Mor $ \(x,y) => bimap (,y) (,y) x
123 |   distribr' = Mor $ either (mapFst Left) (mapFst Right)
124 |   absorbl = Mor snd
125 |   absorbl' = Mor absurd
126 |   absorbr = Mor fst
127 |   absorbr' = Mor absurd
128 |
129 | namespace Bimonoidal
130 |   public export
131 |   [Function] Bimonoidal (~~>) Either Pair Void ()
132 |       using Monoidal.FuncPair Monoidal.FuncEither where
133 |     distribl = \(x,y) => bimap (x,) (x,) y
134 |     distribl' = either (mapSnd Left) (mapSnd Right)
135 |     distribr = \(x,y) => bimap (,y) (,y) x
136 |     distribr' = either (mapFst Left) (mapFst Right)
137 |     absorbl = snd
138 |     absorbl' = absurd
139 |     absorbr = fst
140 |     absorbr' = absurd
141 |
142 | namespace RigCategory
143 |   public export
144 |   Function : RigCategory (~~>) Either Pair Void ()
145 |   Function = (Function, FuncEither)
146 |
147 | namespace SymRigCategory
148 |   public export
149 |   Function : SymRigCategory (~~>) Either Pair Void ()
150 |   Function = (Function, FuncPair)
151 |
152 | namespace Distributive
153 |   public export
154 |   Function : Distributive (~~>) Either Pair Void ()
155 |   Function = (Function, Function, Function)
156 |
157 | public export
158 | Monad m => Bimonoidal (Kleislimorphism m) Either Pair Void () where
159 |   distribl = Kleisli $ \(x,y) => pure $ bimap (x,) (x,) y
160 |   distribl' = Kleisli $ pure . either (mapSnd Left) (mapSnd Right)
161 |   distribr = Kleisli $ \(x,y) => pure $ bimap (,y) (,y) x
162 |   distribr' = Kleisli $ pure . either (mapFst Left) (mapFst Right)
163 |   absorbl = Kleisli $ pure . snd
164 |   absorbl' = Kleisli absurd
165 |   absorbr = Kleisli $ pure . fst
166 |   absorbr' = Kleisli absurd
167 |