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 CategoryTheory.Limits.punitCone {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} : Cone F

A trivial cone for a functor into PUnit. punitConeIsLimit shows it is a limit.

Equations

• CategoryTheory.Limits.punitCone = { pt := { as := PUnit.unit }, π := (((CategoryTheory.Functor.const J).obj { as := PUnit.unit }).punitExt F).hom }

def CategoryTheory.Limits.punitCocone {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} : Cocone F

A trivial cocone for a functor into PUnit. punitCoconeIsLimit shows it is a colimit.

Equations

• CategoryTheory.Limits.punitCocone = { pt := { as := PUnit.unit }, ι := (F.punitExt ((CategoryTheory.Functor.const J).obj { as := PUnit.unit })).hom }

def CategoryTheory.Limits.punitConeIsLimit {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} {c : Cone F} : IsLimit c

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

Equations

• CategoryTheory.Limits.punitConeIsLimit = { lift := fun (s : CategoryTheory.Limits.Cone F) => CategoryTheory.eqToHom ⋯, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.punitCoconeIsColimit {J : Type v} [Category.{v', v} J] {F : Functor J (Discrete PUnit.{u_1 + 1})} {c : Cocone F} : IsColimit c

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

Equations

• CategoryTheory.Limits.punitCoconeIsColimit = { desc := fun (s : CategoryTheory.Limits.Cocone F) => CategoryTheory.eqToHom ⋯, fac := ⋯, uniq := ⋯ }

instance CategoryTheory.Limits.instHasLimitsOfSizeDiscretePUnit : HasLimitsOfSize.{v', v, u_1, u_1} (Discrete PUnit.{u_1 + 1})

instance CategoryTheory.Limits.instHasColimitsOfSizeDiscretePUnit : HasColimitsOfSize.{v', v, u_1, u_1} (Discrete PUnit.{u_1 + 1})