There's a well-known line of research into the equiconsistency of set-theoretica...

		zozbot234 on March 27, 2022 \| parent \| context \| favorite \| on: With Category Theory, Mathematics Escapes from Equ... 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.