This is confusing; you are using `T` twice.  I would write this as `Type -> hProp` (`hProp` is defined in `HProp.v`), or `Type -> { T : Type & IsHProp T }` if you're absolutely wedded to sigma types.  Alternatively, you could define two fields, `subuniverse_predicate : Type -> Type` and `ishprop_subuniverse_predicate : forall T, IsHProp (subuniverse_predicate T)`.