agda-structures Formalizing the mathematics of relational, algebraic, and general structures in type theory and Agda