From HoTT Require Import Foo. fails with several Foo's about coq-hott

[Alizter]

Hi, you need to pass -noinit and -indices-matter to Coq in order to use HoTT. See the README.md. You can do this by putting

-arg -noinit
-arg -indices-matter

in your _CoqProject file.

The reason this is failing is because HoTT is incompatible with the Coq standard library which is loaded implicitly. If the -noinit argument is passed to Coq then it is not loaded.

-indices-matter is about the universe level of inductive types, which in order to be consistent with univalance, needs to be enabled.

When I try the jscoq example it works, mostly because -noinit is setup to be passed correctly. If you are trying this on your own in a project then set up _CoqProject as I indicated above. If are simply passing this to an editor, then you can pass -noinit and -indices-matter directly.

[SnarkBoojum]

Oh, my bad! Thanks, that settles the matter with me, I can proceed on getting it into Debian.

Thanks!