HoTT HITs

[Andrej Bauer]

Dear all,

we have Agda-style higher-inductive types in coq. Thanks to Yves
Bertot, Michael Nahas and Mike Shulman for setting things up. You will
have to recompile Coq to get Yves's changes. If you are an existing
HoTT user, you should

1. Switch to the stable branch of HoTT/coq. From within your copy of HoTT/coq:

git pull
git checkout stable

Then rebuild Coq, probably as follows:

./configure -local
make clean
make coqlight

If you have a dual core or better use insetad 'make -j 2 coqlight'

2. Update your HoTT to get theories/HIT/hit directory, i.e., from your
copy of HoTT/HoTT:

git pull
make clean
make

I will let someone else explain how the hits are implemented.

With kind regards,

Andrej