Allow subgroups to be defined by predicates that don't take values in h-props

[jdchristensen]

As discussed in #2035:

I think it would also be helpful to allow a subgroup of a group to be defined with a predicate that isn't assumed to take values in h-propositions. This would avoid us needing to strip_truncations and apply tr in various places, and would mean that we don't need a separate ab_cokernel_embedding, since ab_cokernel would already not need truncation.

But we also want the concept of subgroups where the predicate does land in h-props, since some statements are only true in that case. (E.g. equiv_path_subgroup and ishset_subgroup.)

However, I think that most statements won't need this extra condition. I'm not exactly sure how to structure things.