<div dir="ltr">Hi,<div>This past Monday, we spent all of the time on exercise 8.2:</div><div>Prove that if A is a set with decidable equality (see Definition 3.4.3), then its suspension ΣA is a 1-type. (It is an open question whether this is provable without the assumption of decidable equality.)</div>
<div><br></div><div>We eventually got to the point where we had the idea to define the free product of A\{a} copies of the integers as a higher inductive type, and try to use the encode-decode method to prove equivalence with the path space of ΣA; this fails by begging the question, because the free product group requires a truncation axiom, which we cannot send to anywhere unless we already know that ΣA is a 1-type.</div>
<div><br></div><div>Here is a solution, I believe: If A has decidable equality, then we can define the free (product) group as a (non-higher-) inductive type, such that the laws are derivable, rather than assumed: we define the carrier to be canonical words, and we define the group operation to be list-append followed by canonicalization (canonicalization on lists of elements is a computable function precisely because A has decidable equality). Then we can use the encode-decode method, and I think everything goes through.</div>
<div><br></div><div><br></div><div><br></div><div>Next week, we will continue with chapter 8.</div><div><br></div><div>Next week will be our last meeting this year. The following two weeks, I will be in Paris at the Formalization of mathematics in proof assistants workshop and the TYPES conference, so we will not be meeting. After that, MIT's semester is over, and we no longer have the room reserved. If there's interest, I'd probably be happy to run the group again starting in the fall, starting from Chapter 8 or Chapter 9.</div>
<div><br></div><div>-Jason</div></div>