A Computer-Checked Library of Category Theory