ΠW-pretopos

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

- In homotopy type theory the h-sets form a ΠW-pretopos (Rijke-Spitter 13). See also at
*structural set theory*.

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

See also at *predicative topos*.

That the h-sets in homotopy type theory form a ΠW-pretopos is discussed in

- Egbert Rijke, Bas Spitters,
*Sets in homotopy type theory*, Mathematical Structures in Computer Science, Volume 25, Issue 5 (From type theory and homotopy theory to Univalent Foundations of Mathematics) (arXiv:1305.3835)

which became one chapter in

- Univalent Foundations Project,
*Homotopy Type Theory ? Univalent Foundations of Mathematics?*

Last revised on October 27, 2017 at 03:22:56. See the history of this page for a list of all contributions to it.