There's a well-known line of research into the equiconsistency of set-theoretical and type-theoretical foundations, with many compelling results. So you actually can do "reverse mathematics" of type-theoretical foundations. You aren't losing anything.