Re: [HoTT] two's complement integers

[Martin Escardo <escardo.martin@gmail.com>]

On 04/03/2021 22:05, Michael Shulman wrote:
> On Thu, Mar 4, 2021 at 1:11 PM Martin Escardo <escardo.martin@gmail.com> wrote:
>> I wonder if your definition of the integers with the HIT is isomorphic
>> to an inductively defined version without a HIT as above, and this is
>> how you proved it to be a set.
> 
> No, I just did an encode-decode.  I formalized most of it, up to some
> obviously true lemmas about squares and cubes.
> 
> I thought for a little bit about whether there is an equivalent
> "lower" inductive version, but nothing immediately occurred to me.  Do
> you have a suggestion?


For example, take ℤ' = ℕ + ℕ and define the functions you have in your
hit and prove the equations you have in your HIT.

Then using the HIT universal property you get a function from your ℤ to
this ℤ', and conversely you define a function from ℤ' to ℤ "manually".

This is what Alex Rice and I did to prove that our 𝔹 and 𝔹' are
equivalent. The cubes don't disappear completely, of course. But there
were much fewer cubes than when we tried to prove directly that 𝔹 is a
set, and we gave up because the code was getting too long and
unpleasant, with too many cases to check. The indirect version was much
shorter and pleasing.

Martin




-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8f4c4a68-dbe0-055b-3462-3230cd09c86f%40gmail.com.