Large subprecategories
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-09-28.
Last modified on 2023-11-01.
module category-theory.large-subprecategories where
Imports
open import category-theory.large-precategories open import foundation.subtypes open import foundation.universe-levels
Idea
A large subprecategory of a
large precategory C
consists of a
family of subtypes P₀
P₀ : (l : Level) → subtype _ (obj C l)
of the objects of C
indexed by universe levels, and a family of subtypes P₁
P₁ : {l1 l2 : Level} (X : obj C l1) (Y : obj C l2) →
P₀ X → P₀ Y → subtype _ (hom X Y)
of the morphisms of C
, such that P₁
contains all identity morphisms of
objects in P₀
and is closed under composition.
Definition
Large subprecategories
module _ {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level) (δ : Level → Level → Level) (C : Large-Precategory α β) where record Large-Subprecategory : UUω where field subtype-obj-Large-Subprecategory : (l : Level) → subtype (γ l) (obj-Large-Precategory C l) subtype-hom-Large-Subprecategory : {l1 l2 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2) → is-in-subtype (subtype-obj-Large-Subprecategory l1) X → is-in-subtype (subtype-obj-Large-Subprecategory l2) Y → subtype (β l1 l2) (hom-Large-Precategory C X Y) contains-id-Large-Subprecategory : {l1 : Level} (X : obj-Large-Precategory C l1) → (H : is-in-subtype (subtype-obj-Large-Subprecategory l1) X) → is-in-subtype ( subtype-hom-Large-Subprecategory X X H H) ( id-hom-Large-Precategory C) is-closed-under-composition-Large-Subprecategory : {l1 l2 l3 : Level} (X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory C l2) (Z : obj-Large-Precategory C l3) (g : hom-Large-Precategory C Y Z) (f : hom-Large-Precategory C X Y) → (K : is-in-subtype (subtype-obj-Large-Subprecategory l1) X) → (L : is-in-subtype (subtype-obj-Large-Subprecategory l2) Y) → (M : is-in-subtype (subtype-obj-Large-Subprecategory l3) Z) → is-in-subtype (subtype-hom-Large-Subprecategory Y Z L M) g → is-in-subtype (subtype-hom-Large-Subprecategory X Y K L) f → is-in-subtype ( subtype-hom-Large-Subprecategory X Z K M) ( comp-hom-Large-Precategory C g f) open Large-Subprecategory public module _ {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level} {δ : Level → Level → Level} (C : Large-Precategory α β) (P : Large-Subprecategory γ δ C) where is-in-obj-Large-Subprecategory : {l : Level} → obj-Large-Precategory C l → UU (γ l) is-in-obj-Large-Subprecategory = is-in-subtype (subtype-obj-Large-Subprecategory P _)
Recent changes
- 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).
- 2023-09-28. Egbert Rijke and Fredrik Bakke. Cyclic types (#800).