@TimothyChow : Adding various amounts of choice, excluded middle, and impredicativity is just as easy, if not easier, in type theory as in set theory. As to type-theoretic Big Five equivalents, I'm afraid this margin is too small to really elaborate, but yes, “relatively easy” for the most part: Basic type theory is ca. ACA₀, a hierarchy of universes bumps to ATR₀, adding W-types lands you in the vicinity of Π¹₁–CA₀. It's slightly trickier to go below towards finitism and RCA₀/WKL₀, but there's work in that direction by Herbelin and Patey. I think polytime systems are also doable, but harder.

@TimothyChow : well, type theory incorporates finite type arithmetic as a subsystem, so that kind of higher-order RM is relatively easy to capture. And there are natural weak subsystems of type theory, as I said. I'm not so familiar with work on RM based on set theory. Could you give some pointers? I can imagine as base system something like IKP with extensions, but perhaps something else is used?

@TimothyChow : By “abstract math” I mean stuff about “arbitrary” sets/groups/topological spaces/etc. that don't have a fixed place in the finite type hierarchy. Results about these are very awkward if not impossible to formalize in simple type theory/HOL.

A comment about reverse mathematics (RM) & Maddy's Risk Assessment and Metamathematical Corral: I think the jury is still out on this: Most work in RM uses either (classical) subsystems of 2nd order arithmetic or of HA/PAomega (arithmetic in finite types), and these systems are not suitable for abstract math. Type theory has natural weak fragments of strength HA, through predicative arithmetic, and up. And there's preliminary work also on finitistic type theories. I think formalization in something like (intuitionistic) Kripke-Platek set theory would be unwieldy by comparison.

As a step in this direction (giving a natural-looking scheme rather than a single sentence), look at Anton Freund's recent A mathematical commitment without computational strength.

In some sense this reminds one of the foundations for random variables, considered as measurable functions $x : \Omega \to \mathbb{R}$, where $\Omega$ is an unspecified probability space. The parallel isn't exact since most operations on random variables leave the domain $\Omega$ intact, whereas operations on “differential variables” change the domain.

Thanks @HJRW, for bringing that up. It predates the papers on the absolute case (from 1980 and 1983), but it states (p. 314): “In fact it can be proved that the absolute PD²-conjecture implies the relative one.” This is then sketched for one-relator groups. I think this amplifies my question: was this stuff ever revisited later? (And perhaps from a more geometric/homotopical perspective?)

You mean: how do you ensure that it's actually an enumeration? Well, the raw terms are given by a context free grammar, so standard techniques work. Your mention of rules suggests an alternative strategy to prove semi-decidability of type inhabitance: enumerate derivable judgments. That also works, but as usual we have to ensure that all rules are tried infinitely often. Again, that's a standard technique.