On 04/03/2021 22:05, Michael Shulman wrote:
> 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?

I'm not sure what the precise thing is that you're looking for because, 
without further specification, any standard definition of Z would 
qualify :-)
The HIT is neat, but wouldn't it in practice behave pretty similar to a 
standard representation via binary lists? E.g. something like Unit + 
Bool * List(Bool), where inl(*) is zero, the first Bool is the sign, and 
you add a 1 in front of the list in order to get a positive integer. 
What's the advantage of the HIT - maybe one can avoid case distinctions?
Nicolai

-- 
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/58a0a515-d8fa-4eb2-9555-d3a41fdee728%40gmail.com.