module Cat.Diagram.Product.Finite
  {o β„“} {C : Precategory o β„“}
  (terminal : Terminal C)
  (products : βˆ€ A B β†’ Product C A B)

Computing finite productsπŸ”—

Throughout the 1lab, we have referred to categories having a terminal object and binary products as Cartesian categories, finite products categories, and other terms like these. But, a priori, there is no reason to believe that this implies all finite products exist, right? Right β€” which is why we have to prove it.

In this module, we prove the following theorem: If you have a sequence of objects in C\mathcal{C} of length nn, then its product exists as long as C\mathcal{C} is Cartesian, and can be computed in terms of iterated binary products and terminal objects.

We take an opportunity to complicate the definition while we’re at it: Instead of computing the product of a one-object sequence to be AΓ—βŠ€A \times \top, we simply let it be AA. This extra case translates to an extra case in all the proofs, but fortunately it does not complicate anything too far.

Cartesianβ†’standard-finite-products : βˆ€ {n} β†’ (F : Fin n β†’ Ob) β†’ Indexed-product C F
Cartesian→standard-finite-products F = prod where
  F-apex : βˆ€ {n} β†’ (F : Fin n β†’ Ob) β†’ Ob
  F-apex {zero} F        = terminal .top
  F-apex {suc zero} F    = F fzero
  F-apex {suc (suc n)} F = F fzero βŠ—β‚€ F-apex (Ξ» e β†’ F (fsuc e))

  F-pi : βˆ€ {n} (F : Fin n β†’ Ob) (i : Fin n) β†’ Hom (F-apex F) (F i)
  F-pi {suc zero} F fzero       = id
  F-pi {suc (suc n)} F fzero    = Cart.π₁
  F-pi {suc (suc n)} F (fsuc i) = F-pi (Ξ» e β†’ F (fsuc e)) i ∘ Cart.Ο€β‚‚

  F-mult : βˆ€ {Y} {n} (F : Fin n β†’ Ob)
         β†’ ((i : Fin n) β†’ Hom Y (F i)) β†’ Hom Y (F-apex F)
  F-mult {n = zero} F maps = ! terminal
  F-mult {n = suc zero} F maps = maps fzero
  F-mult {n = suc (suc n)} F maps = Cart.⟨ maps fzero , F-mult (Ξ» z β†’ F (fsuc z)) (Ξ» i β†’ maps (fsuc i)) ⟩Cart.

  F-commute : βˆ€ {Y} {n} (F : Fin n β†’ Ob) (f : (i : Fin n) β†’ Hom Y (F i))
            β†’ βˆ€ i β†’ F-pi F i ∘ F-mult F f ≑ f i
  F-commute {n = suc zero} F f fzero = idl (f fzero)
  F-commute {n = suc (suc n)} F f fzero = Cart.Ο€β‚βˆ˜βŸ¨βŸ©
  F-commute {n = suc (suc n)} F f (fsuc i) = pullr Cart.Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ F-commute (Ξ» e β†’ F (fsuc e)) (Ξ» e β†’ f (fsuc e)) i

    : βˆ€ {Y} {n} (F : Fin n β†’ Ob) (f : (i : Fin n) β†’ Hom Y (F i))
    β†’ {h : Hom Y (F-apex F)} β†’ ((i : Fin n) β†’ F-pi F i ∘ h ≑ f i)
    β†’ h ≑ F-mult F f
  F-unique {n = zero} F f {h} p = sym $ !-unique terminal _
  F-unique {n = suc zero} F f {h} p = sym (idl h) βˆ™ p fzero
  F-unique {n = suc (suc n)} F f {h} p =
    products _ _ .unique h (p fzero)
      (F-unique (Ξ» e β†’ F (fsuc e)) (Ξ» i β†’ f (fsuc i))
        Ξ» i β†’ assoc _ _ _ βˆ™ p (fsuc i))

  prod : Indexed-product C F
  prod .Ξ F = F-apex F
  prod .Ο€  = F-pi F
  prod .has-is-ip .tuple      = F-mult F
  prod .has-is-ip .commute    = F-commute F _ _
  prod .has-is-ip .unique f p = F-unique F f p

If, in addition, C\mathcal{C} is univalent, then we can strengthen this result to work with all finite types, not just the standard [n][n] types.

To see why univalence is required, remember that finite types are merely equivalent to [n][n], so any two enumerations should yield the same result. But two different permutations of the objects in a diagram would only yield isomorphic products in general; we need them to be equal, which is what univalence ensures.

  : is-category C
  β†’ βˆ€ {β„“} {X : Type β„“} β†’ Finite X
  β†’ has-products-indexed-by C X
Cartesian→finite-products cat {X = X} (fin {n} e) F =
  βˆ₯-βˆ₯-rec (Indexed-product-unique C _ cat) go e
    go : X ≃ Fin n β†’ Indexed-product C F
    go e = Indexed-product-≃ C e
      (Cartesianβ†’standard-finite-products (F βŠ™ Equiv.from e))