abstr.tex

\prefacesection{Abstract}
Building a standard library of mathematical knowledge for a proof system is a
complex task that relies on human effort. By conducting a survey on the standard library
of four proof systems (Agda, Idris, Lean, and Coq), we define the scope for our
research to study types of algebraic structures in proof systems. From the
result of the survey, we establish our focus to contribute to the Agda standard
library. 

Universal algebra studies structures by abstracting out the specific definitions
and properties of algebraic structures. Providing an extensive and well-defined
library of algebraic structures and theorems in Agda will enable researchers to
explore new domains and build upon existing definitions (and theorems). We
explore capturing a select subset of algebraic structures such as quasigroups,
loops, semigroups, rings, and Kleene algebra with some of their constructs.
Constructs like homomorphism, isomorphism and direct products are given to us by
universal algebra which provides a way to relate different structures in a
systematic and rigorous way. Homomorphisms allow us to understand how different
structures are related.

During our exploration of capturing these structures in Agda, we encountered
several issues. We categorized these issues into five classes and analyzed each
problem to provide plausible solutions. As part
of this research, we define more than 20 algebraic structures and add more than
40 proofs to the Agda standard library