open import Cat.Instances.Product
open import Cat.Prelude

module Cat.Diagram.Product {o h} (C : Precategory o h) where


The product PP of two objects AA and BB, if it exists, is the smallest object equipped with “projection” maps PAP \to A and PBP \to B. This situation can be visualised by putting the data of a product into a commutative diagram, as the one below: To express that PP is the smallest object with projections to AA and BB, we ask that any other object QQ with projections through AA and BB factors uniquely through PP:

In the sense that (univalent) categories generalise posets, the product of AA and BB — if it exists — generalises the binary meet ABA \wedge B. Since products are unique when they exist, we may safely denote any product of AA and BB by A×BA \times B.

For a diagram AA×BBA \ot A \times B \to B to be a product diagram, it must be able to cough up an arrow QPQ \to P given the data of another span AQBA \ot Q \to B, which must not only fit into the diagram above but be unique among the arrows that do so.

This factoring is called the pairing of the arrows f:QAf : Q \to A and g:QBg : Q \to B, since in the special case where QQ is the terminal object (hence the two arrows are global elements of AA resp. BB), the pairing f,g\langle f, g \rangle is a global element of the product A×BA \times B.

record is-product {A B P} (π₁ : Hom P A) (π₂ : Hom P B) : Type (o  h) where
    ⟨_,_⟩     :  {Q} (p1 : Hom Q A) (p2 : Hom Q B)  Hom Q P
    π₁∘factor :  {Q} {p1 : Hom Q _} {p2}  π₁   p1 , p2   p1
    π₂∘factor :  {Q} {p1 : Hom Q _} {p2}  π₂   p1 , p2   p2

    unique :  {Q} {p1 : Hom Q A} {p2}
            (other : Hom Q P)
            π₁  other  p1
            π₂  other  p2
            other   p1 , p2 

  unique₂ :  {Q} {pr1 : Hom Q A} {pr2}
            {o1} (p1 : π₁  o1  pr1) (q1 : π₂  o1  pr2)
            {o2} (p2 : π₁  o2  pr1) (q2 : π₂  o2  pr2)
           o1  o2
  unique₂ p1 q1 p2 q2 = unique _ p1 q1  sym (unique _ p2 q2)

  ⟨⟩∘ :  {Q R} {p1 : Hom Q A} {p2 : Hom Q B} (f : Hom R Q)
        p1 , p2   f   p1  f , p2  f 
  ⟨⟩∘ f = unique _ (pulll π₁∘factor) (pulll π₂∘factor)

A product of AA and BB is an explicit choice of product diagram:

record Product (A B : Ob) : Type (o  h) where
    apex : Ob
    π₁ : Hom apex A
    π₂ : Hom apex B
    has-is-product : is-product π₁ π₂

  open is-product has-is-product public

open Product hiding (⟨_,_⟩ ; π₁ ; π₂ ; ⟨⟩∘)


Products, when they exist, are unique. It’s easiest to see this with a diagrammatic argument: If we have product diagrams APBA \ot P \to B and APBA \ot P' \to B, we can fit them into a “commutative diamond” like the one below:

Since both PP and PP' are products, we know that the dashed arrows in the diagram below exist, so the overall diagram commutes: hence we have an isomorphism PPP \cong P'.

We construct the map PPP \to P' as the pairing of the projections from PP, and symmetrically for PPP' \to P.

×-Unique : (p1 p2 : Product A B)  apex p1  apex p2
×-Unique p1 p2 = make-iso p1→p2 p2→p1 p1→p2→p1 p2→p1→p2
    module p1 = Product p1
    module p2 = Product p2

    p1→p2 : Hom (apex p1) (apex p2)
    p1→p2 = p2.⟨ p1.π₁ , p1.π₂ p2.

    p2→p1 : Hom (apex p2) (apex p1)
    p2→p1 = p1.⟨ p2.π₁ , p2.π₂ p1.

