I'm not quite sure what a "strict proposition" is, but if you mean
having a type of propositions that doesn't include all of them, then
the reason that's not enough for me is that frequently in univalent
type theory we encounter types that we *prove* to be propositions even
though they are not "given as such", such as "being contractible" and
"being a proposition", and this is responsible for a significant
amount of the unique flavor and usefulness of univalent type theory.

For semantic reasons I wouldn't want to use intuitionistic set theory,
because it doesn't naturally occur as the internal language of
categories.  You can perform contortions to model it therein, but that
involves interpreting it into type theory rather than the other way
around.  I don't know what you mean by "somehow clean it up into a
type system", but if you can do that cleaning up and obtain a type
theory (a "formal type theory" in Bob Harper's sense, not a
"computational type theory", i.e. one that is inductively generated by
rules rather than assigning types to untyped terms in an "intended
semantics"), then I'd like to see it.