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

import Cat.Reasoning

module Cat.Instances.Product where


# Product categories🔗

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

$\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 $\ca{C} \times_\cat \ca{D} \to \ca{C}$ (resp $\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


## 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.

    ×ᶜ-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 $\ca{C}$ and $\ca{D}$ are precategories, this functor is only unique up to a natural isomorphism↩︎