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 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 \leftarrow 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 \leftarrow 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
    ⟨_,_⟩     : βˆ€ {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)

  ⟨⟩-Ξ· : ⟨ π₁ , Ο€β‚‚ ⟩ ≑ id
  ⟨⟩-η = sym $ unique id (idr _) (idr _)

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


Products, when they exist, are unique. It’s easiest to see this with a diagrammatic argument: If we have product diagrams A←Pβ†’BA \leftarrow P \to B and A←Pβ€²β†’BA \leftarrow 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
      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)))

Categories with all binary productsπŸ”—

Categories with all binary products are quite common, so we define a module for working with them.

has-products : Type _
has-products = βˆ€ a b β†’ Product a b

module Binary-products (all-products : has-products) where

  module product {a} {b} = Product (all-products a b)

  open product renaming
    (unique to ⟨⟩-unique; Ο€β‚βˆ˜factor to Ο€β‚βˆ˜βŸ¨βŸ©; Ο€β‚‚βˆ˜factor to Ο€β‚‚βˆ˜βŸ¨βŸ©) public
  open Functor

  infixr 7 _βŠ—β‚€_
  infix 50 _βŠ—β‚_

We start by defining a β€œglobal” product-assigning operation.

  _βŠ—β‚€_ : Ob β†’ Ob β†’ Ob
  a βŠ—β‚€ b = product.apex {a} {b}

This operation extends to a bifunctor C×C→C\mathcal{C} \times \mathcal{C} \to \mathcal{C}.

  _βŠ—β‚_ : βˆ€ {a b x y} β†’ Hom a x β†’ Hom b y β†’ Hom (a βŠ—β‚€ b) (x βŠ—β‚€ y)
  f βŠ—β‚ g = ⟨ f ∘ π₁ , g ∘ Ο€β‚‚ ⟩

  Γ—-functor : Functor (C Γ—αΆœ C) C
  Γ—-functor .Fβ‚€ (a , b) = a βŠ—β‚€ b
  Γ—-functor .F₁ (f , g) = f βŠ—β‚ g
  Γ—-functor .F-id = sym $ ⟨⟩-unique id id-comm id-comm
  Γ—-functor .F-∘ (f , g) (h , i) =
    sym $ ⟨⟩-unique (f βŠ—β‚ g ∘ h βŠ—β‚ i)
      (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ extendr Ο€β‚βˆ˜βŸ¨βŸ©)
      (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ extendr Ο€β‚‚βˆ˜βŸ¨βŸ©)

We also define a handful of common morphisms.

  Ξ΄ : Hom a (a βŠ—β‚€ a)
  δ = ⟨ id , id ⟩

  swap : Hom (a βŠ—β‚€ b) (b βŠ—β‚€ a)
  swap = ⟨ Ο€β‚‚ , π₁ ⟩
  swap-is-iso : βˆ€ {a b} β†’ is-invertible (swap {a} {b})
  swap-is-iso = make-invertible swap
    (uniqueβ‚‚ (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©) ((pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚βˆ˜βŸ¨βŸ©)) (idr _) (idr _))
    (uniqueβ‚‚ (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©) ((pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ Ο€β‚βˆ˜βŸ¨βŸ©)) (idr _) (idr _))

  by-π₁ : βˆ€ {f f' : Hom a b} {g g' : Hom a c} β†’ ⟨ f , g ⟩ ≑ ⟨ f' , g' ⟩ β†’ f ≑ f'
  by-π₁ p = sym Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ ap (π₁ ∘_) p βˆ™ Ο€β‚βˆ˜βŸ¨βŸ©

  extend-π₁ : βˆ€ {f : Hom a b} {g : Hom a c} {h} β†’ ⟨ f , g ⟩ ≑ h β†’ f ≑ π₁ ∘ h
  extend-π₁ p = sym Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ ap (π₁ ∘_) p

  by-Ο€β‚‚ : βˆ€ {f f' : Hom a b} {g g' : Hom a c} β†’ ⟨ f , g ⟩ ≑ ⟨ f' , g' ⟩ β†’ g ≑ g'
  by-Ο€β‚‚ p = sym Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ ap (Ο€β‚‚ ∘_) p βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©

  extend-Ο€β‚‚ : βˆ€ {f : Hom a b} {g : Hom a c} {h} β†’ ⟨ f , g ⟩ ≑ h β†’ g ≑ Ο€β‚‚ ∘ h
  extend-Ο€β‚‚ p = sym Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ ap (Ο€β‚‚ ∘_) p

    : βˆ€ {f : Hom (a βŠ—β‚€ b) c} {g : Hom (a βŠ—β‚€ b) d}
    β†’ (⟨⟩-inv : is-invertible ⟨ f , g ⟩)
    β†’ f ∘ is-invertible.inv ⟨⟩-inv ≑ π₁
  π₁-inv {f = f} {g = g} ⟨⟩-inv =
    pushl (sym Ο€β‚βˆ˜βŸ¨βŸ©) βˆ™ elimr (is-invertible.invl ⟨⟩-inv)

    : βˆ€ {f : Hom (a βŠ—β‚€ b) c} {g : Hom (a βŠ—β‚€ b) d}
    β†’ (⟨⟩-inv : is-invertible ⟨ f , g ⟩)
    β†’ g ∘ is-invertible.inv ⟨⟩-inv ≑ Ο€β‚‚
  Ο€β‚‚-inv {f = f} {g = g} ⟨⟩-inv =
    pushl (sym Ο€β‚‚βˆ˜βŸ¨βŸ©) βˆ™ elimr (is-invertible.invl ⟨⟩-inv)

Representability of productsπŸ”—

The collection of maps into a product aΓ—ba \times b is equivalent to the collection of pairs of maps into aa and bb. The forward direction of the equivalence is given by postcomposition of the projections, and the reverse direction by the universal property of products.

  : βˆ€ {a b}
  β†’ (prod : Product a b)
  β†’ (x : Ob)
  β†’ Hom x (Product.apex prod) ≃ (Hom x a Γ— Hom x b)
product-repr prod x = Iso→Equiv λ where
    .fst f β†’ π₁ ∘ f , Ο€β‚‚ ∘ f
    .snd .is-iso.inv (f , g) β†’ ⟨ f , g ⟩
    .snd .is-iso.rinv (f , g) β†’ Ο€β‚βˆ˜factor ,β‚š Ο€β‚‚βˆ˜factor
    .snd .is-iso.linv f β†’ sym (⟨⟩∘ f) βˆ™ eliml ⟨⟩-Ξ·
  where open Product prod