metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

Published 20 hours ago • verified publisher icon MetaCoq

Compatibility with HoTT

Open annenkov opened this issue 5 years ago • 5 comments

It would be nice to make MetaCoq compatible with the HoTT library (https://github.com/HoTT/HoTT). I know that @andreaslyn would be interested in this kind of compatibility. I guess, making translations to work with HoTT would be already nice, the rest (like CIC meta-theory and extraction) is probably not needed to be compatible. Of course, this requires at least to resolve #138 first.

annenkov avatar May 20 '19 12:05 annenkov

What incompatibilities are there? Is this an issue with the translations or with the core meta-coq infrastructure?

gmalecha avatar May 20 '19 13:05 gmalecha

I guess, the first thing is that HoTT library builds with the dev version of Coq and MetaCoq is not compatible with the dev version of Coq currently.

annenkov avatar May 20 '19 13:05 annenkov

The HoTT library relies on Coq version >= 8.10. So at least issue https://github.com/MetaCoq/metacoq/issues/138 is standing in the way of making metacoq compatible with HoTT.

andreaslyn avatar May 20 '19 21:05 andreaslyn

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 not used in HoTT.

spitters avatar May 29 '19 17:05 spitters

@mattam82 @SkySkimmer would this be a viable approach?

spitters avatar Jun 03 '19 13:06 spitters