Constructing the Propositional Truncation using Nonrecursive HITs

Posted on 28 July 2015 by Floris van Doorn

In this post, I want to talk about a construction of the propositional truncation of an arbitrary type using only non-recursive HITs. The whole construction is formalized in the new proof assistant Lean, and available on Github. I’ll write another blog post explaining more about Lean in August.

The construction of the propositional truncation of a type $A$ is as follows. Let $\{A\}$ be the following HIT:

HIT {-} (A : Type) : Type :=
| f : A → {A}
| e : ∀(a b : A), f a = f b

I call this the “one step truncation”, because the HIT is like the propositional truncation, but takes out the recursive part. Martin Escardo calls this the generalized circle, since $\{\mathbf{1}\} \simeq S^1$ . We can repeat this multiple times: $A_0 :\equiv A$ and $A_{n+1} :\equiv \{A_n\}$ . Now the colimit $A_\infty$ of this sequence is the propositional truncation of $A$ : $A_\infty \simeq \| A \|$ . To make sure we’re on the same page, and to introduce the notation I use for the constructors, the (sequential) colimit is the following HIT: (I will mostly leave the arguments in $\mathbb{N}$ implicit)

HIT colimit (A : ℕ → Type)
  (f : ∀(n : ℕ), A n → A (n+1)) : Type :=
| i : ∀(n : ℕ), A n → colimit A f
| g : ∀(n : ℕ) (a : A n), i (f a) = i a

Below I’ll give an intuition of why the construction works, and after that a proof. But first I want to talk about some consequences of the construction.

First of all this is the first instance of a HIT which has a recursive path constructor which has been reduced to non-recursive HITs. During the HoTT workshop in Warsaw there was a conjecture that all HITs with recursive (higher) path constructors can be reduced to HITs where only point constructors are allowed to be recursive. Although I have no idea whether this conjecture is true in general, this is the first step towards proving it.

Secondly, this gives an alternative answer to the question about the universal property of the propositional truncation. This construction shows that (using function extensionality) a function $h : \|A\| \to B$ for an arbitrary type $B$ is “the same” as a sequence of functions $h_n : A_n \to B$ (with $A_n$ defined above) such that for all $a : A_n$ we have $h_{n+1}\ (f\ a) = h\ a$ . In a formula

$(\|A\| \to B)\ \simeq\ (\Sigma(h : \Pi n, A_n \to B), \Pi (n : \mathbb{N}) (a : A_n), h_{n+1}\ (f\ a) = h_n\ a)$ .

