Instances on pempty

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

theorem AddSemigroupPEmpty.proof_1 (x : PEmpty.{u_1 + 1} ) (y : PEmpty.{u_1 + 1} ) (z : PEmpty.{u_1 + 1} ) : x + y + z = x + (y + z)

instance AddSemigroupPEmpty : AddSemigroup PEmpty.{u + 1}

instance SemigroupPEmpty : Semigroup PEmpty.{u + 1}