Initial and terminal objects in the category of functors

We show that if a functor F : C ⥤ D is such that F.obj X is terminal for all X, then F is a terminal object.

def CategoryTheory.Functor.isTerminal {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} (hF : (X : C) → Limits.IsTerminal (F.obj X)) : Limits.IsTerminal F

If F : C ⥤ D is such that F.obj X is terminal for any X : C, then F is a terminal object.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Functor.isInitial {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F : Functor C D} (hF : (X : C) → Limits.IsInitial (F.obj X)) : Limits.IsInitial F

If F : C ⥤ D is such that F.obj X is initial for any X : C, then F is an initial object.

Equations

• One or more equations did not get rendered due to their size.