open import Cat.Prelude

module Cat.Instances.Product where


# Product categories🔗

Given two categories $\ca{C}$ and $\ca{D}$, we construct their product $\ca{C} \times_\cat \ca{D}$. The objects of the product are pairs $(x,y)$ where $x \in \ca{C}$ and $y \in \ca{D}$; The product admits projection functors $\ca{C} \times_\id{Cat} \ca{D} \to \ca{C}$ (onto both factors, not just the first), and given a diagram of categories as below, there is a unique (in the bicategorical sense) functor $\mathcal{A} \to \ca{C} \times_\cat \ca{D}$ making the diagram commute.

This would suggest that $\ca{C} \times_\cat \ca{D}$ is the categorical product of $\ca{C}$ and $\ca{D}$ in a metaphorical “category of categories”, but homotopical considerations prevent such a category from existing: The space of functors $[\ca{C},\ca{D}]$ is a groupoid (since the component with highest h-level is the object mapping $\ca{C}_0 \to \ca{D}_0$), but the hom-spaces in a precategory must be sets

_×Cat_ : Precategory o₁ h₁ → Precategory o₂ h₂ → Precategory _ _
C ×Cat D = prodcat where
module C = Precategory C
module D = Precategory D

prodcat : Precategory _ _
prodcat .Ob = Ob C × Ob D
prodcat .Hom (a , a') (b , b') = Hom C a b × Hom D a' b'
prodcat .Hom-set (a , a') (b , b') = ×-is-hlevel 2 (Hom-set C a b) (Hom-set D a' b')
prodcat .id = id C , id D
prodcat ._∘_ (f , f') (g , g') = f C.∘ g , f' D.∘ g'
prodcat .idr (f , f') i = C.idr f i , D.idr f' i
prodcat .idl (f , f') i = C.idl f i , D.idl f' i
prodcat .assoc (f , f') (g , g') (h , h') i =
C.assoc f g h i , D.assoc f' g' h' i

infixr 20 _×Cat_


We define the two projection functors $\ca{C} \times_\cat \ca{D} \to \ca{C}$ (resp $\to \ca{D}$) as the evident liftings of the fst and snd operations on the product type.

Fst : Functor (C ×Cat D) C
Fst .F₀ = fst
Fst .F₁ = fst
Fst .F-id = refl
Fst .F-∘ _ _ = refl

Snd : Functor (C ×Cat D) D
Snd .F₀ = snd
Snd .F₁ = snd
Snd .F-id = refl
Snd .F-∘ _ _ = refl

Cat⟨_,_⟩ : Functor E C → Functor E D → Functor E (C ×Cat D)
Cat⟨ F , G ⟩Cat = f where
f : Functor _ _
f .F₀ x = F₀ F x , F₀ G x
f .F₁ f = F₁ F f , F₁ G f
f .F-id i = F-id F i , F-id G i
f .F-∘ f g i = F-∘ F f g i , F-∘ G f g i