HoTT in prose

Posted on 5 December 2011 by Carlo Angiuli

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 $\pi_1(S^1)=\mathbb{Z}$ .

Here’s the PDF. (Added section 4, 3/26/12.)

This entry was posted in Uncategorized. Bookmark the permalink.

13 Responses to HoTT in prose

andrejbauer says:

5 December 2011 at 16:30

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 $P(a \leadsto b) = (x \leadsto a) \to (x \leadsto b)$ can be written out in full as $P (a, b, s) = (x \leadsto a) \to (y \leadsto b)$ where $s : a \leadsto b$ . (I agree it is better to just write $P (a \leadsto b) = \cdots$ or maybe $P (s : a \leadsto b) = \cdots$ , but want to be sure I understand your definition.) We plug in $a = y$ , $b = z$ and $s = q$ , use $J$ -elimination with respect to $p : x \leadsto y$ to get $a = b = x$ , and then we plug in $id_x$ .

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 $p : a \leadsto b$ . Then it suffices to show it for $p = id_a : a \leadsto a$ . Now we proceed to the proof of Propostion 1.1. We do not mention any fibrations, we just say: by induction on $p$ it suffices to consider the case $x = y$ and $p = id_x$ . But then the desired path from $x$ to $z$ is simply $q$ . Would that be ok?

Reply
- Carlo Angiuli says:
  
  5 December 2011 at 18:38
  
  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 $q:y\leadsto z$ to yield a function $(x\leadsto y)\to (x\leadsto z)$ , and applying that function to $p:x\leadsto y$ , to yield $pq$ .
  
  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 $P$ is suitable: it’s inhabited at each $id_a$ , so $P(q)$ is inhabited, and that term applied to $p$ is $pq$ . In the proof you give, what is the fibration explicitly?
  
  Reply
Mike Shulman says:

6 December 2011 at 13:52

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 $p : a \leadsto b$ . Then it suffices to show it for $p = id_a : a \leadsto a$ ” 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 $p : a \leadsto b$ 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 $p : a \leadsto b$ and $q : b \leadsto c$ , a path $a \leadsto c$ . By path-induction, it suffices to do this when $p$ is an identity. But in thus case, we can take the result to be $q$ .”

When speaking to someone less familiar with induction, I might say something like this: “We want to construct, for any paths $p : a \leadsto b$ and $q : b \leadsto c$ , a path $a \leadsto c$ . That means that we want to construct, for any path $p : a \leadsto b$ , an operation which takes any path $b \leadsto c$ to a path $a \leadsto c$ . Thus, for fixed $c$ , consider the fibration over $Paths_A$ whose fiber over $p : a \leadsto b$ is the space of maps $(b \leadsto c) \to (a \leadsto c)$ . We want a section of this fibration, and by path-induction it suffices to construct such a section in the case when $a=b$ and $p$ is an identity. However, in this case, we can take the inhabitant of $(b \leadsto c) \to (a \leadsto c)$ 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 $p : a \leadsto b$ and $q : b \leadsto c$ , a path $a \leadsto c$ . By path-induction, it suffices to do this when $p$ and $q$ are identities. But in thus case, we can take the result to also be an identity.”

Reply
- Carlo Angiuli says:
  
  6 December 2011 at 14:27
  
  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.
  
  Reply
- Mike Shulman says:
  
  7 December 2011 at 01:35
  
  One of my frustrations with the Coq proofs is that they rely heavily on induction even when a simple, more meaningful proof exists.
  
  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 $\infty$ -groupoid structure of a type are proven in the same way (by performing induction on all relevant paths).
  
  Reply
  - Carlo Angiuli says:
    
    8 December 2011 at 00:36
    
    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.
    
    Reply
    - Mike Shulman says:
      
      9 December 2011 at 12:24
      
      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.
      
      Reply
- Urs Schreiber says:
  
  7 December 2011 at 10:36
  
  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.”
  
  Reply
  - Mike Shulman says:
    
    7 December 2011 at 22:37
    
    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.
    
    Reply
Bas Spitters says:

8 December 2011 at 15:25

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

Reply
Carlo Angiuli says:

26 March 2012 at 01:03

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.

Reply
- Mike Shulman says:
  
  26 March 2012 at 16:40
  
  The comparison is nice! But I don’t understand what you mean by “reduces some propositional equalities to definitional ones”.
  
  Reply
  - Carlo Angiuli says:
    
    26 March 2012 at 20:06
    
    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.
    
    Reply