Code-along for Categories for the Working Mathematician [Coq]