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)
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 _))
When and are precategories, this functor is only unique up to a natural isomorphismβ©οΈ