Properties for the HITs? about cubical HOT 5 CLOSED

I don't understand this comment. What are you asking for?

from cubical.

In the stdlib, we have functions (plus, minus, divmod, times) for different number types (Nat, Int, Conat). These are missing in this library -- there's only succ, pred and various conversion functions.

from cubical.

Yes, so far I've only been focusing on proving that the various HIT encodings of int are equivalent to nat + nat. This should allow us to transport all the theory from nat + nat to the HIT encodings using univalence. It might also be interesting to directly develop some theory for the HIT encodings just to see how it is to program and prove with them. Anyway, I'm closing this issue now as it is not very concrete.

from cubical.

Currently I can't define + for HitInt due to agda/agda#3314. Otherwise I'll create a PR for this :(

from cubical.

@Saizan What is the status of the above issue?

Regardless of the above bug, it might still be interesting to transport some functions from nat + nat and try to compute with them.

from cubical.