So, why does the construction work?
To give an intuition why this works consider the propositional truncation of the booleans, $\|2\|$ . Of course, this type is equivalent to the interval (and any other contractible type), but there is actually a little more going on. The path constructor of the propositional truncation (let’s call it $e'$ here) gives rise to two paths between $0_2$ and $1_{2}$ : $e'\ |0_{2}|\ |1_{2}|$ and $(e'\ |1_{2}|\ |0_{2}|)^{-1}$ . Since the resulting type is a mere proposition, these paths must be equal. We can construct a path between them explicitly by using the continuity of $e'$ . We can prove that for every $x : \|2\|$ and every $p : |0_2| = x$ we have $p = (e' \ |0_{2}|\ |0_{2}|)^{-1}\cdot e' \ |0_{2}|\ x$ by path induction, and this leads to the conclusion that any two elements in $|0_2| = |1_{2}|$ are equal. This is exactly the proof that any proposition is a set.

Now consider the type $\{2\}$ . This is a type with points $a:\equiv f\ 0_2$ and $b:\equiv f\ 1_2$ and we have two paths from $a$ to $b$ . Let’s call them $p:\equiv e\ 0_2\ 1_2$ and $q:\equiv(e\ 1_2\ 0_2)^{-1}$ . These two paths are not equal. Of course, we also have a loop at both $a$ and $b$ .
However, in the type $\{\{2\}\}$ the corresponding paths $\text{ap}_f\ p$ and $\text{ap}_f\ q$ of type $f\ a = f\ b$ are equal. To see this, we can mimic the above proof. We can prove that for all $x : \{2\}$ and all $p : a = x$ we have $\text{ap}_f\ p = (e\ a\ a)^{-1} \cdot e\ a\ x$ , just by path induction on $p$ . Then we can conclude that $\text{ap}_f\ p = \text{ap}_f\ q$ . Of course, in $\{\{2\}\}$ there are new paths of type $f\ a = f\ b$ , but they will be identified again in $\{\{\{2\}\}\}$ .

<sidenote>
The above argument also shows that if any function $f$ is weakly constant, then $\text{ap}_f : x = y \to f\ x = f\ y$ is weakly constant for any $x,y$ (using the terminology of this post).
</sidenote>

So this is the intuition why $A_\infty$ is the propositional truncation of $A$ . In $\{A\}$ a path is added between any two points of $A$ , between any two existing parallel paths (and between any two parallel higher paths). Then in $\{\{A\}\}$ higher paths are added between all newly introduced (higher) paths, and so on. In the colimit, paths exist between any two points, parallel paths, and parallel higher paths, so we get the propositional truncation.

The proof.
But this is just the intuition. How do we prove that we get the propositional truncation? We clearly get the point constructor for the propositional truncation, because $i_0$ (the constructor of the colimit) has type $A \to A_\infty$ . Now we still have to show two things:

We have to show that $A_\infty$ is a mere proposition
We have to construct the induction principle for the propositional truncation on $A_\infty$ , with the judgmental computation rule

2. The second part is easy. If we’re given a family of propositions $P : A_\infty \to \text{Prop}$ with a map $h : \Pi(a : A), P\ (i_0\ a)$ we have to construct a map $k : \Pi(x : A_\infty), P\ x$ . We do this by induction on $x : A_\infty$ . Since we construct something in $P\ a$ , which is a mere proposition, the path construction is automatic, and we only have to deal with the case that $x\equiv i_n\ a$ for some $n : \mathbb{N}$ and $a : A\ n$ . Now we do induction on $n$ .
If $n\equiv0$ , we can choose the element $h\ a : P\ (i_0\ a)$ .
If $n\equiv k+1$ , we know that $a : \{A_k\}$ , so we can induct on $a$ . If $a\equiv f\ b$ , we need an element of $P\ (i_{n+1}\ (f\ b))$ . We have an element of $P\ (i_n\ b)$ by induction hypothesis. So we can transport this point along the equality $(g_n\ b)^{-1} : i_n\ b = i_{n+1}\ (f\ b)$ to get the desired point. The path construction is again automatic. In pattern matching notation we have defined:

$k\ (i_{0}\ a) :\equiv h\ a$ and
$k\ (i_{n+1}\ (f\ b)) :\equiv (g_n\ b)^{-1}_*(k\ (i_n\ b))$ .

The definition $k\ (i_{0}\ a) :\equiv h\ a$ is also the (judgmental) computation rule for the propositional truncation.

1. So we only need to show that $A_\infty$ is a mere proposition, i.e. $\Pi(x\ y : A_\infty), x = y$ . We first do induction on $x$ . Note that $\Pi(y : A _\infty), x = y$ is a mere proposition. (Left as exercise to the reader. Hint: assume that it is inhabited.) So we only have to consider the case where $x$ is a point constructor, say $x\equiv i_n\ a$ . Now we do induction on $y$ . Now the goal is $i_n\ a = y$ , and we don’t know (yet) that this is a mere proposition, so we have to show two things:

We have to construct a $p\ a\ b : i_n\ a = i_m\ b$ for all $n,m,a,b$ ;
We have to show that $p$ satisfies the following coherence condition: $p\ a\ (f\ b)\ \cdot\ g_m\ b = p\ a\ b$ .

In particular, we want to make the construction of $p$ as simple as possible, so that the coherence condition for $p$ remains doable.

For the construction of $p$ , let’s first consider a special case where $a$ and $b$ live in the same level, i.e. where $n \equiv m$ . This will be used in the general construction. In this case, we have $i_n\ a = i_{n+1}\ (f\ a) = i_{n+1}\ (f\ b) = i_n\ b$ , where the second equality is by the path constructor $e$ of $\{A_n\}$ and the other two equalities are by the path constructor $g$ of the colimit. Let’s call this equality $q\ a\ b : i_n\ a = i_n\ b$ .

For the general construction of $p$ with arbitrary $n$ and $m$ , I have considered three approaches. I will first discuss two approaches where I failed to complete the proof.

(failed) Approach 1. Induct on both $n$ and $m$ . In the successor case, induct on $a$ and $b$ . Unfortunately, this becomes horrible very quickly, because we now have a nested double induction on HITs. This means that we already need to prove coherence conditions just to construct $p$ , and after that we still need to show that $p$ satisfies a coherence condition. I quickly gave up on this idea.

(failed) Approach 2. Lift $a$ and $b$ both to $A\ (n + m)$ by repeatedly applying $f$ , and then show that $i_n\ a = i_{n+m}\ (f^m\ a) = i_{n+m}\ (f^n\ b) = i_m\ b$ , where the second equality is $q\ (f^m\ a)\ (f^n\ b)$ . This works, but there is a catch: $f^m\ a$ lives in $A (n + m)$ and $f^n\ b$ lives in $A (m + n)$ (assuming addition is defined by induction on the second argument). So to complete the construction, we also have to transport along the equality $n+m=m+n$ . This is fine, but for the coherence condition for $p$ this transport becomes an annoying obstacle. Showing the coherence condition is possible, but I didn’t see how to do it. Then realized there was a more convenient approach, where I didn’t have to worry about transports.

(succeeded) Approach 3. Distinguish cases between $n\le m$ and $m \le n$ and induct on those inequalities. I’m assuming that the inequality is defined by an (ordinary) inductive family

inductive le (n : ℕ) : ℕ → Type :=
| refl : le n n
| step : Π(m : ℕ), le n m → le n (m+1)

This definition gives a very useful induction principle for this construction. If $H : m\le n$ we can construct a map $f^H : A\ m \to A\ n$ by induction on $H$ :

$f^{\text{refl}_n}\ a:\equiv a$ ;
$f^{\text{step}\ H}\ a:\equiv f\ (f^H\ a)$ .

I use the notation $f^H$ for this, similar to $f^n$ , because we repeatedly apply $f$ and the number of times is determined by $H$ . Since the type $m \le n$ is a mere proposition, $f^H$ doesn’t really depend on $H$ , only on the fact that its type $m \le n$ has an inhabitant.
We can now also show that $g^H\ b : i_n\ (f^H\ b) = i_m\ b$ by induction on $H$ as concatenation of multiple $g$ s. Now if $H : m \le n$ we can construct $p\ a\ b$ by $i_n\ a = i_n\ (f^H\ b) = i_m\ b$ , where the first equality is $q\ a\ (f^H\ b)$ . The case $n \le m$ is similar.

This is a nice and simple construction of $p$ (without transports), and we can prove the coherence conditions using this definition, but that is more involved.

We have constructed $p$ in such a way that for $H : n \le m$ we have that $p\ a\ b$ equals $(g^H\ a)^{-1}\ \cdot\ q\ (f^H\ a)\ b$ and in the case that $H : m \le n$ we have that $p\ a\ b$ equals $q\ a\ (f^H\ b)\ \cdot\ g^H\ b$ . This is not purely by definition, for the case $n = m$ we have to prove something here, because we cannot get both inequalities by definition.

Now we have to show that $p\ a\ (f\ b)\ \cdot\ g_m\ b = p\ a\ b$ . We distinguish two cases: $n > m$ and $n \le m$ .

Case $n > m$
In this case we can find $H : m+1 \le n$ and $H' : m \le n$ . In this case $p\ a\ b = q\ a\ (f^{H'}\ b)\ \cdot\ g^H\ b$ and $p\ a\ (f\ b) = q\ a\ (f^{H}\ (f\ b))\ \cdot\ g^H\ (f\ b)$

The situation is displayed below (click image for larger view). Some arguments of paths are omitted, and the maps $i$ and $\text{ap}_i$ are also omitted for readability (the actual equalities live in $A_\infty$ ). We need to fill the pentagon formed by the outer (thick) equalities.

By induction on $H$ we can find a path $r : f^{H'}\ b = f^H\ (f\ b)$ and by another induction on $H$ we can fill the bottom square in the diagram. We will skip the details here. The top triangle can be filled for a general path $r$ by induction on $r$ . This finishes the case $n > m$ .

Case $n \le m$
Now we can find $H : n \le m$ and $H' : n \le m+1$ . Here $p\ a\ b = (g^H\ a)^{-1}\ \cdot\ q\ (f^H\ a)\ b$ and $p\ a\ (f\ b) = (g^{H'}\ a)^{-1}\ \cdot\ q\ (f^{H'}\ a)\ (f\ b)$ . The situation is below.

If we choose $H'$ correctly (namely as $\text{step}\ H$ ), then by definition $f^{H'}\ a\equiv f\ (f^H\ a)$ and $g^{H'}\ a\equiv g\ (f^H\ a)\ \cdot\ g^H\ a$ , so the triangle in the left of the diagram is a definitional equality. We can prove the remaining square in more generality. See the below diagram, where we mention $i$ explicitly.

The bottom square is filled by induction on $p$ . To show that the two paths in the top are equal, first note that $i_{k+1} : A_{k+1} \to A_\infty$ is weakly constant, because that is exactly the type of $q$ . So $\text{ap}_i : f\ x = f\ y \to i\ (f\ x) = i\ (f\ y)$ is weakly constant. This finishes the case $n \le m$ , and hence the proof that $A_\infty$ is a mere proposition.

Future Work
The natural question is whether we can construct arbitrary $n$ -truncations using non-recursive HITs. The construction in this post can be easily generalized by using an “one-step $n$ -truncation,” but the proof that the resulting type is $n$ -truncated cannot be generalized easily. However, Egbert Rijke has a proof sketch of the construction of localizations between $\omega$ -compact types using nonrecursive HITs, and these include all the $n$ -truncations.

This entry was posted in Code, Higher Inductive Types. Bookmark the permalink.

25 Responses to Constructing the Propositional Truncation using Nonrecursive HITs

Martin Escardo says:

28 July 2015 at 17:36

This is very nice! In particular, it gives an answer to the following question: Suppose you want to eliminate $\left\Vert A \right \Vert \to B$ using a function $A \to B$ . What should the function $A \to B$ satisfy? At least, it should be weakly constant. Your answer is that it is enough to exhibit a cocone whose first leg is the function $A \to B$ . The second leg gives the weak constancy of $A \to B$ . Then the other legs give the weak constancy of the previous legs. We may call such a function $A \to B$ “coherently constant” if it can be completed to such a cocone. Then your answer is that we can eliminate $\left\Vert A \right \Vert \to B$ using a coherently constant function $A \to B$ .

Question: We know that we can eliminate $\left\Vert A \right\Vert \to A$ using any weakly constant function $A \to A$ (so that we don’t need to give all coherence data when $B=A$ ). There are at least two explanations of this. Does your work give a third explanation?

Reply
- Floris van Doorn says:
  
  28 July 2015 at 18:09
  
  Your comment about coherently constant functions is exactly right.
  
  To answer your question: Yes! I do not know either of the other two explanations, so I can’t compare my argument with them. Can you provide a link?
  
  Using this construction: Suppose we’re given a weakly constant function $A \to A$ . This corresponds exactly to a function $\{A\} \to A$ . By functoriality of $\{{-}\}$ we get a map $\{\{A\}\} \to \{A\}\to A$ and similarly by induction a map $h_n : A_n \to A$ . These maps do indeed form a cocone, the equality $h_{n+1}\ (f\ a)=h_n\ a$ is true by reflexivity. So this gives a map $\|A\|\to A$ .
  
  Reply
  - Martin Escardo says:
    
    28 July 2015 at 19:04
    
    Nice again! Just a corollary of your development.
    
    Here are the links you want:
    
    The first explanation is by Nicolai Kraus: The type of fixed points of any weakly constant endomap is a proposition,
    http://www.cs.nott.ac.uk/~ngk/docs/hedberg.pdf,
    from which the claim follows almost directly.
    
    The second explanation is the same, with a different argument for the fact that the type of fixed points is a proposition, by Christian Sattler, recorded in page 19 of
    
    Click to access existence.pdf
    
    Reply
  - Nicolai Kraus says:
    
    29 July 2015 at 20:22
    
    Oh, this is great! (And thanks to Martin for giving the links to our previous work!)
    
    Reply
Martin Escardo says:

28 July 2015 at 19:27

Another question is this: Nicolai has an alternative notion of coherently constant function with the same elimination property: http://arxiv.org/abs/1411.2682
I wonder how this relates to your work.

Reply
- Floris van Doorn says:
  
  29 July 2015 at 11:07
  
  Here is a comparison of the resulting universal property you get.
  
  The disadvantage of my universal property is that it is “useless” when eliminating to $n$ -types. That is: the universal property is not easier when assuming that the codomain is an $n$ -type; you still have to construct a cocone over the whole diagram. In Nicolai’s work you only have to check finitely many things when eliminating to an $n$ -type.
  
  Nicolai also had an idea where in the $n$ -th step of the diagram you only add $n$ -dimensional paths, so that $A_n$ becomes $n$ -connected. If that works, this gives a nice universal property when eliminating to $n$ -types.
  
  The advantage of my work is that it is possible to formulate the general universal property (without assuming that the codomain is an $n$ -type) inside type theory, without assuming that the type theory has Reedy limits. And that it has been formalized in a proof assistant.
  
  In neither case it is clear how useful the universal property is in applications; i.e. how bothersome it is to construct all the required data.
  
  Reply
  - Mike Shulman says:
    
    29 July 2015 at 11:26
    
    The universal property for eliminating to sets can be obtained by noting that $\Vert \{A\}\Vert_0 = \Vert A\Vert_{-1}$ . If it were true that $\Vert A_{n+1} \Vert_n = \Vert A\Vert_{-1}$ as well, then that would also give a universal property for eliminating to $n$ -types; but it sounds from your comment like maybe that is not the case?
    
    Reply
    - Floris van Doorn says:
      
      29 July 2015 at 11:45
      
      You’re right, for eliminating to sets this construction does work.
      
      However, in this construction, $\Vert A_{n+1} \Vert_n = \Vert A\Vert_{-1}$ is indeed not true for larger $n$ . At every step we’re adding new 1-paths, and only the next step corresponding 2-paths are added equating those 1-paths which are parallel, so $A_n$ is not $n$ -connected, even if it is inhabited.
      
      Nicolai’s idea of an alternative construction (which I mentioned in my previous comment) will have this property, so can be used for this.
      
      Reply
    - Mike Shulman says:
      
      29 July 2015 at 12:01
      
      Intriguing. This seems kind of similar to my splitting-idempotents construction; in both cases we seem to get something “fully coherent” and involving paths of all dimensions without ever talking about anything above dimension 1. Of course we’ve seen that before, e.g. in the hub-and-spoke construction and even in Vladimir’s original definition of contractibility, but somehow it is more surprising to me that these two constructions work.
      
      Reply
    - Mike Shulman says:
      
      29 July 2015 at 17:35
      
      Ah, I have a better idea what’s happening now. For any $A$ there is a map $\{A\} \to S^1$ which sends all the f-points to base and all the e-paths to loop. As long as A is inhabited, this map hits loop with an endo-path, which is therefore nontrivial. So there is no way $\{A\}$ could ever be 1-connected. And yet each new 1-path added in $A_n$ gets killed in $A_{n+1}$ , so in the colimit they all die. This makes the fact that the colimit ends up propositional more plausible to me than when I was imagining that the connectedness simply increases at every step.
      
      Reply
      - Nicolai Kraus says:
        
        29 July 2015 at 20:28
        
        This makes the fact that the colimit ends up propositional more plausible to me than when I was imagining that the connectedness simply increases at every step.
        
        Yes, Floris’ construction is very clever at that point! So clever that I also found it surprising when I heard it the first time. But I do think that the approach where the connectedness increases at every step works as well (see my longer comment below). It’s true that the argument for that construction would be much easier if we had a “general Whitehead” at hand, but we can do it without (at least, that’s what I currently believe).
        
        Reply
        
        Mike Shulman says:
        
        29 July 2015 at 22:06
        
        Maybe the conclusion to draw is that I still don’t really understand what the world looks like when Whitehead’s principle fails, for all that I talk about it a lot.
        
        Reply
  - Mike Shulman says:
    
    29 July 2015 at 11:30
    
    Here’s a possible test case for usefulness of these universal properties. In the proof of Lemma 8.2 in this paper (formalized in Coq here), I used the universal property for eliminating out of $\Vert A\Vert$ into sets. That necessitated a restriction in the lemma statement that $P$ be a family of sets (which was sufficient for what I needed at the time). But can the more general universal properties be used to generalize this lemma?
    
    Reply
    - Nicolai Kraus says:
      
      29 July 2015 at 20:29
      
      Oh, that’s interesting. I hope I can find some time to look at that. Thanks for the pointer.
      
      Reply
Mike Shulman says:

29 July 2015 at 00:16

Indeed, very nice! At first I didn’t think that this would work, because in general a type can be n-connected for all n without being contractible; but somehow the sequential colimit takes care of that. I’m still dubious that one can get arbitrary localizations; does Egbert assume some kind of compactness of the generators?

Another question: can your notion of “coherently constant function” be defined without using the one-step-truncation HIT, and if so, can one show directly that it suffices to eliminate from the propositional truncation?

Reply
- Floris van Doorn says:
  
  29 July 2015 at 10:52
  
  You’re completely right about the localizations. Egbert assumes that the types for the localization are $\omega$ -compact. I clarified it in the article.
  
  Your other question is interesting. I don’t know. To get it, you probably want to give the universal property of $A_n$ , but I don’t even see how to get the universal property of $\{\{A\}\}$ . I’ll think about it!
  
  Reply
Nicolai Kraus says:

29 July 2015 at 20:20

This is a very interesting construction, and a nice write-up!
For me, it’s especially interesting how you prove that $A_{\infty}$ is a mere proposition. I would have attempted to do it like this:
1. to show $\mathsf{isProp}(A_\infty)$ , it’s enough to show $A_\infty \to \mathsf{isContr}(A_\infty)$ .
2. because $\mathsf{isContr}(A_\infty)$ is propositional, it is relatively easy to see that $A \to \mathsf{isContr}(A_\infty)$ suffices.
3. given $a : A$ , we then want to show that $i_0 a$ is a centre of contraction.
That way, we really only need to do induction on one variable at a time. Maybe it could simplify things a tiny bit, but I think I understand why you didn’t do it: the easy case is if the two points in $A_\infty$ that we want to prove equal come from the same $A_n$ , i.e. $i_n a = i_n b$ is much easier that $i_0 a = i_n b$ . For comparison, in the other approach that you mentioned in the comments, this is not the case.
(You have described very well what this approach is, but maybe it’s confusing to link between comments like this, so, let me quickly say what I mean. The approach for constructing truncations that Thorsten and I wanted to take is to start with $A$ , then take the 1-step [-1]truncation, then take the 1-step 0-truncation of the result, then take the 1-step 1-truncation of that result, and so on. Then, it’s really true that $\Vert A_n \Vert_{n-1}$ is the correct thing, so it would simplify if we want to eliminate into $n$ -types – but it’d probably be more complicated otherwise.)
I think I have a proof on paper for that construction, but at the moment not formalised and there could be all kind of flaws (maybe I’ll write a blog post, but only if I manage to find a nice presentation). This approach has its own difficulties, because even reducing the goal to $i_n a = i_n b$ won’t help much; I really need to go all the way down to $i_0 a = i_0 b$ , because “level zero” is the only time where we get actual equalities between points.

Reply
- Floris van Doorn says:
  
  30 July 2015 at 08:40
  
  This idea is great! It doesn’t “simplify things a tiny bit”, it cuts the length my proof in half! If I can assume that $A$ is inhabited by $a$ , then I can choose $i_0\ a$ as my center of contraction, and then I only have to worry about other points which are in a *higher* level than $a$ . So this makes the whole case $n > m$ obsolete. Moreover, there’s no need to induct on inequalities anymore, we can just induct on ordinary natural numbers. I implemented your proof strategy:
  https://github.com/fpvandoorn/leansnippets/blob/master/short_prop_trunc.hlean
  The proof that $A_\infty$ is a mere proposition went down from ~163 to ~76 lines.
  
  I feel a bit stupid that I didn’t see this myself. I was already thinking that if I could assume that $A$ is inhabited, things would be easier. I also thought about your first step, but I didn’t see how assuming a point in $A_\infty$ could help: you cannot construct a point in $A_n$ or even $A$ from it. However, you can actually do that if you are proving only a mere proposition.
  
  Reply
  - Nicolai Kraus says:
    
    1 August 2015 at 10:12
    
    Great to see this implemented! I have used this strategy in a couple of other cases before, it’s often useful when you want to prove that some HIT is n-truncated.
    The general strategy goes like this: To prove that $X$ is an $n$ -type (for $n \geq -1$ ), it’s enough to show $\mathsf{forall }\, x:X, \mathsf{isContr}(\Omega^{n+1}(X,x))$ . But, if $X$ is some HIT, then you can show this by induction on $x$ , and, because you’re proving a mere proposition, all you need to check are the point-constructors. All higher constructors are automatic.
    There are also some simple strategies to show something of the form $\mathsf{isContr}(\Omega^{n+1}(X,x))$ (basically some higher versions of Hedberg’s argument), I have written about that in my thesis (Thm 3.2.1 summarises some of these “tools”, they are all trivial to prove; in Chp 8.10 in an application).
    
    Reply
    - Mike Shulman says:
      
      6 August 2015 at 00:04
      
      Does this technique make it easier to prove that $S^\infty$ is contractible (with either definition of $S^\infty$ )? (Luis Scoccola has recently submitted solutions to the two exercises in the book about this, 8.3 and 8.4.)
      
      Reply
      - Nicolai Kraus says:
        
        12 August 2015 at 18:09
        
        Good question, but I don’t see how it might help for $S^\infty$ (as a colimit). I think it’s the other way round: If you have a more difficult problem, you can try that strategy to reduce it to a problem which looks similar to “colimit – $S^\infty$ is contractible”. For example, in Floris’ construction, it essentially gives you this point in the “starting type” $A_0$ , and you already have such a point (or two) in the “starting type” $S^0$ . For “ $S^\infty$ as its own suspension”, I also don’t think it can be used.
        
        Reply
        
        Mike Shulman says:
        
        12 August 2015 at 18:48
        
        I see. Too bad.
        
        Reply
Pingback: The Lean Theorem Prover | Homotopy Type Theory
Pingback: Colimits in HoTT | Homotopy Type Theory
Pingback: Reflexive graph quotients are pushouts | Egbert RIJKE