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 (reformatted to match the Software Foundations presentation):
Inductive eq1 {X:Type} (x:X) : X -> Prop :=
refl_equal1 : eq1 x x.
What’s the difference? The trick is to look at the induction principles that Coq generates for each of these:
Read more...
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 these have been test solved.
You will need HoTT/coq in order to run this development; instructions on how to install it are here.
Read more...
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 to read a math textbook, so don’t expect detailed technical commentary from non-authors for a while.
Of course, being a puny grad student, I was, of course, most interested in the book’s contribution of yet another Martin-Löf intuitionistic type theory introduction, e.g. chapter one. The classic introduction is, of course, the papers that Martin Löf wrote (nota bene: there were many iterations of this paper, so it’s a little hard to find the right one, though it seems Giovanni Sambin’s notes are the easiest to find), but an introduction of type theory for homotopy type theory has to make certain adjustments, and this makes for some novel presentation. In particular, the chapter’s discussion of identity types is considerably more detailed than I have seen elsewhere (this is not surprising, since identity is of central importance to homotopy type theory). There is also a considerable bit of pedantry/structure in the discussion of the types that make up the theory, reminiscent of the PFPL (though I believe that this particular chapter was mostly written by others). And, of course, there are many little variations in how the theory is actually put together, expounded upon in some detail in the chapter notes.
Read more...