Bas Spitters
Bas Spitters
I agree. It seems better to generalize this to general instances.
I'm fine with the changes, but propose to wait until the discussion in coq/coq#10760 stabilizes.
Perhaps take the files at the bottom of these hierarchies: https://math-classes.github.io/ E.g. https://github.com/coq-community/math-classes/blob/master/theory/dec_fields.v https://github.com/coq-community/math-classes/blob/master/interfaces/orders.v
Yes, that seems like the right solution.
Doesn't #138 just mean that we cannot reflect SProp. Is there anything standing in the way of making this more limited version of metacoq compile with HoTT? Currently SProp is...
@mattam82 @SkySkimmer would this be a viable approach?
Did you consider also join semilattices? Perhaps as an meet semilattice on the opposite order.
It's done using duality in Corn. The HoTT library has duality for categories. What are the issues in math-comp? On Sun, Apr 26, 2020 at 8:52 PM Kazuhiko Sakaguchi wrote:...
I don't think that has been done, so a PR would be welcome.