Instances on PUnit

This file collects facts about ordered algebraic structures on the one-element type.

instance PUnit.canonicallyOrderedAdd : CanonicallyOrderedAdd PUnit.{u_1 + 1}

instance PUnit.isOrderedCancelAddMonoid : IsOrderedCancelAddMonoid PUnit.{u_1 + 1}

instance PUnit.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop PUnit.{1}

Equations

• One or more equations did not get rendered due to their size.