Category theory is a general language for reasoning about mathematical structures, their behaviors, and their relationships with other structures. The goals of this talk are twofold: to introduce the fundamental concepts from category theory and to enable writing machine-checked proofs by formalizing the concepts in the dependently typed programming language Agda. Along the way, we’ll see a few techniques to keep the code manageable and coherent as we use and expand our newfound powers.