A set theory formalization in Agda.
Published in Working paper, 2017
Recommended citation: A. Calle-Saldarriaga. (2017). "A Set Theory Formalization." Tech. Report. Universidad EAFITs. https://acallesalda.github.io/files/settheoryagda.pdf
Abstract: A set theory formalization in agda. Our main goal was to prove the induction property. See the github repository: https://github.com/acallesalda/setform.
A bit of context: during my undergrad I was quite interested in logic and formalization of mathematics, and this report (together with the premise selection work in the talks section) came out of that period. Formalizing the Zermelo axioms and some theorems in a dependently typed language was a very cool job, and it taught me a lot about being precise. I am not working on anything related to this nowadays, but I still keep a soft spot for it.