A -pretopos is a pretopos that is also a locally cartesian closed category.
A ΠW-pretopos is a -pretopos that also has all W-types.
A predicative topos is -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.