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

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

ProductsπŸ”—

The product PP of two objects AA and BB, if it exists, is the smallest object equipped with β€œprojection” maps Pβ†’AP \to A and Pβ†’BP \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 A∧BA \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 A←AΓ—Bβ†’BA \ot A \times B \to B to be a product diagram, it must be able to cough up an arrow Qβ†’PQ \to P given the data of another span A←Qβ†’BA \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:Qβ†’Af : Q \to A and g:Qβ†’Bg : 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
  field
    ⟨_,_⟩     : βˆ€ {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
  no-eta-equality
  field
    apex : Ob
    π₁ : Hom apex A
    Ο€β‚‚ : Hom apex B
    has-is-product : is-product π₁ Ο€β‚‚

  open is-product has-is-product public

open Product hiding (⟨_,_⟩ ; π₁ ; Ο€β‚‚ ; ⟨⟩∘)

UniquenessπŸ”—

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

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

We construct the map P→P′P \to P' as the pairing of the projections from PP, and symmetrically for P′→PP' \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
  where
    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 =
      p2.uniqueβ‚‚
        (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 =
      p1.uniqueβ‚‚
        (assoc _ _ _ Β·Β· ap (_∘ _) p1.Ο€β‚βˆ˜factor Β·Β· p2.Ο€β‚βˆ˜factor)
        (assoc _ _ _ Β·Β· ap (_∘ _) p1.Ο€β‚‚βˆ˜factor Β·Β· p2.Ο€β‚‚βˆ˜factor)
        (idr _) (idr _)

is-product-iso
  : βˆ€ {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 Γ—αΆœ 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