[HoTT-reading-group] This week 4/21; remaining meetings

[Jason Gross]

Hi,
This past Monday, we spent all of the time on exercise 8.2:
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.)

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.

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.



Next week, we will continue with chapter 8.

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.

-Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140424/ced1f726/attachment.htm