Large subcategories

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-28.
Last modified on 2023-11-24.

module category-theory.large-subcategories where
Imports 
open import category-theory.large-categories
open import category-theory.large-subprecategories

open import foundation.universe-levels

Idea

A large subcategory of a large category C is a large subprecategory P of the underlying large precategory of C.

Definition

module _
  {α : Level → Level} {β : Level → Level → Level}
  (γ : Level → Level) (δ : Level → Level → Level)
  (C : Large-Category α β)
  where

  Large-Subcategory : UUω
  Large-Subcategory =
    Large-Subprecategory γ δ (large-precategory-Large-Category C)

Recent changes