module Cat.Instances.Product where

Product categoriesπŸ”—

Let C\mathcal{C} and D\mathcal{D} be two precategories; we put no restrictions on their relative sizes. Their product category CΓ—cD\mathcal{C} \times^c \mathcal{D} is the category having as object pairs (x,y)(x, y) of an object x:Cx : \mathcal{C} and y:Dy : \mathcal{D}, and the morphisms are pairs (f,g)(f, g) of a morphism in C\mathcal{C} and a morphism in D\mathcal{D}. The product category admits two projection functors

C←π1(CΓ—cD)β†’Ο€2D, \mathcal{C} \xleftarrow{\pi_1} (\mathcal{C} \times^c \mathcal{D}) \xrightarrow{\pi_2} \mathcal{D}\text{,}

satisfying a universal property analogous to those of product diagrams in categories. Namely, given a setup like in the diagram below, there is a unique1 functor which fits into the dashed line and makes the whole diagram commute.

Formulating this universal property properly would take us further afield into 2-category theory than is appropriate here.

_Γ—αΆœ_ : Precategory o₁ h₁ β†’ Precategory oβ‚‚ hβ‚‚ β†’ Precategory _ _
C Γ—αΆœ D = prodcat module Γ—αΆœ 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') = hlevel!
  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

{-# DISPLAY Γ—αΆœ.prodcat a b = a Γ—αΆœ b #-}
infixr 20 _Γ—αΆœ_

We define the two projection functors C×D→C\mathcal{C} \times \mathcal{D} \to \mathcal{C} (resp →D\to \mathcal{D}) as the evident liftings of the fst and snd operations from the product type. Functoriality is automatic because composites (and identities) are defined componentwise in the product category.

Fst : Functor (C Γ—αΆœ D) C
Fst .Fβ‚€ = fst
Fst .F₁ = fst
Fst .F-id = refl
Fst .F-∘ _ _ = refl

Snd : Functor (C Γ—αΆœ 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 Γ—αΆœ 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

_FΓ—_ : Functor B D β†’ Functor C E β†’ Functor (B Γ—αΆœ C) (D Γ—αΆœ E)
_FΓ—_ {B = B} {D = D} {C = C} {E = E} G H = func
  module FΓ— where

  func : Functor (B Γ—αΆœ C) (D Γ—αΆœ E)
  func .Fβ‚€ (x , y) = (G .Fβ‚€ x) , (H .Fβ‚€ y)
  func .F₁ (f , g) = (G .F₁ f) , (H .F₁ g)
  func .F-id = (G .F-id) ,β‚š (H .F-id)
  func .F-∘ (f , g) (f' , g') = (G .F-∘ f f') ,β‚š H .F-∘ g g'


Isomorphisms in functor categories admit a short description, too: They are maps which are componentwise isomorphisms. It follows, since paths in product types are products of paths in the component types, that the product of univalent categories is itself a univalent category.

    Γ—αΆœ-is-category : is-category (C Γ—αΆœ D)
    Γ—αΆœ-is-category .to-path im =
      Σ-pathp (C.iso→path (F-map-iso Fst im)) (D.iso→path (F-map-iso Snd im))
    Γ—αΆœ-is-category .to-path-over p = C*D.β‰…-pathp _ _ $
      Ξ£-pathp-dep (Univalent.Hom-pathp-reflr-iso c-cat (C.idr _))
                  (Univalent.Hom-pathp-reflr-iso d-cat (D.idr _))

  1. When C\mathcal{C} and D\mathcal{D} are precategories, this functor is only unique up to a natural isomorphismβ†©οΈŽ