Bas Spitters
Bas Spitters
@mortberg did you ever review this fix? It would be nice to have a correct implementation of truncation.
I believe this is a problem that [lean4](https://arxiv.org/pdf/2001.04301.pdf) is trying to solve. @mattam82 This may be a good test case.
We have more annotations now. I guess this can be closed?
@mattam82 Did you ever open this CEP?
Where's the branch?
For comparison. [Here](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html) is an example of literate HoTT in agda. I guess for a better comparison with agda, we might also want Equations to work for HoTT.
Quick response. Yes, that's what ssr does. There is also the decide equality tactic which is used in software foundations/logical foundations. On Wed, Apr 21, 2021 at 1:48 PM Ali...
This [paper by Altenkirch and Scoccolla](http://luisscoccola.github.io/Luis%20Scoccola_files/int-as-hit.pdf) may be relevant
That's my understanding. We should probably wait until it gets moved to trunk, but I wanted to record the fact that it's there. On Mon, Mar 9, 2015 at 8:05...
The algorithm already works on stdlib, cpdt and math-comp. Testing it on HoTT would probably be interesting, but I will wait a bit before doing it myself. On Tue, Mar...