open import Cat.Prelude

module Cat.Instances.Product where

Product categories🔗

Given two categories C\ca{C} and D\ca{D}, we construct their product C×CatD\ca{C} \times_\cat \ca{D}. The objects of the product are pairs (x,y)(x,y) where xCx \in \ca{C} and yDy \in \ca{D}; The product admits projection functors C×CatDC\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 AC×CatD\mathcal{A} \to \ca{C} \times_\cat \ca{D} making the diagram commute.

This would suggest that C×CatD\ca{C} \times_\cat \ca{D} is the categorical product of C\ca{C} and D\ca{D} in a metaphorical “category of categories”, but homotopical considerations prevent such a category from existing: The space of functors [C,D][\ca{C},\ca{D}] is a groupoid (since the component with highest h-level is the object mapping C0D0\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 C×CatDC\ca{C} \times_\cat \ca{D} \to \ca{C} (resp D\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