the arc of software bends towards understanding
In Software Foundations, equality is defined in this way: Even Coq's equality relation is not built in. It has (roughly) the following inductive definition. Inductive eq0 {X:Type} : X -> X -> Prop := refl_equal0 : forall x, eq0 x x. Why the roughly? Well, as it turns out, Coq defines equality a little differently […]
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 […]
In what is old news by now, the folks at the Institute for Advanced Study have released Homotopy Type Theory: Univalent Foundations of Mathematics. There has been some (meta)commentary (Dan Piponi, Bob Harper, Andrej Bauer, François G. Dorais, Steve Awodey, Carlo Angiuli, Mike Shulman, John Baez) on the Internet, though, of course, it takes time […]