nLab ΠW-pretopos

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Definition

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

Examples

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 January 9, 2023 at 07:15:51. See the history of this page for a list of all contributions to it.