Large precategories
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Bonnevier, Julian KG, fernabnor and louismntnu.
Created on 2022-03-11.
Last modified on 2023-09-26.
module category-theory.large-precategories where
Imports
open import category-theory.precategories open import foundation.action-on-identifications-binary-functions open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.sets open import foundation.universe-levels
Idea
A large precategory is a precategory where we don't fix a universe for the type of objects or morphisms. (This cannot be done with Σ-types, we must use a record type.)
Definition
Large precategories
record Large-Precategory (α : Level → Level) (β : Level → Level → Level) : UUω where constructor make-Large-Precategory field obj-Large-Precategory : (l : Level) → UU (α l) hom-set-Large-Precategory : {l1 l2 : Level} → obj-Large-Precategory l1 → obj-Large-Precategory l2 → Set (β l1 l2) comp-hom-Large-Precategory : {l1 l2 l3 : Level} {X : obj-Large-Precategory l1} {Y : obj-Large-Precategory l2} {Z : obj-Large-Precategory l3} → type-Set (hom-set-Large-Precategory Y Z) → type-Set (hom-set-Large-Precategory X Y) → type-Set (hom-set-Large-Precategory X Z) id-hom-Large-Precategory : {l1 : Level} {X : obj-Large-Precategory l1} → type-Set (hom-set-Large-Precategory X X) associative-comp-hom-Large-Precategory : {l1 l2 l3 l4 : Level} {X : obj-Large-Precategory l1} {Y : obj-Large-Precategory l2} {Z : obj-Large-Precategory l3} {W : obj-Large-Precategory l4} → (h : type-Set (hom-set-Large-Precategory Z W)) (g : type-Set (hom-set-Large-Precategory Y Z)) (f : type-Set (hom-set-Large-Precategory X Y)) → ( comp-hom-Large-Precategory (comp-hom-Large-Precategory h g) f) = ( comp-hom-Large-Precategory h (comp-hom-Large-Precategory g f)) left-unit-law-comp-hom-Large-Precategory : {l1 l2 : Level} {X : obj-Large-Precategory l1} {Y : obj-Large-Precategory l2} (f : type-Set (hom-set-Large-Precategory X Y)) → ( comp-hom-Large-Precategory id-hom-Large-Precategory f) = f right-unit-law-comp-hom-Large-Precategory : {l1 l2 : Level} {X : obj-Large-Precategory l1} {Y : obj-Large-Precategory l2} (f : type-Set (hom-set-Large-Precategory X Y)) → ( comp-hom-Large-Precategory f id-hom-Large-Precategory) = f open Large-Precategory public
module _ {α : Level → Level} {β : Level → Level → Level} (C : Large-Precategory α β) where hom-Large-Precategory : {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2) → UU (β l1 l2) hom-Large-Precategory X Y = type-Set (hom-set-Large-Precategory C X Y) is-set-hom-Large-Precategory : {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2) → is-set (hom-Large-Precategory X Y) is-set-hom-Large-Precategory X Y = is-set-type-Set (hom-set-Large-Precategory C X Y) ap-comp-hom-Large-Precategory : {l1 l2 l3 : Level} {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} {Z : obj-Large-Precategory C l3} {g g' : hom-Large-Precategory Y Z} (p : g = g') {f f' : hom-Large-Precategory X Y} (q : f = f') → comp-hom-Large-Precategory C g f = comp-hom-Large-Precategory C g' f' ap-comp-hom-Large-Precategory = ap-binary (comp-hom-Large-Precategory C) comp-hom-Large-Precategory' : {l1 l2 l3 : Level} {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} {Z : obj-Large-Precategory C l3} → hom-Large-Precategory X Y → hom-Large-Precategory Y Z → hom-Large-Precategory X Z comp-hom-Large-Precategory' f g = comp-hom-Large-Precategory C g f
Precomposition by a morphism
precomp-hom-Large-Precategory : {l1 l2 l3 : Level} {X : obj-Large-Precategory C l1} {Y : obj-Large-Precategory C l2} (f : hom-Large-Precategory X Y) → (Z : obj-Large-Precategory C l3) → hom-Large-Precategory Y Z → hom-Large-Precategory X Z precomp-hom-Large-Precategory f Z g = comp-hom-Large-Precategory C g f
Postcomposition by a morphism
postcomp-hom-Large-Precategory : {l1 l2 l3 : Level} (X : obj-Large-Precategory C l1) {Y : obj-Large-Precategory C l2} {Z : obj-Large-Precategory C l3} (f : hom-Large-Precategory Y Z) → hom-Large-Precategory X Y → hom-Large-Precategory X Z postcomp-hom-Large-Precategory X f g = comp-hom-Large-Precategory C f g
Precategories obtained from large precategories
module _ {α : Level → Level} {β : Level → Level → Level} (C : Large-Precategory α β) where precategory-Large-Precategory : (l : Level) → Precategory (α l) (β l l) pr1 (precategory-Large-Precategory l) = obj-Large-Precategory C l pr1 (pr2 (precategory-Large-Precategory l)) = hom-set-Large-Precategory C pr1 (pr1 (pr2 (pr2 (precategory-Large-Precategory l)))) = comp-hom-Large-Precategory C pr2 (pr1 (pr2 (pr2 (precategory-Large-Precategory l)))) = associative-comp-hom-Large-Precategory C pr1 (pr2 (pr2 (pr2 (precategory-Large-Precategory l)))) x = id-hom-Large-Precategory C pr1 (pr2 (pr2 (pr2 (pr2 (precategory-Large-Precategory l))))) = left-unit-law-comp-hom-Large-Precategory C pr2 (pr2 (pr2 (pr2 (pr2 (precategory-Large-Precategory l))))) = right-unit-law-comp-hom-Large-Precategory C
Recent changes
- 2023-09-26. Fredrik Bakke and Egbert Rijke. Maps of categories, functor categories, and small subprecategories (#794).
- 2023-09-19. Egbert Rijke. Isomorphisms in large categories and large precategories (#791).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-13. Fredrik Bakke. Remove unused imports and fix some unaddressed comments (#621).