Initial objects of large precategories

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-09-21.
Last modified on 2023-09-26.

module category-theory.initial-objects-large-precategories where
Imports 
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)

Recent changes