Subsingleton elimination and impredicativity for SProp, Prop and hProp#55

Open

herbelin wants to merge 4 commits intocoq:masterfrom herbelin:subsingleton-elimination

+220

Commits on Mar 4, 2021

Proposal on subsingleton elimination and hProp
herbelin
committed
Take Gaëtan's remark into account (prod are already de facto recognized in Prop for subsingleton elimination thanks to impredicativity).
herbelin
committed

Commits on Mar 5, 2021

Reformulating the document:
herbelin
committed

Commits on Jul 11, 2021

More comments
herbelin
committed