search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

+Int≡+ #1028

Closed timorl closed 1 year ago

timorl commented 1 year ago

This is more of a warmup, since I actually want ·Int≡· (useful to prove QuoQ≡HITQ I think?). But this might also prove useful to prove that, so no effort wasted.

I'm aware of some problems with this, but I'm not sure how to fix them, so I'll be grateful for any comments.

  1. The import looks ridiculous and I'm pretty sure it's not conformant with the contribution guidelines. However, I wasn't able to figure out how to write it in any other way and have all this still work (as imports still cause conflicts I think?).
  2. I'm not sure whether the changes to Iso are ok or if there is a better way of doing a similar thing. Similarly, exporting isoIntℤ might be controversial?
  3. I think at least some of the reasoning should be private, but I'm not sure what the best way of achieving this is – private is kinda obvious, but I think I've also seen some unnamed modules? What should I do with this?
  4. The big comment in line 298 – is this something worth pursuing? Within this PR?
  5. In general I have a feeling there might be a much simpler way of doing all this...
timorl commented 1 year ago

I also privated a lot of the PR after all, I think they are pretty irrelevant.

felixwellen commented 1 year ago

Thanks! Looks all good to me now -> will merge if CI is happy.