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, MonSymmetric 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, MonSymmetric 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 | -- Characterization
112 | ------------------------------------------------------------
113 |
114 | ||| An expanded sum-of-products in a bimonoidal category.
115 | public export
116 | TenSOP : (add,mul : obj -> obj -> obj) -> (z,i : obj) -> List (List obj) -> obj
117 | TenSOP add mul z i = TenSeq add z . map (TenSeq mul i)
118 |
119 |
120 | ------------------------------------------------------------
121 | -- Existing Instances
122 | ------------------------------------------------------------
123 |
124 | -- These instances should not be used unless necessary, as they have
125 | -- poor runtime quantity behavior. Prefer `Typ` over base's `Morphism`
126 | -- and `Kleisli` over base's `Kleislimorphism`.
127 |
128 | public export
129 | Bimonoidal Morphism Either Pair Void () where
130 |   distribl = Mor $ \(x,y) => bimap (x,) (x,) y
131 |   distribl' = Mor $ either (mapSnd Left) (mapSnd Right)
132 |   distribr = Mor $ \(x,y) => bimap (,y) (,y) x
133 |   distribr' = Mor $ either (mapFst Left) (mapFst Right)
134 |   absorbl = Mor snd
135 |   absorbl' = Mor absurd
136 |   absorbr = Mor fst
137 |   absorbr' = Mor absurd
138 |
139 | namespace Bimonoidal
140 |   public export
141 |   [Function] Bimonoidal (~~>) Either Pair Void ()
142 |       using Monoidal.FuncPair Monoidal.FuncEither where
143 |     distribl = \(x,y) => bimap (x,) (x,) y
144 |     distribl' = either (mapSnd Left) (mapSnd Right)
145 |     distribr = \(x,y) => bimap (,y) (,y) x
146 |     distribr' = either (mapFst Left) (mapFst Right)
147 |     absorbl = snd
148 |     absorbl' = absurd
149 |     absorbr = fst
150 |     absorbr' = absurd
151 |
152 | namespace RigCategory
153 |   public export
154 |   Function : RigCategory (~~>) Either Pair Void ()
155 |   Function = (Function, FuncEither)
156 |
157 | namespace SymRigCategory
158 |   public export
159 |   Function : SymRigCategory (~~>) Either Pair Void ()
160 |   Function = (Function, FuncPair)
161 |
162 | namespace Distributive
163 |   public export
164 |   Function : Distributive (~~>) Either Pair Void ()
165 |   Function = (Function, Function, Function)
166 |
167 | public export
168 | Monad m => Bimonoidal (Kleislimorphism m) Either Pair Void () where
169 |   distribl = Kleisli $ \(x,y) => pure $ bimap (x,) (x,) y
170 |   distribl' = Kleisli $ pure . either (mapSnd Left) (mapSnd Right)
171 |   distribr = Kleisli $ \(x,y) => pure $ bimap (,y) (,y) x
172 |   distribr' = Kleisli $ pure . either (mapFst Left) (mapFst Right)
173 |   absorbl = Kleisli $ pure . snd
174 |   absorbl' = Kleisli absurd
175 |   absorbr = Kleisli $ pure . fst
176 |   absorbr' = Kleisli absurd
177 |