A pretopos is a coherent category which is both extensive and exact. (See familial regularity and exactness for why extensivity and exactness deserve to be considered together.)
I think it’s a bit reduntant to demand the category to be coherent, since the joins in the subobject lattices can be constructed using coproducts and image factorizations. A more minimal definition would be: “A pretopos is a regular category which is extensive and exact”. – Jonas
Frequently one is especially interested in pretoposes having additional properties, such as:
An infinitary pretopos is an infinitary coherent category which is both infinitary extensive and exact. Giraud's theorem says that infinitary pretoposes with small generating sets are the same as Grothendieck toposes, and in particular are toposes (although this last result is not valid in predicative mathematics).
Like any coherent (or Heyting) category, a (Heyting) pretopos has an internal logic. Extensivity and exactness make a Heyting pretopos a very set-like category. One can say imprecisely that it has “all the good first-order properties of a topos”, meaning not that it has those properties that can be expressed in elementary terms (which is false) but that it has those properties that (unlike exponential and power objects) correspond to first-order reasoning in ordinary mathematics. Therefore, pretoposes (especially Heyting, , and/or ones) are related to predicative constructive mathematics in a way similar to how toposes are related to non-predicative constructive mathematics.
A pretopos is necessarily balanced, but while it has coproducts and coequalizers of equivalence relations, it need not have all finite colimits. However, if it has countable pullback-stable unions of subobjects, then any internal binary relation generates an equivalence relation and therefore has a quotient, so we can construct arbitrary coequalizers and thus arbitrary finite colimits. And we can perform an “internal” version of this argument in a -pretopos with a NNO, such as a --pretopos.
A pretopos, being a coherent category, admits a subcanonical Grothendieck topology called the coherent topology. In a pretopos, this topology is generated by finite jointly epimorphic families. Since the canonical topology on a Grothendieck topos consists of all jointly epimorphic families, the coherent topology on a pretopos is sometimes called the precanonical topology.
The codomain fibration of a pretopos is always a stack for its precanonical topology. Being a pretopos is stronger than necessary for this condition to hold in a coherent category, however; see coherent category for the necessary and sufficient conditions.