Formalization of Mathematical Logic

We formally assessed four different algebraic descriptions of classical propositional logic. We defined categories of algebras, where objects are algebras and morphisms are algebra homomorphisms. We defined a subcategory for the first three with the restriction that logically equivalent propositions are equal. We showed that all four categories are equivalent. We also showed the completeness of subset algebras for boolean algebras. All of the results were formalized in the proof assistant Agda