Just some information for those of you relying on MetaCoq:
we finally have all the cumulative inductive type theory formalized, it does enjoy subject reduction, "weak" principality and does not invalidate elimination principles needed for erasure.
we didn't find a way yet to extended the formalisation with eta-conversion. As such our first "beta" release will not have it, and I'll remove the "todoeta" axioms that appear here and there.
the metatheory of pcuic is otherwise admit-free.
once this cleanup is done I'll release a beta package (working with ocaml 4.10 hopefully).
Matthieu Sozeau (Sep 15 2020 at 19:31):