ΠW-pretopos

*Could not include topos theory - contents*

A **$\Pi W$-pretopos** is a Π-pretopos with all W-types.

- A predicative topos is a $\Pi W$-pretopos satisfying the axiom of multiple choice.

See at *predicative topos*.

Revised on April 21, 2013 13:27:51
by Urs Schreiber
(89.204.135.147)