fact: Record EqSignature (S : OpSignature) := { eq :> Type ; eq_arity : eq → Type ; lhs : ∀ (A : OpAlgebra S) (e : eq), (eq_arity e → A) → A ; rhs : ∀ (A : OpAlgebra S) (e : eq), (eq_arity e → A) → A ; lhs_natural : ∀ (A B : OpAlgebra S) (f : AlgHom A B) (e : eq) (args : eq_arity e → A), f (lhs A e args) = lhs B e (fun i => f (args i)) ; rhs_natural : ∀ (A B : OpAlgebra S) (f : AlgHom A B) (e : eq) (args : eq_arity e → A), f (rhs A e args) = rhs B e (fun i => f (args i)) ; }.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian