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