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.

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

Instances For