Your indexing is off :) Propositions (or 'facts' as you call them) are the (-1)-types, whereas 0-types are usually referred to as sets. A way to remember this is that the path-spaces (i.e. equalities) in a set are propositions, bringing you one level down.
While you're right that "proof relevance" is one of the key features of HoTT, I don't agree that what's being described here "is the HoTT point of view". Any mathematical proof bears on techniques that may be interesting beyond the proven result itself; HoTT doesn't clarify or elucidate that, nor does it aim to.
> I don't agree that what's being described here "is the HoTT point of view".
I am no expert in HoTT, so I certainly defer to what sounds like your expertise here. I should probably have said something closer to the weaker statement "this reminds me of HoTT", which hopefully is not incorrect—although you're right that what I really had in mind was proof relevance.
While you're right that "proof relevance" is one of the key features of HoTT, I don't agree that what's being described here "is the HoTT point of view". Any mathematical proof bears on techniques that may be interesting beyond the proven result itself; HoTT doesn't clarify or elucidate that, nor does it aim to.