Some progress in [HoTT_light.v].
Some progress in [HoTT_light.v].

There are still some bugs with universes in Equations.
See for instance the first FIXME in the file.
Also, Equations does not handle well for now the elimination
of equalities such as [f x = x].
See the second FIXME.

mattam82/Coq-Equations,clarus/Coq-Equations,mattam82/Coq-Equations