  We present recent updates in our development of a library for Universal
Algebra in the UniMath proof assistant. The code here discussed concerns
multi-sorted signatures and their algebras, along with the basics for equation
systems. Moreover, we give neat constructions of the corresponding univalent
categories by using the formalism of displayed categories, and show that the
term algebra over a signature is the initial object of the category.
  Besides the formalization, we reflect on the methodological principles --
based on the idea of evaluability of our elementary construction by the
built-in normalization procedure of the system -- leading our coding style, and
show that this path is practicable indeed by sketching simple examples.
