This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Initial objects of large precategories

module category-theory.initial-objects-large-precategories where

open import category-theory.large-precategories

open import foundation.contractible-types
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-Precategory α β)
  {l : Level} (X : obj-Large-Precategory C l)
  where

  is-initial-obj-Large-Precategory : UUω
  is-initial-obj-Large-Precategory =
    {l2 : Level} (Y : obj-Large-Precategory C l2) →
    is-contr (hom-Large-Precategory C X Y)