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