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

import Cat.Reasoning

module Cat.Instances.Product where

open Precategory
open Functor
private variable
  o₁ h₁ o₂ h₂ : Level
  B C D E : Precategory o₁ h₁

Product categories🔗

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

$$\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 unique¹ 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  _×ᶜ_

We define the two projection functors $\mathcal{C} \times \mathcal{D} \to \mathcal{C}$ (resp $\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'

{-# DISPLAY F×.func F G = F F× G #-}

Univalence🔗

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.

module
  _ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
    (c-cat : is-category C) (d-cat : is-category D) where
    private
      module C   = Univalent c-cat
      module D   = Univalent d-cat
      module C*D = Cat.Reasoning (C ×ᶜ D)

    ×ᶜ-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 _))