mathlibdocumentation

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.

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