Bas Spitters
Bas Spitters
That sounds great.
This turns out to be easier in cubical type theory. [PDF](https://www.cs.au.dk/~spitters/Emil.pdf).
I recall that they were just slow. @limemloh will confirm. In fact, I believe performance even improved with a later version of agda. @tlringer Exciting. I'm looking forward to your...
Precisely, this should be a way to get better proof terms. On Thu, Sep 11, 2014 at 7:41 PM, Jason Gross [email protected] wrote: > Why? Anytime we don't want to...
In fact, this can be one step towards a computational interpretation of univalence, we can see to what extend we can push through all the uses of equiv. On Fri,...
Here's something that allows rewriting with ``. it's probably not complete, but I'd like to check whether there is an interest in this. I've been quite aggressive removing things from...
There are some here. Any requests for the kinds of example you'd like to see? https://github.com/spitters/HoTT/blob/setoidrewrite/setoidtest.v
That seems reasonable. Although I don't have a strong opinion on it. There are a number of people building on the library, but not contributing to it. E.g. https://github.com/HoTT/HoTT/wiki/Publications-based-on-the-HoTT-library (...
https://mattam82.github.io/Coq-Equations/
Do you or @cmangin (or @SkySkimmer for that matter) have any plans of doing that in the future. HoTT seems to be an ideal application for Equations.