I'm working on presenting an extension of MLTT which uses a (from what I can tell) novel conception of type universes which I believe is not equivalent to the standard Russell/Tarski-style approaches.
However, before I further develop this idea, I'd like to have a simple argument for its consistency, and am not sure how I should proceed. Eventually, I'd like to give a ordinal analysis of this type theory, but I am not very experienced in ordinal analysis, so this would be rather involved for me and I'd like to have a simpler way of establishing consistency.
Besides ordinal analysis, my other two methods were either:
- Find a translation from my type theory to some other type theory believed to be consistent.
- Formalize my type theory as a first order (second order?) theory and find a model in ZFC.
I think (1) requires more insight than I currently have into the nature of this type theory, as I don't think a translation is possible into standard MLTT, or MLTT with universes indexed over $\omega$, so out of my own ideas, (2) seems to be the best option, which leaves me with the question:
Is there a standard way of formalizing type theories as first order (or perhaps second order) theories, or at least examples of this having been done fruitfully in the literature?
Beyond this, I'd also like to know if there are any other feasible approaches for relatively easy approaches for showing the consistency of a type theory.