ezyang’s blog

the arc of software bends towards understanding

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