I would suggest calling this something other than `O`.  You also have the option to split it into two fields, one for the type, and another for the proof.  Finally, if you use `subuniverse_HProp : Type -> hProp`, then you won't need the `.1` here, as there's a coercion `hProp -> Type`.