Initial objects of a precategory

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-03-21.
Last modified on 2023-09-21.

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

open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

open import foundation-core.identity-types

Idea

The initial object of a precategory (if it exists) is an object with the universal property that there is a unique morphism from it to any object.

Definition

The universal property of initial objects in precategories

module _
  {l1 l2 : Level} (C : Precategory l1 l2) (X : obj-Precategory C)
  where

  is-initial-prop-obj-Precategory : Prop (l1 ⊔ l2)
  is-initial-prop-obj-Precategory =
    Π-Prop
      ( obj-Precategory C)
      ( λ Y → is-contr-Prop (type-hom-Precategory C X Y))

  is-initial-obj-Precategory : UU (l1 ⊔ l2)
  is-initial-obj-Precategory = type-Prop is-initial-prop-obj-Precategory

  is-prop-is-initial-obj-Precategory : is-prop is-initial-obj-Precategory
  is-prop-is-initial-obj-Precategory =
    is-prop-type-Prop is-initial-prop-obj-Precategory

The type of initial objects in a precategory

initial-object-Precategory :
  {l1 l2 : Level} (C : Precategory l1 l2) → UU (l1 ⊔ l2)
initial-object-Precategory C =
  Σ (obj-Precategory C) λ i →
    (x : obj-Precategory C) → is-contr (type-hom-Precategory C i x)

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (i : initial-object-Precategory C)
  where

  object-initial-object-Precategory : obj-Precategory C
  object-initial-object-Precategory = pr1 i

  morphism-initial-object-Precategory :
    (x : obj-Precategory C) →
    type-hom-Precategory C object-initial-object-Precategory x
  morphism-initial-object-Precategory x = pr1 (pr2 i x)

  is-unique-morphism-initial-object-Precategory :
    (x : obj-Precategory C)
    (f : type-hom-Precategory C object-initial-object-Precategory x) →
    morphism-initial-object-Precategory x ＝ f
  is-unique-morphism-initial-object-Precategory x = pr2 (pr2 i x)

Recent changes