Portability | non-portable (class-associated types) |
---|---|

Stability | experimental |

Maintainer | Edward Kmett <ekmett@gmail.com> |

- class (Associative k (Product k), Disassociative k (Product k), Symmetric k (Product k), Braided k (Product k)) => PreCartesian k where
- bimapProduct :: (PreCartesian k, <*> ~ Product k) => (a `k` c) -> (b `k` d) -> (a <*> b) `k` (c <*> d)
- braidProduct :: PreCartesian k => Product k a b `k` Product k b a
- associateProduct :: PreCartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)
- disassociateProduct :: PreCartesian k => Product k a (Product k b c) `k` Product k (Product k a b) c
- class (Associative k (Sum k), Disassociative k (Sum k), Symmetric k (Product k), Braided k (Sum k)) => PreCoCartesian k where
- bimapSum :: (PreCoCartesian k, Sum k ~ +) => (a `k` c) -> (b `k` d) -> (a + b) `k` (c + d)
- braidSum :: (PreCoCartesian k, + ~ Sum k) => (a + b) `k` (b + a)
- associateSum :: PreCoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)
- disassociateSum :: PreCoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) c
- class (Monoidal k (Product k), PreCartesian k) => Cartesian k
- class (Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k

# Pre-(Co)Cartesian categories

class (Associative k (Product k), Disassociative k (Product k), Symmetric k (Product k), Braided k (Product k)) => PreCartesian k whereSource

NB: This is weaker than traditional category with products! That is Cartesian, below.
The problem is `(->)`

lacks an initial object, since every type is inhabited in Haskell.
Consequently its coproduct is merely a semigroup, not a monoid (as it has no identity), and
since we want to be able to describe its dual category, which has this non-traditional
form being built over a category with an associative bifunctor rather than as a monoidal category
for the product monoid.

Minimum definition:

fst, snd, diag fst, snd, (&&&)

fst :: Product k a b `k` aSource

snd :: Product k a b `k` bSource

diag :: a `k` Product k a aSource

(&&&) :: (a `k` b) -> (a `k` c) -> a `k` Product k b cSource

PreCartesian (->) |

bimapProduct :: (PreCartesian k, <*> ~ Product k) => (a `k` c) -> (b `k` d) -> (a <*> b) `k` (c <*> d)Source

braidProduct :: PreCartesian k => Product k a b `k` Product k b aSource

associateProduct :: PreCartesian k => Product k (Product k a b) c `k` Product k a (Product k b c)Source

disassociateProduct :: PreCartesian k => Product k a (Product k b c) `k` Product k (Product k a b) cSource

class (Associative k (Sum k), Disassociative k (Sum k), Symmetric k (Product k), Braided k (Sum k)) => PreCoCartesian k whereSource

PreCoCartesian (->) |

bimapSum :: (PreCoCartesian k, Sum k ~ +) => (a `k` c) -> (b `k` d) -> (a + b) `k` (c + d)Source

braidSum :: (PreCoCartesian k, + ~ Sum k) => (a + b) `k` (b + a)Source

associateSum :: PreCoCartesian k => Sum k (Sum k a b) c `k` Sum k a (Sum k b c)Source

free construction of `Associative`

for the coproduct `Bifunctor`

`Sum k`

associateSum :: (PreCoCartesian k, (+) ~ Sum k) => ((a + b) + c) ~> (a + (b + c))

disassociateSum :: PreCoCartesian k => Sum k a (Sum k b c) `k` Sum k (Sum k a b) cSource

free construction of `Disassociative`

for the coproduct `Bifunctor`

`Sum k`

disassociateSum :: (PreCoCartesian k, (+) ~ Sum k) => (a + (b + c)) ~> ((a + b) + c)

# (Co)Cartesian categories

class (Monoidal k (Product k), PreCartesian k) => Cartesian k Source

(Monoidal k (Product k), PreCartesian k) => Cartesian k |

class (Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k Source

(Comonoidal k (Sum k), PreCoCartesian k) => CoCartesian k |