I have adapted some basic HoTT theorems and proofs to prose form, in an attempt to better understand the results and their proofs. The Coq proof scripts often obscure details of the exposition, like the choice of fibration in an induction tactic, or run the argument backwards in a mathematically awkward way. At times they also duplicate proofs that are completely symmetric, or choose an easily mechanizable but somewhat unnatural argument.
Of course these are all matters of taste, but I at least thought it would be worth a try to “mathematize” the arguments and notation. (I have nothing against Coq proofs except that they’re not well-suited for human consumption!) I think the result is pretty readable, and Dan Licata has pointed out that this could be a useful resource for anyone interested in porting these proofs to a different system.
The file covers results from path concatenation through function extensionality. I closely follow Andrej Bauer’s Coq proof scripts, which are in turn based on Voevodsky’s. I have taken minor liberties and invented some notation. (Does anyone have better notation for transport?) I’m hoping to continue adding results to this file, starting with Mike Shulman’s proof of 
Here’s the PDF. (Added section 4, 3/26/12.)
Homotopy Type Theory 
Quite interesting. I am not sure I understand the proof of Proposition 1.1 (concat). Let me see if I understand it. First, the definition
can be written out in full as 
where 
. (I agree it is better to just write 
or maybe 
, but want to be sure I understand your definition.) We plug in 
, 
and 
, use 
-elimination with respect to 
to get 
, and then we plug in 
.
I would phrase this differently. I would first explain how to prove things “by induction on a path”: suppose we want to show that property $P$ of paths in a given space holds for a particular path
. Then it suffices to show it for 
. Now we proceed to the proof of Propostion 1.1. We do not mention any fibrations, we just say: by induction on 
it suffices to consider the case 
and 
. But then the desired path from 
to 
is simply 
. Would that be ok?
Your understanding of the definition is correct. Remark 1.1 is an abbreviated explanation of induction on paths, but I agree it should be explained more carefully. I’m not sure about your explanation of the proof though; I’m using J-elimination with respect to
to yield a function 
, and applying that function to 
, to yield 
.
In particular, I’m emphasizing the fact that induction on paths (i.e., J-elimination) is done with respect to some fibration, and the fibration I give explicitly as
is suitable: it’s inhabited at each 
, so 
is inhabited, and that term applied to 
is 
. In the proof you give, what is the fibration explicitly?
This is great. I have always believed that we need to learn to speak about these proofs in natural language, both for purposes of understanding and communication, and so that we can learn to think in this language when looking for new proofs. There are certainly a lot of choices to be made in how one speaks, however. In general, I tend to favor Andrej’s approach, which doesn’t mention fibrations explicitly when constructing something by induction — but on the other hand, thinking about the fibration is sometimes important when formalizing the proof, and it is probably also helpful for beginners not as familiar yet with path-induction.
I also think Andrej’s phrasing “suppose we want to show that property P of paths in a given space holds for a particular path
. Then it suffices to show it for 
” is subtly misleading to the newcomer. I would say instead “suppose we want to show that property P of paths in a given space A holds for all paths 
in A. Then…” I think Andrej’s phrasing would lead naively to acceptance of the K rule.
I would also phrase this particular proof in terms of constructing a path, rather than proving a fact, since the path-space is not necessarily a proposition. So I would phrase the proof as follows when speaking to someone familiar with induction: “We want to construct, for any paths
and 
, a path 
. By path-induction, it suffices to do this when 
is an identity. But in thus case, we can take the result to be 
.”
When speaking to someone less familiar with induction, I might say something like this: “We want to construct, for any paths
and 
, a path 
. That means that we want to construct, for any path 
, an operation which takes any path 
to a path 
. Thus, for fixed 
, consider the fibration over 
whose fiber over 
is the space of maps 
. We want a section of this fibration, and by path-induction it suffices to construct such a section in the case when 
and 
is an identity. However, in this case, we can take the inhabitant of 
to be the identity map.”
Actually, though, that isn’t the proof that appears in the Coq file! That one goes like this (for the expert): “We want to construct, for any paths
and 
, a path 
. By path-induction, it suffices to do this when 
and 
are identities. But in thus case, we can take the result to also be an identity.”
Thanks! The proofs get less exacting later in the file; I wanted to be very explicit in the first few uses of induction. Your penultimate paragraph is precisely the proof I give, but phrased more clearly.
One of my frustrations with the Coq proofs is that they rely heavily on induction even when a simple, more meaningful proof exists. But since Coq constructs the fibration automatically, induction is certainly the path of least resistance.
Are you referring to my final paragraph? I don’t think of either of these proofs as more meaningful than the other; can you explain?
The proof that only performs induction on one of the paths has the disadvantage of being asymmetric, but the advantage that concatenation with an identity on one side is definitionally equal to the identity map. For the latter reason, some people have advocated using it instead. But I dislike the asymmetry involved; I think I like it better if all the basic lemmas that give the
-groupoid structure of a type are proven in the same way (by performing induction on all relevant paths).
In this case, I think either proof is reasonable. But, being the first use of induction in the file, I feel like using induction twice is a bit confusing, especially because it avoids the explicit identity map construction. But symmetry is a fair argument, too.
I was particularly referring to proofs later on in the file, where performing induction on every path is sufficient to yield the desired path, but there exists a simple, explicit construction with an intuitive geometric meaning. In particular, compare my proof for concat_cancel_right with the Coq proof. Nothing’s morally wrong with the inductions; it’s just harder to get any intuition from such a construction.
Perhaps one moral of the inductive definition of equality is that we should teach our intuition to be satisfied with a proof of the form “it suffices to consider the case when all paths are identities, in which case it is trivial.” After all, our undergraduates sometimes have to teach their intuitions to be happy with proofs by ordinary induction on natural numbers; so it’s not out of the question for our intuitions to need retraining.
I’m not sure whether I think that, but it’s an intriguing viewpoint. It seems perhaps related to Adam Chlipala’s oft-made argument that (my words, not his) any proof that can be automated can’t give us very much intuition anyway, and therefore should be automated.
Hi Mike,
you suggest something like
“Suppose we want to show that property P of paths in a given space A holds for all paths, then it suffices to show it for the identity path.”
We talked about it before. I think it must read
“Suppose we want to show that property P of paths in a given space A holds for all paths AND is equivariant with respect to path composition, then it suffices to show it for the identity path.”
But any property of paths which makes sense for all paths is necessarily equivariant with respect to path composition, since a “property” means a fibration. When we’re talking internally (even in prose), we don’t have to mention equivariance explicitly.
There used to be a way to transform coq terms into natural language:
http://www-sop.inria.fr/lemme/personnel/Yann.Coscoy/index-en.html
There is also this more recent work
Click to access jar_plmms.pdf
I’ve added a section with the proof that the interval implies function extensionality, and a detailed comparison with the proof that univalence implies the same. My current understanding is that, by allowing one to reduce equivalences to the identity function, univalence (via “equivalence induction”) reduces some propositional equalities to definitional ones. More details in the new link.
The comparison is nice! But I don’t understand what you mean by “reduces some propositional equalities to definitional ones”.
I couldn’t think of a better way of phrasing it. Essentially, if f, g witness an equivalence then (f o -), (g o -) should witness an equivalence. Without univalence this amounts to needing to show \x. f (g x) ~~> \x. x, given that \x. (f (g x) ~~> x), but we cannot reduce this propositional equality under the binder. With univalence we must simply show \x. id x ~~> \x. x, which reduces definitionally (under the binder!). At this point in the proof of function extensionality, univalence actually hands us an instance of extensionality.