fact: Record Object (sign: Signature) : Type := object { algebra_carriers:> sorts sign → Type ; algebra_equiv: ∀ a, Equiv (algebra_carriers a) ; algebra_ops: AlgebraOps sign algebra_carriers ; algebra_proof: Algebra sign algebra_carriers }.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.theory.categories