fact: Record Algebra (S : OpSignature) (E : EqSignature S) := { alg :> OpAlgebra S ; equations : ∀ (e : E) (args : eq_arity e → alg), lhs e args = rhs e args }.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian