Palmgren (1997), On universes in type theory, discusses work of several theorists that provide what we might call a family of Large Universe Axioms (LUAs) for predicative type theory, culminating in Rathjen's MLF_w that corresponds to Kripke-Platek set theory with a weakened epsilon-induction principle. He also provides a criterion for recognising predicative universe-forming operations: does it come equipped with an induction rule?

That work and work since has been suggestive of a partial analogy between LCAs in set theory (specifically KP set theory) and LUAs in type theory. This is provocative and interesting, but what I have read has left me unclear about how productive the analogy is. How well-founded is the analogy? What are its limits?