Inaccessibility in constructive set theory and type theory

This paper is the first in a series whose objective is to study notions of large sets in the context of formal theories of constructivity. The two theories considered are Aczel's constructive set theory (CZF) and Martin-Löf's intuitionistic theory of types.This paper treats Mahlo's π-numbers which give rise classically to the enumerations of inaccessibles of all transfinite orders. We extend the axioms of CZF and show that the resulting theory, …