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 and be two precategories; we put no restrictions on their relative sizes. Their product category is the category having as object pairs of an object and and the morphisms are pairs of a morphism in and a morphism in 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 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 2
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 (resp 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 _))


1. When and are precategories, this functor is only unique up to a natural isomorphismβ©οΈ