  The Agda Universal Algebra Library (UALib) is a library of types and programs
(theorems and proofs) we developed to formalize the foundations of universal
algebra in dependent type theory using the Agda programming language and proof
assistant.
  The UALib includes a substantial collection of definitions, theorems, and
proofs from universal algebra, equational logic, and model theory, and as such
provides many examples that exhibit the power of inductive and dependent types
for representing and reasoning about mathematical structures and equational
theories. In this paper, we describe the the types and proofs of the UALib that
concern homomorphisms, terms, and subalgebras.
