# mathlibdocumentation

topology.category.Top.limits

def Top.limit_cone {J : Type u} (F : J Top) :

A choice of limit cone for a functor F : J ⥤ Top. Generally you should just use limit.cone F, unless you need the actual definition (which is in terms of types.limit_cone).

Equations
def Top.limit_cone_is_limit {J : Type u} (F : J Top) :

The chosen cone Top.limit_cone F for a functor F : J ⥤ Top is a limit cone. Generally you should just use limit.is_limit F, unless you need the actual definition (which is in terms of types.limit_cone_is_limit).

Equations
@[instance]

@[instance]

Equations
def Top.colimit_cocone {J : Type u} (F : J Top) :

A choice of colimit cocone for a functor F : J ⥤ Top. Generally you should just use colimit.coone F, unless you need the actual definition (which is in terms of types.colimit_cocone).

Equations
def Top.colimit_cocone_is_colimit {J : Type u} (F : J Top) :

The chosen cocone Top.colimit_cocone F for a functor F : J ⥤ Top is a colimit cocone. Generally you should just use colimit.is_colimit F, unless you need the actual definition (which is in terms of types.colimit_cocone_is_colimit).

Equations
@[instance]

@[instance]

Equations