module Cat.Diagram.Product where


The product of two objects and if it exists, is the smallest object equipped with β€œprojection” maps and This situation can be visualised by putting the data of a product into a commutative diagram, as the one below: To express that is the smallest object with projections to and we ask that any other object with projections through and factors uniquely through

In the sense that (univalent) categories generalise posets, the product of and β€” if it exists β€” generalises the binary meet Since products are unique when they exist, we may safely denote any product of and by

For a diagram to be a product diagram, it must be able to cough up an arrow given the data of another span 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 and since in the special case where is the terminal object (hence the two arrows are global elements of resp. the pairing is a global element of the product

  record is-product {A B P} (π₁ : Hom P A) (Ο€β‚‚ : Hom P B) : Type (o βŠ” β„“) 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 and is an explicit choice of product diagram:

  record Product (A B : Ob) : Type (o βŠ” β„“) 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 and we can fit them into a β€œcommutative diamond” like the one below:

Since both and are products, we know that the dashed arrows in the diagram below exist, so the overall diagram commutes: hence we have an isomorphism

We construct the map as the pairing of the projections from and symmetrically for

  Γ—-Unique : (p1 p2 : Product C 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 C π₁ Ο€β‚‚
    β†’ is-product C (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 : βˆ€ {o β„“} β†’ Precategory o β„“ β†’ Type _
has-products C = βˆ€ a b β†’ Product C a b

module Binary-products
  {o β„“}
  (C : Precategory o β„“)
  (all-products : has-products C)
  open Cat.Reasoning C
  private variable
    A B a b c d : Ob

  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

  _βŠ—β‚_ : βˆ€ {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 is equivalent to the collection of pairs of maps into and 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 C 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