Displayed universal algebra in UniMath: basic definitions and results

Univalent mathematics and homotopy type theory provide a structural approach to formalizing mathematical concepts. Inspired by the role of displayed categories in the univalent treatment of category theory, we develop an analogous notion of displayed algebras for universal algebra. This modular and layered approach allows us to construct and reason about algebraic structures over a fixed base. Classical constructions such as cartesian products, pullbacks, semidirect products, and subalgebras naturally arise as total algebras of suitable displayed algebras. The main results are fully formalized in the UniMath library.