nLab
ΠW-pretopos

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

Revised on October 27, 2017 03:22:56 by Urs Schreiber (46.183.103.17)