Hereditarily effective typestreams (Q1360315)

In previous work the author has introduced the notion of typestreams to generalize types defined by strictly positive induction. Modifying this by imposing effectivity conditions, the present paper constructs the so-called hereditarily effective typestreams. The construction is inductive, and the paper's main result is that the closure ordinal of this induction is the first recursively inaccessible ordinal.