Product.idr

Cartesian Product

The cartesian product of container is distinct from the tensor product in that the responses are combined with a coproduct, rather than a product.

Definition

$(A,\bar{A})\ast (B,\bar{B})=((a,b):A\ast B,\bar{A}(a)+\bar{B}(b))$

(*) : (c1, c2 : Container) -> Container
(*) c1 c2 = (x : c1.req * c2.req) !> c1.res x.π1 + c2.res x.π2

The product is also a bifunctor using both the fact that both the product and the coproduct on types are bifunctors. That is why in the implementation of (~*~), we see bimap appear twice, but the first one operates on (*) : Type -> Type -> Type and the second one operates on (+) : Type -> Type -> Type.

Proposition

The cartesian product forms a bifuctor in $\mathcal{C}ont$

(~*~) : a =%> a' -> b =%> b' -> a * b =%> a' * b'
(~*~) m1 m2 =
    (bimap m1.fwd m2.fwd) <!
    (\x => bimap (m1.bwd x.π1) (m2.bwd x.π2))

Building the proof that the cartesian product is a bifunctor in $\mathcal{C}ont$ is easy but it must be done in order to implement more interesting structures.

public export
ProductBifunctor : Bifunctor Cont Cont Cont
ProductBifunctor = MkFunctor
    (uncurry (*))
    (\_, _ => uncurry (~*~))
    (\(x && y) => depLensEqToEq $ MkDepLensEq
        (\z => projIdentity z)
        (\z => bifunctorId')
    )
    (\(x1 && x2), (y1 && y2), (z1 && z2), (m1 && m2), (n1 && n2) =>
      depLensEqToEq $ MkDepLensEq
        (\(vx && vy) => Refl)
        (\(vz && vy), vz => bimapCompose vz)
    )

In particular, it gives us projection maps.

Proposition

We can map out of a product by projecting forward and injecting backward.

proj1 : {0 c1, c2 : Container} -> (c1 * c2) =%> c1
proj1 = π1 <! (\x => (<+))
 
proj2 : {0 c1, c2 : Container} -> (c1 * c2) =%> c2
proj2 = π2 <! (\x => (+>))

Additionally, given two morphisms with the same domain, we can build products

Proposition

There is a universal map $(c\to a)\times (c\to b)\to c\to a\ast b$.

contProd : c =%> a -> c =%> b -> c =%> a * b
contProd x y = (\v => x.fwd v && y.fwd v) <!
               (\v => choice (x.bwd v) (y.bwd v))

This map is the universal property of products, fact we can prove here.

Proposition

The category of containers has products via $(\ast )$.

ContProd : HasProduct Cont
ContProd = MkProd
  (*)
  proj1
  proj2
  contProd
  (\(m1 <! m1'), m2 => Refl)
  (\m1, (m2 <! m2') => Refl)
  contProdUniq

Additionally, the cartesian product provides a monoidal structure in $\mathcal{C}ont$

Proposition

$\mathcal{C}ont$ is monoidal in $(\ast )$ with $1$ as the neutral.

public export
CartesianMonoidal : Monoidal Cont
CartesianMonoidal = MkMonoidal
    ProductBifunctor
    One
    alpha
    leftUnitor
    rightUnitor