A $\Pi$-pretopos is a pretopos that is also a locally cartesian closed category.
A ΠW-pretopos is a $\Pi$-pretopos that also has all W-types.
A predicative topos is $\Pi W$-pretopos with axiom of multiple choice.
See at predicative topos.
Last revised on September 13, 2012 at 03:22:13. See the history of this page for a list of all contributions to it.