  This document provides a formal proof of Birkhoff's completeness theorem for
multi-sorted algebras which states that any equational entailment valid in all
models is also provable in the equational theory.
  More precisely, if a certain equation is valid in all models that validate a
fixed set of equations, then this equation is derivable from that set using the
proof rules for a congruence.
  The proof has been formalized in Agda version 2.6.2 with the Agda Standard
Library version 1.7 and this document reproduces the commented Agda code.
