Comment by blueberry87

What are your other options? A type-based proof system implies dependent types, implies universe levels if you want it to be consistent.