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.