open import Cat.Instances.Product open import Cat.Prelude module Cat.Diagram.Product {o h} (C : Precategory o h) where
Productsπ
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 β h) where field β¨_,_β© : β {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)
A product of and is an explicit choice of product diagram:
record Product (A B : Ob) : Type (o β h) where no-eta-equality field apex : Ob Οβ : Hom apex A Οβ : Hom apex B has-is-product : is-product Οβ Οβ open is-product has-is-product public open Product hiding (β¨_,_β© ; Οβ ; Οβ ; β¨β©β)
Uniquenessπ
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 A B) β apex p1 β apex p2 Γ-Unique p1 p2 = make-iso p1βp2 p2βp1 p1βp2βp1 p2βp1βp2 where 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 = p2.uniqueβ (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 = p1.uniqueβ (assoc _ _ _ Β·Β· ap (_β _) p1.Οββfactor Β·Β· p2.Οββfactor) (assoc _ _ _ Β·Β· ap (_β _) p1.Οββfactor Β·Β· p2.Οββfactor) (idr _) (idr _) is-product-iso : β {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)))
The product functorπ
If admits products of all pairs of objects, then the assignment extends to a bifunctor .
module Cartesian (hasprods : β A B β Product A B) where open Functor Γ-functor : Functor (C ΓαΆ C) C Γ-functor .Fβ (A , B) = hasprods A B .apex Γ-functor .Fβ {a , x} {b , y} (f , g) = hasprods b y .has-is-product .is-product.β¨_,_β© (f β hasprods a x .Product.Οβ) (g β hasprods a x .Product.Οβ) Γ-functor .F-id {a , b} = uniqueβ (hasprods a b) (hasprods a b .Οββfactor) (hasprods a b .Οββfactor) id-comm id-comm Γ-functor .F-β {a , b} {c , d} {e , f} x y = uniqueβ (hasprods e f) (hasprods e f .Οββfactor) (hasprods e f .Οββfactor) ( pulll (hasprods e f .Οββfactor) Β·Β· pullr (hasprods c d .Οββfactor) Β·Β· assoc _ _ _) ( pulll (hasprods e f .Οββfactor) Β·Β· pullr (hasprods c d .Οββfactor) Β·Β· assoc _ _ _)
We refer to a category admitting all binary products as cartesian. When working with products, a Cartesian category is the place to be, since we can work with the βcanonicalβ product operations β rather than requiring different product data for any pair of objects we need a product for.
Here we extract the data of the βglobalβ product-assigning operation to separate top-level definitions:
_β_ : Ob β Ob β Ob A β B = Fβ Γ-functor (A , B) β¨_,_β© : Hom a b β Hom a c β Hom a (b β c) β¨ f , g β© = hasprods _ _ .has-is-product .is-product.β¨_,_β© f g Οβ : Hom (a β b) a Οβ = hasprods _ _ .Product.Οβ Οβ : Hom (a β b) b Οβ = hasprods _ _ .Product.Οβ Οβββ¨β© : {f : Hom a b} {g : Hom a c} β Οβ β β¨ f , g β© β‘ f Οβββ¨β© = hasprods _ _ .has-is-product .is-product.Οββfactor Οβββ¨β© : {f : Hom a b} {g : Hom a c} β Οβ β β¨ f , g β© β‘ g Οβββ¨β© = hasprods _ _ .has-is-product .is-product.Οββfactor β¨β©β : β {Q R} {p1 : Hom Q a} {p2 : Hom Q b} (f : Hom R Q) β β¨ p1 , p2 β© β f β‘ β¨ p1 β f , p2 β f β© β¨β©β f = is-product.β¨β©β (hasprods _ _ .has-is-product) f β¨β©-unique : β {Q} {p1 : Hom Q A} {p2 : Hom Q B} β (other : Hom Q (A β B)) β Οβ β other β‘ p1 β Οβ β other β‘ p2 β other β‘ β¨ p1 , p2 β© β¨β©-unique = hasprods _ _ .has-is-product .is-product.unique β¨β©-Ξ· : β {A B} β β¨ Οβ , Οβ β© β‘ id {A β B} β¨β©-Ξ· = sym $ β¨β©-unique id (idr Οβ) (idr Οβ)