Inside 214-1E

Existential Pontification and Generalized Abstract Digressions

HoTT exercises in Coq (in progress)

I spent some of my plane ride yesterday working on Coq versions of the exercises in The HoTT book. I got as far as 1.6 (yeah, not very far, perhaps I should make a GitHub repo if other folks are interested in contributing skeletons. Don't know what to do about the solutions though). All of […]

  • July 1, 2013