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))
:
If F : C ⥤ D is such that F.obj X is terminal for any X : C,
then F is a terminal object.
Equations
Instances For
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))
:
If F : C ⥤ D is such that F.obj X is initial for any X : C,
then F is an initial object.