# Constructions related to weakly initial objects #

This file gives constructions related to weakly initial objects, namely:

- If a category has small products and a small weakly initial set of objects, then it has a weakly initial object.
- If a category has wide equalizers and a weakly initial object, then it has an initial object.

These are primarily useful to show the General Adjoint Functor Theorem.

theorem
CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{ι : Type v}
{B : ι → C}
(hB : ∀ (A : C), ∃ i, Nonempty (B i ⟶ A))
:

If `C`

has (small) products and a small weakly initial set of objects, then it has a weakly initial
object.

theorem
CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasWideEqualizers C]
{T : C}
(hT : ∀ (X : C), Nonempty (T ⟶ X))
:

If `C`

has (small) wide equalizers and a weakly initial object, then it has an initial object.

The initial object is constructed as the wide equalizer of all endomorphisms on the given weakly initial object.