nLab sigma-pretopos

Contents

Context

Category theory

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Contents

Idea

A categorification of the notion of σ \sigma -frame.

Definition

A σ\sigma-pretopos is a pretopos \mathcal{E} where all countable unions of subobjects (exist and) are pullback-stable.

Girard-esque axioms

A σ\sigma-pretopos is

Examples

See also

References

The concept is defined and discussed around Lemma A.1.4.19 in

A predicative approach to foundations using σ\sigma-pretoposes is given in

  • Alex Simpson and Thomas Streicher, Constructive toposes with countable sums as models of constructive set theory, Annals of Pure and Applied Logic 163 (2012), 1419–1436.

Simplicial homotopy internal to a σ\sigma-pretopos is studied in:

Last revised on May 10, 2022 at 08:06:35. See the history of this page for a list of all contributions to it.