I had a limited interest in exploring type theories for their own sake some time ago but it receded when I was unable to resolve, or find a resolution to, a conceptual problem that seems extremely foundational.

Each type theory has a hierarchy of types: 1-types, 2-types, 3.1*10^62-types, etc. but some niche type theories allow for types indexed by transfinite ordinals: ω-types, ω+5-types, I even found a construction of a theory that supports φ_α-types. There is apparently at least one very counterintuitive type theory where the hierarchy of indexable types provably continues past the proof-theoretic ordinal of the theory, somehow, but I haven't seen it myself.

These have real implications of what kinds of proofs you can do with a given type theory.

.

The problem is deciding which of these theories to permit, or possibly even deciding how to decide which theories to permit, if you'll pardon the pun. I decided to give it up and get back to PDEs.