| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Category.Monoidal.Cartesian
Contents
Description
Cartesian monoidal categories (Cartesian: tensor = product, with CopyDiscard as
superclass by Fox's theorem) and cartesian closed ones (CCC, BiCCC). Lives above
Proarrow.Category.Monoidal.CopyDiscard rather than with the products, because the superclass
points that way.
Synopsis
- class (a ** b) ~ (a && b) => TensorIsProduct (a :: k) (b :: k)
- class (HasProducts k, SymMonoidal k, Semicartesian k, CopyDiscard k, forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k
- tensorToProduct :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) => (a ** b) ~> (a && b)
- productToTensor :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) => (a && b) ~> (a ** b)
- unparRepCartesian :: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j) (a' :: k) (b' :: k). (Representable p, Cartesian k, Cartesian j, TensorIsProduct a b, TensorIsProduct a' b', Ob a, Ob b) => ((p % a) ~> a') -> ((p % b) ~> b') -> (p % (a ** b)) ~> (a' ** b')
- class (Cartesian k, Closed k) => CCC k
- class (CCC k, HasCoproducts k) => BiCCC k
- ap :: forall {j} {k} (y :: j) (a :: k) (x :: j) p. (Closed j, Cartesian k, MonoidalProfunctor p, Ob y) => p a (x ~~> y) -> p a x -> p a y
Documentation
class (a ** b) ~ (a && b) => TensorIsProduct (a :: k) (b :: k) Source Github #
Instances
| (a ** b) ~ (a && b) => TensorIsProduct (a :: k) (b :: k) Source Github # | |
Defined in Proarrow.Category.Monoidal.Cartesian | |
class (HasProducts k, SymMonoidal k, Semicartesian k, CopyDiscard k, forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k Source Github #
A cartesian monoidal category: the tensor is the product and the unit the terminal object.
By Fox's theorem this is exactly a CopyDiscard category whose copy and discard are
natural, so CopyDiscard is a superclass: every cartesian category supplies its diagonals as
comonoids, and anything asking only for copying and discarding (prisms, for instance) accepts
a cartesian category directly. The law relating the two is copy = id &&& id and
discard = terminate.
Instances
| (HasProducts k, SymMonoidal k, Semicartesian k, CopyDiscard k, forall (a :: k) (b :: k). TensorIsProduct a b) => Cartesian k Source Github # | |
Defined in Proarrow.Category.Monoidal.Cartesian | |
tensorToProduct :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) => (a ** b) ~> (a && b) Source Github #
In a cartesian category the tensor is the product (TensorIsProduct), but GHC only applies
that equation at the top of a type, never under another type family such as (, and
using the quantified form of it directly sends the solver in circles. These two identities take
the equation as an ordinary given -- discharged at the call site from the quantified superclass
of ||)Cartesian -- and let it be applied exactly where a product-typed leg meets tensor-typed
plumbing.
productToTensor :: forall {k} (a :: k) (b :: k). (HasBinaryProducts k, TensorIsProduct a b, Ob a, Ob b) => (a && b) ~> (a ** b) Source Github #
unparRepCartesian :: forall {j} {k} (p :: j +-> k) (a :: j) (b :: j) (a' :: k) (b' :: k). (Representable p, Cartesian k, Cartesian j, TensorIsProduct a b, TensorIsProduct a' b', Ob a, Ob b) => ((p % a) ~> a') -> ((p % b) ~> b') -> (p % (a ** b)) ~> (a' ** b') Source Github #
class (CCC k, HasCoproducts k) => BiCCC k Source Github #
Instances
| (CCC k, HasCoproducts k) => BiCCC k Source Github # | |
Defined in Proarrow.Category.Monoidal.Cartesian | |
ap :: forall {j} {k} (y :: j) (a :: k) (x :: j) p. (Closed j, Cartesian k, MonoidalProfunctor p, Ob y) => p a (x ~~> y) -> p a x -> p a y Source Github #
Orphan instances
| (Representable p, Cartesian j, Cartesian k) => MonoidalProfunctor (RepCostar p :: j -> k -> Type) Source Github # | Every functor between cartesian categories is oplax monoidal, |
| HasProducts k => CopyDiscard (PROD k) Source Github # | A category with products, viewed through |
| (HasProducts k, Ob a) => CocommutativeComonoid ('PR a :: PROD k) Source Github # | |
| (HasProducts k, Ob a) => Comonoid ('PR a :: PROD k) Source Github # | In a category with products every object is a comonoid via the diagonal and the terminal
map -- the natural comonoid structure that makes |