open import Cat.Instances.Product
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Product where

module _ {o β} (C : Precategory o β) where
open Cat.Reasoning C


# 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 β β) where
field
β¨_,_β© : β {Q} (p1 : Hom Q A) (p2 : Hom Q B) β Hom Q P
Οβββ¨β© : β {Q} {p1 : Hom Q _} {p2} β Οβ β β¨ p1 , p2 β© β‘ p1
Οβββ¨β© : β {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 β©

β¨β©-Ξ· = sym $unique (idr _) (idr _)  A product of and is an explicit choice of product diagram:  record Product (A B : Ob) : Type (o β β) 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  ## Uniquenessπ module _ {o β} {C : Precategory o β} where open Cat.Reasoning C open Product hiding (β¨_,_β© ; Οβ ; Οβ ; β¨β©β) private variable A B a b c d : Ob  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 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.Οβββ¨β© Β·Β· p1.Οβββ¨β©) (assoc _ _ _ Β·Β· ap (_β _) p2.Οβββ¨β© Β·Β· p1.Οβββ¨β©) (idr _) (idr _) p2βp1βp2 : p2βp1 β p1βp2 β‘ id p2βp1βp2 = p1.uniqueβ (assoc _ _ _ Β·Β· ap (_β _) p1.Οβββ¨β© Β·Β· p2.Οβββ¨β©) (assoc _ _ _ Β·Β· ap (_β _) p1.Οβββ¨β© Β·Β· p2.Οβββ¨β©) (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 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' .Οβββ¨β© = pullr (prod .Οβββ¨β©) β cancell fi.invl prod' .Οβββ¨β© = pullr (prod .Οβββ¨β©) β cancell gi.invl prod' .unique p q = prod .unique (sym (ap (_ β_) (sym p) β pulll (cancell fi.invr))) (sym (ap (_ β_) (sym q) β pulll (cancell gi.invr))) is-product-iso-apex : β {A B P P'} {Οβ : Hom P A} {Οβ : Hom P B} {Οβ' : Hom P' A} {Οβ' : Hom P' B} {f : Hom P' P} β is-invertible f β Οβ β f β‘ Οβ' β Οβ β f β‘ Οβ' β is-product C Οβ Οβ β is-product C Οβ' Οβ' is-product-iso-apex {f = f} f-iso f-Οβ f-Οβ prod = prod' where module fi = is-invertible f-iso open is-product prod' : is-product _ _ _ prod' .β¨_,_β© qa qb = fi.inv β prod .β¨_,_β© qa qb prod' .Οβββ¨β© = pulll (rswizzle (sym f-Οβ) fi.invl) β prod .Οβββ¨β© prod' .Οβββ¨β© = pulll (rswizzle (sym f-Οβ) fi.invl) β prod .Οβββ¨β© prod' .unique p q = sym$ lswizzle
(sym (prod .unique (pulll f-Οβ β p) (pulll f-Οβ β q))) fi.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) where

  open Cat.Reasoning C
private variable
A B a b c d : Ob

-- Note: here and below we have to open public the aliases in a module
-- with parameters so Agda picks up the display forms.
module _ {a b} where open Product (all-products a b) renaming (unique to β¨β©-unique) hiding (apex) public
open Functor

infix 50 _ββ_


We start by defining a βglobalβ product-assigning operation.

  module _ a b where
open Product (all-products a b)
renaming (apex to infixr 7 _ββ_)
using () public


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-comm id-comm Γ-functor .F-β (f , g) (h , i) = sym$ β¨β©-unique


We also define a handful of common morphisms.

  Ξ΄ : Hom a (a ββ a)
Ξ΄ = β¨ id , id β©

swap : Hom (a ββ b) (b ββ a)
swap = β¨ Οβ , Οβ β©

Γ-assoc : Hom (a ββ (b ββ c)) ((a ββ b) ββ c)
Γ-assoc = β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β©

  Ξ΄-natural : is-natural-transformation Id (Γ-functor Fβ Catβ¨ Id , Id β©Cat) Ξ» _ β Ξ΄
Ξ΄-natural x y f = uniqueβ

swap-is-iso : β {a b} β is-invertible (swap {a} {b})
swap-is-iso = make-invertible swap

swap-natural
: β {A B C D} ((f , g) : Hom A C Γ Hom B D)
β (g ββ f) β swap β‘ swap β (f ββ g)
swap-natural (f , g) =
β¨ Οβ β (f ββ g) , Οβ β (f ββ g) β©     β‘Λβ¨ β¨β©β _ β©β‘Λ
swap β (f ββ g)                       β

swap-Ξ΄ : β {A} β swap β Ξ΄ β‘ Ξ΄ {A}

assoc-Ξ΄ : β {a} β Γ-assoc β (id ββ Ξ΄ {a}) β Ξ΄ {a} β‘ (Ξ΄ ββ id) β Ξ΄
assoc-Ξ΄ = uniqueβ
refl

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

Οβ-inv
: β {f : Hom (a ββ b) c} {g : Hom (a ββ b) d}
β f β is-invertible.inv β¨β©-inv β‘ Οβ
Οβ-inv {f = f} {g = g} β¨β©-inv =

Οβ-inv
: β {f : Hom (a ββ b) c} {g : Hom (a ββ b) d}
β g β is-invertible.inv β¨β©-inv β‘ Οβ
Οβ-inv {f = f} {g = g} β¨β©-inv =


# Representability of productsπ

module _ {o β} {C : Precategory o β} where
open Cat.Reasoning C


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.

  product-repr
: β {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 β©