Instances on pempty #
This file collects facts about algebraic structures on the (universe-polymorphic) empty type, e.g. that it is a semigroup.
Equations
- SemigroupPEmpty = { mul := fun (x x_1 : PEmpty.{?u.1 + 1}) => PEmpty.casesOn (fun (t : PEmpty.{?u.1 + 1}) => x = t → PEmpty.{?u.1 + 1}) x ⋯, mul_assoc := SemigroupPEmpty._proof_1 }
Equations
- One or more equations did not get rendered due to their size.