One more HIT Int about cubical HOT 4 CLOSED

This is inspiring me to finish a port of redprl's biinv-int that I started last year (https://github.com/m-yac/cubical/tree/biinv-int). It adds the following HIT equivalent to Int:

data BiInvInt : Type₀ where
  zero : BiInvInt
  suc : BiInvInt -> BiInvInt
  -- suc is a bi-invertible equivalence:
  predr : BiInvInt -> BiInvInt
  suc-predr : ∀ z -> suc (predr z) ≡ z
  predl : BiInvInt -> BiInvInt
  predl-suc : ∀ z -> predl (suc z) ≡ z

A close cousin of this type is mentioned* in the linked slides as an example of the other way to solve the 'truncation problem' -- adding coherences. I think these twos HITs would complement one another well.

* What Thorsten actually states is hard to work with, I tried and failed to prove it equivalent to Int and it seems others have too: https://github.com/agda/cubical/blob/master/Cubical/Experiments/HInt.agda

from cubical.

It would be great to have both the truncated and untruncated (based on biinv-int) versions in the library. So please make PRs.

The version from Thorsten's slides is indeed a nightmare to work with and I only pushed what worked to the HInt file. I tried many different approaches to filling those holes, but it always led straight to coherence hell.

from cubical.

@mortberg Should I put my variant into Cubical.HITs.IntTrunc ?

from cubical.

from cubical.