Style nit/question: Is there a particular reason to ask for a single sigma as a hypothesis (`Q`) rather than two hypotheses (`Q : Type` and `H : subuniverse_HProp Q` (or similar))?