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

import Cat.Reasoning

module Cat.Instances.Product where

open Precategory
open Functor
open _=>_
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}\text{,}$ and the morphisms are pairs $(f,g)$ of a morphism in $\mathcal{C}$ and a morphism in $\mathcal{D}\text{.}$ 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 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}\text{)}$ 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'

_nt×_
  : {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)

{-# 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 (Univalent.Hom-pathp-reflr-iso c-cat (C.idr _))
              (Univalent.Hom-pathp-reflr-iso d-cat (D.idr _))