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
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-09-28. Egbert Rijke and Fredrik Bakke. Cyclic types (#800).