mathlib documentation

category_theory.limits.punit

discrete punit has limits and colimits #

Mostly for the sake of constructing trivial examples, we show all (co)cones into discrete punit are (co)limit (co)cones, and discrete punit has all (co)limits.

source
def category_theory.limits.punit_cone_is_limit {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.discrete punit} {c : category_theory.limits.cone F} :
category_theory.limits.is_limit c

Any cone over a functor into punit is a limit cone.

Equations
source
def category_theory.limits.punit_cocone_is_colimit {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.discrete punit} {c : category_theory.limits.cocone F} :
category_theory.limits.is_colimit c

Any cocone over a functor into punit is a colimit cocone.

Equations
source
@[protected, instance]
def category_theory.limits.category_theory.discrete.has_limits  :
category_theory.limits.has_limits (category_theory.discrete punit)
source
@[protected, instance]
def category_theory.limits.category_theory.discrete.has_colimits  :
category_theory.limits.has_colimits (category_theory.discrete punit)