Instances on pempty

This file collects facts about algebraic structures on the (universe-polymorphic) empty type, e.g. that it is a semigroup.

@[implicit_reducible]

instance SemigroupPEmpty : Semigroup PEmpty.{u + 1}

@[implicit_reducible]

instance AddSemigroupPEmpty : AddSemigroup PEmpty.{u + 1}