Instances on pempty

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

ink

def AddSemigroupPEmpty.proof_1 (x : PEmpty) (y : PEmpty) (z : PEmpty) : x + y + z = x + (y + z)

Equations

• (_ : x + y + z = x + (y + z)) = (_ : x + y + z = x + (y + z))

ink

instance AddSemigroupPEmpty : AddSemigroup PEmpty

Equations

• AddSemigroupPEmpty = AddSemigroup.mk AddSemigroupPEmpty.proof_1

ink

instance SemigroupPEmpty : Semigroup PEmpty

Equations

• SemigroupPEmpty = Semigroup.mk SemigroupPEmpty.proof_1