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
open import category-theory.large-precategories

open import foundation.subtypes
open import foundation.universe-levels


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.


Large subprecategories

module _
  {α : Level  Level} {β : Level  Level  Level}
  (γ : Level  Level) (δ : Level  Level  Level)
  (C : Large-Precategory α β)

    Large-Subprecategory : UUω
      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) 
          ( 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 
          ( 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)

  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