nLab ΠW-pretopos

Definition

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

Examples

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

Related concepts

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

• list-arithmetic pretopos

References

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