fact: Record Object (et: EquationalTheory) : Type := object { variety_carriers:> sorts et → Type ; variety_equiv: ∀ a, Equiv (variety_carriers a) ; variety_ops: AlgebraOps et variety_carriers ; variety_proof: InVariety et variety_carriers }.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms