Could not include topos theory - contents
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.