Introducing displayed universal algebra in UniMath

This paper presents a formalisation of displayed algebras within UniMath, extending the displayed-category framework to universal algebra. We establish that algebras displayed over a base structure correspond to morphisms into that base, enabling modular development of algebraic constructions. The approach is illustrated through natural examples -- including products, pullbacks, and subalgebras -- and all results are mechanised within univalent foundations. We outline future work integrating this framework more deeply into UniMath and exploring connections with Lawvere theories.