These are unique because they are maps into products which commute with the projections.

    p1→p2→p1 : p1→p2  p2→p1  id
    p1→p2→p1 =
        (assoc _ _ _ ·· ap (_∘ _) p2.π₁∘factor ·· p1.π₁∘factor)
        (assoc _ _ _ ·· ap (_∘ _) p2.π₂∘factor ·· p1.π₂∘factor)
        (idr _) (idr _)

    p2→p1→p2 : p2→p1  p1→p2  id
    p2→p1→p2 =
        (assoc _ _ _ ·· ap (_∘ _) p1.π₁∘factor ·· p2.π₁∘factor)
        (assoc _ _ _ ·· ap (_∘ _) p1.π₂∘factor ·· p2.π₂∘factor)
        (idr _) (idr _)

  :  {A A′ B B′ P} {π₁ : Hom P A} {π₂ : Hom P B}
      {f : Hom A A′} {g : Hom B B′}
   is-invertible f
   is-invertible g
   is-product π₁ π₂
   is-product (f  π₁) (g  π₂)
is-product-iso f-iso g-iso prod = prod′ where
  module fi = is-invertible f-iso
  module gi = is-invertible g-iso

  open is-product
  prod′ : is-product _ _
  prod′ .⟨_,_⟩ qa qb = prod .⟨_,_⟩ (fi.inv  qa) (gi.inv  qb)
  prod′ .π₁∘factor = pullr (prod .π₁∘factor)  cancell fi.invl
  prod′ .π₂∘factor = pullr (prod .π₂∘factor)  cancell gi.invl
  prod′ .unique other p q = prod .unique other
    (sym (ap (_ ∘_) (sym p)  pulll (cancell fi.invr)))
    (sym (ap (_ ∘_) (sym q)  pulll (cancell gi.invr)))

The product functor🔗

If C\ca{C} admits products of all pairs of objects, then the assignment (A,B)(A×B)(A, B) \mapsto (A \times B) extends to a bifunctor (C×C)C(\ca{C} \times \ca{C}) \to \ca{C}.

module Cartesian (hasprods :  A B  Product A B) where
  open Functor

  ×-functor : Functor (C ×Cat C) C
  ×-functor .F₀ (A , B) = hasprods A B .apex
  ×-functor .F₁ {a , x} {b , y} (f , g) =
    hasprods b y .has-is-product .is-product.⟨_,_⟩
      (f  hasprods a x .Product.π₁) (g  hasprods a x .Product.π₂)

  ×-functor .F-id {a , b} =
    unique₂ (hasprods a b)
      (hasprods a b .π₁∘factor)
      (hasprods a b .π₂∘factor)
      id-comm id-comm

  ×-functor .F-∘ {a , b} {c , d} {e , f} x y =
    unique₂ (hasprods e f)
      (hasprods e f .π₁∘factor)
      (hasprods e f .π₂∘factor)
      (  pulll (hasprods e f .π₁∘factor)
      ·· pullr (hasprods c d .π₁∘factor)
      ·· assoc _ _ _)
      (  pulll (hasprods e f .π₂∘factor)
      ·· pullr (hasprods c d .π₂∘factor)
      ·· assoc _ _ _)

We refer to a category admitting all binary products as cartesian. When working with products, a Cartesian category is the place to be, since we can work with the “canonical” product operations — rather than requiring different product data for any pair of objects we need a product for.

Here we extract the data of the “global” product-assigning operation to separate top-level definitions:

  _⊗_ : Ob  Ob  Ob
  A  B = F₀ ×-functor (A , B)

  ⟨_,_⟩ : Hom a b  Hom a c  Hom a (b  c)
   f , g  = hasprods _ _ .has-is-product .is-product.⟨_,_⟩ f g

  π₁ : Hom (a  b) a
  π₁ = hasprods _ _ .Product.π₁

  π₂ : Hom (a  b) b
  π₂ = hasprods _ _ .Product.π₂

  π₁∘⟨⟩ : {f : Hom a b} {g : Hom a c}  π₁   f , g   f
  π₁∘⟨⟩ = hasprods _ _ .has-is-product .is-product.π₁∘factor

  π₂∘⟨⟩ : {f : Hom a b} {g : Hom a c}  π₂   f , g   g
  π₂∘⟨⟩ = hasprods _ _ .has-is-product .is-product.π₂∘factor

  ⟨⟩∘ :  {Q R} {p1 : Hom Q a} {p2 : Hom Q b} (f : Hom R Q)
        p1 , p2   f   p1  f , p2  f 
  ⟨⟩∘ f = is-product.⟨⟩∘ (hasprods _ _ .has-is-product) f