Contents

topos theory

# Contents

## Definition

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

## 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

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