Products of precategories
Content created by Egbert Rijke, Fredrik Bakke, Fernando Chu, Julian KG, fernabnor and louismntnu.
Created on 2023-05-04.
Last modified on 2023-09-13.
module category-theory.products-of-precategories where
Imports
open import category-theory.precategories open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.sets open import foundation.universe-levels
Idea
The product of two precategories C
and
D
has as objects pairs (x , y)
, for x
in obj-Precategory C
and y
in
obj-Precategory D
; and has a morphism Hom (x , y) (x' , y)
for each pair of
morphisms f : x → x'
and g : y → y'
. Composition of morphisms is given by
composing each entry.
Definition
module _ {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) where prod-Precategory : Precategory (l1 ⊔ l3) (l2 ⊔ l4) pr1 prod-Precategory = obj-Precategory C × obj-Precategory D pr1 (pr2 prod-Precategory) (x , y) (x' , y') = prod-Set (hom-Precategory C x x') (hom-Precategory D y y') pr1 (pr1 (pr1 (pr2 (pr2 prod-Precategory))) (f' , g') (f , g)) = comp-hom-Precategory C f' f pr2 (pr1 (pr1 (pr2 (pr2 prod-Precategory))) (f' , g') (f , g)) = comp-hom-Precategory D g' g pr2 (pr1 (pr2 (pr2 prod-Precategory))) (f'' , g'') (f' , g') (f , g) = eq-pair ( associative-comp-hom-Precategory C f'' f' f) ( associative-comp-hom-Precategory D g'' g' g) pr1 (pr1 (pr2 (pr2 (pr2 prod-Precategory))) (x , y)) = id-hom-Precategory C {x} pr2 (pr1 (pr2 (pr2 (pr2 prod-Precategory))) (x , y)) = id-hom-Precategory D {y} pr1 (pr2 (pr2 (pr2 (pr2 prod-Precategory)))) (f , g) = eq-pair ( left-unit-law-comp-hom-Precategory C f) ( left-unit-law-comp-hom-Precategory D g) pr2 (pr2 (pr2 (pr2 (pr2 prod-Precategory)))) (f , g) = eq-pair ( right-unit-law-comp-hom-Precategory C f) ( right-unit-law-comp-hom-Precategory D g)
Recent changes
- 2023-09-13. Fredrik Bakke and Egbert Rijke. Refactor structured monoids (#761).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-05-06. Egbert Rijke. Big cleanup throughout library (#594).
- 2023-05-04. Fernando Chu and Fernando Chu. The product of precategories (#586).