Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda.