open import 1Lab.Reflection.Record open import Cat.Instances.Functor open import Cat.Instances.Product open import Cat.Diagram.Product open import Cat.Prelude module Cat.Instances.StrictCat where
Strict precategoriesπ
We call a precategory strict if its space of objects is a Set. While general precategories are too homotopically interesting to fit into a Precategory (because functor spaces will not, in general, be h-sets), the strict categories do form a precategory, which we denote .
Strict-cats : β o h β Precategory _ _ Strict-cats o h .Ob = Ξ£[ C β Precategory o h ] (is-set (Ob C)) Strict-cats o h .Hom (C , _) (D , _) = Functor C D Strict-cats o h .id = Id Strict-cats o h ._β_ = _Fβ_ Strict-cats o h .idr _ = Functor-path (Ξ» _ β refl) Ξ» _ β refl Strict-cats o h .idl _ = Functor-path (Ξ» _ β refl) Ξ» _ β refl Strict-cats o h .assoc _ _ _ = Functor-path (Ξ» _ β refl) Ξ» _ β refl
This assembles into a Precategory because the only bit of a Functor that doesnβt have a fixed h-level is the object mapping; By asking that D be a strict category, this fixes the functors to be sets.
Strict-cats o h .Hom-set _ (D , dset) = Functor-is-set dset
Productsπ
We prove that Strict-cats has products. This is because is , and h-levels are closed under products.
Strict-cats-products : {C D : Precategory o h} β (cob : is-set (Ob C)) (dob : is-set (Ob D)) β Product (Strict-cats o h) (C , cob) (D , dob) Strict-cats-products {C = C} {D = D} cob dob = prod where prod : Product (Strict-cats _ _) (C , cob) (D , dob) prod .apex = C ΓαΆ D , Γ-is-hlevel 2 cob dob prod .Οβ = Fst {C = C} {D = D} prod .Οβ = Snd {C = C} {D = D} prod .has-is-product .β¨_,_β© p q = Catβ¨ p , q β©Cat prod .has-is-product .Οββfactor = Functor-path (Ξ» _ β refl) Ξ» _ β refl prod .has-is-product .Οββfactor = Functor-path (Ξ» _ β refl) Ξ» _ β refl prod .has-is-product .unique other p q = Functor-path (Ξ» x i β Fβ (p i) x , Fβ (q i) x) Ξ» f i β Fβ (p i) f , Fβ (q i) f