open import Cat.Functor.Base
open import Cat.Univalent
open import Cat.Prelude

import Cat.Reasoning

module Cat.Instances.Product where

Product categoriesπŸ”—

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

C←π1(CΓ—cD)β†’Ο€2D, \ca{C} \xot{\pi_1} (\ca{C} \times^c \ca{D}) \xto{\pi_2} \ca{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 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

infixr 20 _Γ—αΆœ_

We define the two projection functors C×CatD→C\ca{C} \times_\cat \ca{D} \to \ca{C} (resp →D\to \ca{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


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\ca{C} and D\ca{D} are precategories, this functor is only unique up to a natural isomorphismβ†©οΈŽ