fact: Record OpAlgebra (S : OpSignature) := { carrier :> Type ; op : ∀ o : operation S, (arity o → carrier) → carrier }.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian