open import Cat.Diagram.Product.Indexed open import Cat.Diagram.Limit.Finite open import Cat.Diagram.Limit.Base open import Cat.Diagram.Equaliser 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
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