Small maps from a universe Universes are essential in the context of algebraic set theory where one is interested in making models of various flavors of Zermelo-Fraenkel set theory. Developments of algebraic set theory usually proceed as follows.

• One starts with some ambient category `C`. This category is required to satisfy several properties, usually that it is finitely complete, extensive, regular, and that it is a Heyting category.
• This category must be equipped with a class of maps, which are called the small maps. If we think about small maps from the context of set theory, then we think of them as maps `f : x --> y` whose fibers are contained in some fixed cardinal `κ`. There are various axiomatizations for the class of small maps, and we discuss them below.
• There must be a universe. Specifically, there is a morphsm `p : e --> b` such that every small map can be obtained as some pullback of `p`.
• There also must be a powerclass operator, which intuitively means that for every object `x` we have an object `P x` that contains all small subobjects of `x` (i.e., all small monomorphism into `x`), and this powerclass operator must have an initial algebra.

The final ingredient (powerclass and its initial algebra) is necessary to construct the collection `V` of all sets, which allows us to make models of Zermelo-Fraenkel set theory where one has unbounded quantification. However, in this file we are only interested in the first three ingredients. There are various axioms that one considers for classes of small maps. Here we list some of them and we give their type theoretic interpretation.

• Every identity morphism is small. From a type theoretic perspective, this means that the terminal object is small.
• The composition of small morphisms is small. From a type theoretic perspective, this means that small types are closed under ∑-types.
• Every monomorphism is small. This corresponds to propositional resizing, as it says that the universe contains every proposition (monomorphisms correspond to propositions).
• Small morphisms are closed under pullback. This means that small types are closed under substitution.
• Small morphisms are closed under taking copairs. This means that small types are closed under sums.
• Small morphisms are closed under regular epimorphisms. This means that every quotient of a small type again is small. Note that there is no restriction on the equivalence relation, which can be large.
• The natural numbers object and the subobject classifier are small. The first means that the type of natural numbers is small and the second is another impredicativity axiom. More specifically, it says that the type of all propositions is small.

And there are much more axioms that one might consider for classes of small maps depending on the context. In this file, we construct a class of small maps in every category with a universe. We also show how closure conditions of the universe gives rise to closure conditions on the class of small maps. The main idea is that a morphism is said to be small if there is a code in the universe whose associated type corresponds to that type. If we use suggestive notation, then we can see a morphism `π A : Γ & A --> Γ` as a type `A` in context `Γ`, and we say that `A` is small if there is a term `a` of the universe type in context `Γ` such that `el a` and `A` are isomorphic. It is worthwhile to notice that approaches based on small maps endow morphisms with an additional property. However, our development of type formers is based on operations. More concretely, the axiom for ∑-types in the context of small maps says that small maps are closed under composition, and this purely talks about property. However, our axiom for ∑-types is expressed via an operation on terms of the universe type with suitable stability conditions. To illustrate the axioms below, we compare them to "A brief introduction to algebraic set theory" by Awodey, and we highlight similarities and differences. Note that the axiom (U), which says that the powerclass has an initial algebra `V`, is not considered in this file. References

• "A brief introduction to algebraic set theory" by Awodey
• "Algebraic set theory" by Joyal and Moerdijk
• "A unified approach to algebraic set theory" by Van den Berg and Moerdijk
• "Elementary axioms for categories of classes" by Simpson
• "Type theories, toposes and constructive set theory: predicative aspects of AST" by Moerdijk and Palmgren

Contents 1. Small maps 2. Closure under isomorphism 3. Closure under pullback 4. All isomorphisms are small 5. Composition of small maps 6. All monomorphisms are small 7. Copairs are small 8. Small NNOs 9. Small subobject classifiers 10. ∏-types

1. Small maps

2. Closure under isomorphism

3. Closure under pullback

This corresponds to axiom (S2) in "A brief introduction to algebraic set theory" by Awodey

4. All isomorphisms are small

The statement `all_identity_small` corresponds to axiom (S1) in "A brief introduction to algebraic set theory" by Awodey. Note that our class of small maps is closed under isomorphism, because small maps are some pullback of the universe. For this reason, we can conclude that all isomorphisms are small. Note that (S1) says that the small maps form a subcategory, so they contain all identities and they are closed under composition,

5. Composition of small maps

This corresponds to axiom (S1) in "A brief introduction to algebraic set theory" by Awodey. Note that (S1) says that the small maps form a subcategory, so they contain all identities and they are closed under composition,

6. All monomorphisms are small

This corresponds to axiom (S3) in "A brief introduction to algebraic set theory" by Awodey.

7. Copairs are small

This corresponds to axiom (S5) in "A brief introduction to algebraic set theory" by Awodey.

8. Small NNOs

This corresponds to axiom (I) in "A brief introduction to algebraic set theory" by Awodey.

9. Small subobject classifiers

Axiom (P1) and (P2) in "A brief introduction to algebraic set theory" by Awodey says that powerclasses exist and that powerclasses of small objects again are small objects. From this, one can conclude that the ambient category has a subobject classifier (see Proposition 2.5 in "Elementary axioms for categories of classes" by Simpson), and that the subobject classifier is small. Note that here one needs that all monomorphisms are small. The following statement expresses the smallness of the subobject classifier. If the ambient category is locally Cartesian closed, then powerclasses can be constructed from the subobject classifier.

10. ∏-types