# mathlibdocumentation

category_theory.limits.unit

# 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. We also show that such (co)cones exist, and that discrete punit has all (co)limits.

def category_theory.limits.punit_cone {J : Type v} {F : J } :

A trivial cone for a functor into punit. punit_cone_is_limit shows it is a limit.

Equations
def category_theory.limits.punit_cocone {J : Type v} {F : J } :

A trivial cocone for a functor into punit. punit_cocone_is_limit shows it is a colimit.

Equations
def category_theory.limits.punit_cone_is_limit {J : Type v} {F : J }  :

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

Equations

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

Equations