Ssreflect Users Discussion List

[Andrej Bauer <>]

> Well, I full agree with you on that point and I'm currently working on this
> matter. In order to begin as quickly as possible, I started from a patched
> version of Coq v8.3 (with the patches that can be found in the Foundation
> repository) and I modified (in a very ugly way for now) the ssr1.4_v8.3
> plugin to make it work in the univalent setting. I also converted the most
> basic ssr libraries and began to formalize the beginning of the foundation
> from it, in a ssreflect style (mainly to understand it).
>
> I will make my early development available on github anytime now (even if I
> think it will not match your expectations since I work with coq v8.3 right
> now) ... As for the proper ssr library, Enrico's answer coincides with what
> I expected.

Ah great! And we have Assia here so she can help. But please note that
the Foundations library is likely to get ported to HoTT and that most
effort is going into HoTT. Think of HoTT as a "Foundations library
cleaned up". So if we could have the basic ssr stuff working in HoTT
that would be excellent. We're making people recompile Coq already, so
a bit of additional plugin compilation won't hurt that much.

To answer Assia's question: yes, the HoTT library does not use the
standard library because we redefine equality (or to put it better, it
does not land in Prop). So we want to be careful about putting things
back in, but we will of course put back in anything that is ok with
the new interpretation. I was forced to get rid of the standard
library because it would not compile at all with the new
interpretation of inductive types. I don't think there is anything
problematic in Bool.v.

With kind regards,

Andrej