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 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 $\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 _))


1. When $\mathcal{C}$ and $\mathcal{D}$ are precategories, this functor is only unique up to a natural isomorphism↩︎