ProductCat.idr

Product of Categories

Given two categories $\mathcal{C},\mathcal{D}$, the product category combines both by having using the catesian product of objects in $\mathcal{C}$ and $\mathcal{D}$ for its set of objects, and the cartesian product of morphisms in $\mathcal{C}$ and $\mathcal{D}$ for its set of morphisms.

Definition

The product category $\mathcal{C}\times \mathcal{D}$ has

• objects $|\mathcal{C}|\ast |\mathcal{D}|$
• morphisms $\forall x,y\in \mathcal{C},z,w\in \mathcal{D}.\mathcal{C}(x,y)\times \mathcal{D}(z,w)$
• identity given by the pair of identity morphisms $i{d}_{\mathcal{C}\times \mathcal{D}}=i{d}_{\mathcal{C}}\ast i{d}_{\mathcal{D}}$
• composition given by the pair of the composition of morphisms in $\mathcal{C}$ and $\mathcal{D}$ ${;}_{\mathcal{C}\times \mathcal{D}}={;}_{\mathcal{C}}\ast {;}_{\mathcal{D}}$

In this definition $\ast$ is the cartesian product in $\mathcal{S}et$ and $\times$ is the product of categories. We reproduce this convention in Idris.

(×) : Category o -> Category p -> Category (o * p)
(×) x y = MkCategory
  (\a, b => ((~:>) x a.π1 b.π1) * ((~:>) y a.π2 b.π2))
  (\v => x.id v.π1 && y.id v.π2)
  (\f, g => (|:>) x f.π1 g.π1 && (|:>) y f.π2 g.π2)
  (\_, _, idl => cong2 (&&)
      (x.idRight _ _ idl.π1)
      (y.idRight _ _ idl.π2) `trans` Data.Product.projIdentity idl
  )
  (\_, _, idr => cong2 (&&)
      (x.idLeft  _ _ idr.π1)
      (y.idLeft  _ _ idr.π2) `trans` Data.Product.projIdentity idr
  )
  (\_, _, _, _, f, g, h => cong2 (&&)
      (compAssoc x _ _ _ _ f.π1 g.π1 h.π1)
      (compAssoc y _ _ _ _ f.π2 g.π2 h.π2)
  )