I recently reengaged w/ a wonderful band of hackworthy humans doing some very cool things in Agda. I needed to dust off my Agda coding skills and remember how to interact w/ its proof assistant and needed a focal point. Just before leaving my last job, we’d been reading Conal Elliott’s The Simple Essence of Automatic Differentiation. So, I decided that I’d try proving some of the isomorphisms Conal reveals in that paper, in Agda.

You can view my work here: Agda Proofs.