module Cat.Instances.Product where

Product categoriesπŸ”—

Let and be two precategories; we put no restrictions on their relative sizes. Their product category is the category having as object pairs of an object and and the morphisms are pairs of a morphism in and a morphism in The product category admits two projection functors

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 2
  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 (resp 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 , G .Fβ‚€ x
  f .F₁ f = F .F₁ f , G .F₁ f
  f .F-id i = F .F-id i , G .F-id i
  f .F-∘ f g i = F .F-∘ f g i , G .F-∘ 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'

  : {F G : Functor B D} {H K : Functor C E}
  β†’ F => G β†’ H => K β†’ (F FΓ— H) => (G FΓ— K)
_ntΓ—_ Ξ± Ξ² .Ξ· (c , d) = Ξ± .Ξ· c , Ξ² .Ξ· d
_ntΓ—_ Ξ± Ξ² .is-natural (c , d) (c' , d') (f , g) = Ξ£-pathp
  (Ξ± .is-natural c c' f)
  (Ξ² .is-natural d d' 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 (Univalent.Hom-pathp-reflr-iso c-cat (C.idr _))
              (Univalent.Hom-pathp-reflr-iso d-cat (D.idr _))

  1. When and are precategories, this functor is only unique up to a natural isomorphismβ†©οΈŽ