  In the context of constructive set theory, large sets have been introduced by Aczel in the form of so-called regular sets to allow inductive definitions of sets (Aczel 1986). Rathjen and Crosilla have considered inaccessible sets (Rathjen al. 1998; Crosilla and Rathjen 2001) and Mahlo sets (Rathjen 2003a). Nevertheless, an objection could be raised to extensions of constructive set theory by large set axioms. In classical set theory, large cardinals can be seen as an incarnation of higher infinity. How do we justify these principles constructively? The constructive justification of these notions relies again on the type theoretic interpretation. The addition of these principles corresponds in fact to that of universes and \(W\)-types within constructive type theory. The justification of extensions by large sets is thus bound up with the question of the limits of Martin-Löf type theory (Rathjen 2005). We also note that the addition of inacessible set axioms  to a weak subsystem of CZF (with no set induction) produces a theory of strength \(\Gamma_0\), the ordinal singled out by Feferman and Schütte as the limit of predicativity given the natural numbers (Crosilla and Rathjen 2001; see also section 1.3). This is  witness to the fact that by working in a constructive, predicative context, we can tame traditionally strong set-theoretic notions.