A categorification of the notion of $\sigma$-frame.
A $\sigma$-pretopos is a pretopos $\mathcal{E}$ where all countable unions of subobjects (exist and) are pullback-stable.
A $\sigma$-pretopos is
a category
with a generating set,
with all finite limits,
with all countable coproducts, which are disjoint, and pullback-stable,
where all congruences have effective quotient objects, which are also pullback-stable.
Any infinitary pretopos is a $\sigma$-topos.
The category of countable sets (for instance, subquotients of the natural numbers $\mathbb{N}$) is a $\sigma$-pretopos.
The category of sets in the predicative set theory $CZF_{Exp}$ from (Simpson-Streicher 2012) is a $\sigma$-pretopos.
The concept is defined and discussed around Lemma A.1.4.19 in
A predicative approach to foundations using $\sigma$-pretoposes is given in
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.