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}
[category_theory.small_category J]
{F : J ⥤ category_theory.discrete punit}
{c : category_theory.limits.cone F} :
Any cone over a functor into punit is a limit cone.
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} :
Any cocone over a functor into punit is a colimit cocone.
@[instance]
Equations
- category_theory.limits.category_theory.limits.has_limits = {has_limits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_limit := λ (F : J ⥤ category_theory.discrete punit), {cone := category_theory.limits.category_theory.limits.has_limits._aux_3 J F, is_limit := {lift := category_theory.limits.category_theory.limits.has_limits._aux_4 J F, fac' := _, uniq' := _}}}}
@[instance]
Equations
- category_theory.limits.category_theory.limits.has_colimits = {has_colimits_of_shape := λ (J : Type u_1) (𝒥 : category_theory.small_category J), {has_colimit := λ (F : J ⥤ category_theory.discrete punit), {cocone := category_theory.limits.category_theory.limits.has_colimits._aux_3 J F, is_colimit := {desc := category_theory.limits.category_theory.limits.has_colimits._aux_4 J F, fac' := _, uniq' := _}}}}