Carette, J., & Hu, J. (2021). Formalizing Category Theory in Agda. https://doi.org/10.1145/3437992.3439922