Initial objects of large categories

Content created by Egbert Rijke and Gregor Perčič.

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

module category-theory.initial-objects-large-categories where
Imports 
open import category-theory.initial-objects-large-precategories
open import category-theory.large-categories

open import foundation.universe-levels

Idea

An initial object in a large category C is an object X such that hom X Y is contractible for any object Y.

Definitions

Initial objects in large categories

module _
  {α : Level → Level} {β : Level → Level → Level}
  (C : Large-Category α β)
  {l : Level} (X : obj-Large-Category C l)
  where

  is-initial-obj-Large-Category : UUω
  is-initial-obj-Large-Category =
    is-initial-obj-Large-Precategory (large-precategory-Large-Category C) X

Recent changes