open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Fin

import Cat.Reasoning as Cr

module Cat.Diagram.Product.Finite
{o β} {C : Precategory o β}
(terminal : Terminal C)
(products : β A B β Product C A B)
where

open is-indexed-product
open Indexed-product
open is-product
open Terminal
open Product
open Cr C
private module Cart = Binary-products C products
open Cart using (_ββ_)


# 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 of length then its product exists as long as 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 we simply let it be 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

F-unique
: β {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, is univalent, then we can strengthen this result to work with all finite types, not just the standard types.

To see why univalence is required, remember that finite types are merely equivalent to 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.

Cartesianβfinite-products
: 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
where
go : X β Fin n β Indexed-product C F
go e = Indexed-product-β C e
(Cartesianβstandard-finite-products (F β Equiv.from e))