Open MathsAll courses

Draft lesson.

Coproduct covers and generator bounds

A map into a filtered colimit need not lift directly to one stage. Instead, pull it back to every stage, find an epimorphic pullback leg, and lift only the generator maps that actually occur there. A second cardinal bound controls the relations of this cover. Those relations become equal at a later stage, where the cover descends to the required map. A different argument assembles a quotient from all its small subcovers and bounds its generator maps by a regular tagged union.

1. The hypotheses and the actual comparison

Work in ZF with set-indexed Choice, a fixed Grothendieck universe and the explicitly stated enlargement convention of Universes and small categories. A small set is bijective to a universe member; its original labels need not belong to that universe. Categories have ambient set data, and a small indexing category includes its entire arrow set, with identities and composites. All Hom values below are small, with the actual Hom encoding when universe-member values are required.

Keep the following assumptions on a locally small category \(C\), jointly denoted \(H\).

Thus \(G\) is an isomorphism-detecting generator, in the precise convention of Generators, Section 1. It is not merely a separating object. The finite-limit preservation assumption is about \(C\)-valued diagrams; no preservation by \(\operatorname{Hom}(G,-)\) follows from these words.

For an arrow \(u:B\to A\), its coimage is the coequalizer of its kernel pair and its image is the equalizer of the two self-pushout legs. Strictness means that the specified comparison from coimage to image is invertible. The complete strict epimorphism and coimage proofs give the following equivalent form for a strict epimorphism:

\[ B\times_A B\ \rightrightarrows\ B \xrightarrow{u}A \quad\text{is a coequalizer fork}. \tag{1.1} \]

Here is why the precise comparison matters. If \(u\) is epic, its self-pushout legs agree by cancellation; its image inclusion is therefore the identity of \(A\), up to the unique compatible isomorphism. Strictness says that its coimage factor to \(A\) is invertible, which is exactly (1.1). A coequalizer is epic by factor uniqueness. Moreover, a monic strict epimorphism is invertible: its kernel-pair projections agree, so \(1_B\) equalizes them and descends to \(s:A\to B\) with \(su=1_B\); cancellation of \(u\) in \(usu=u\) gives \(us=1_A\). These consequences require the stated strictness, rather than a general assertion about monic epimorphisms.

Let \(\pi\) be infinite regular. We use the complete cardinal-filtered convention and whole-arrow criterion: fewer than \(\pi\) objects have a receiver, and fewer than \(\pi\) parallel arrows have one common equalizing postarrow. The empty object family forces nonemptiness. These conditions imply ordinary filteredness. A diagram \(X:I\to C\) on a small \(\pi\)-filtered category has a chosen colimit \(L\) with actual legs \(c_i:X_i\to L\). Write \(X(s):X_i\to X_j\) for a transition.

The canonical function is

\[ \begin{gathered} \chi_{A,X}:\operatorname{colim}_{i\in I} \operatorname{Hom}_C(A,X_i) \longrightarrow\operatorname{Hom}_C(A,L),\\ \chi_{A,X}[i,f]=c_i f. \end{gathered} \tag{1.2} \]

The complete filtered Set quotient defines the classes. The cocone equation \(c_jX(s)=c_i\) makes (1.2) well-defined. In particular, equality of two classes is an equality after two actual arrows to one common stage. For two representatives already at \(i\), equality is witnessed by one arrow \(s:i\to j\): equalize the possibly distinct same-source witness arrows before transporting the maps.

For \(a:A'\to A\), precomposition sends \([i,f]\) to \([i,fa]\), and \(c_i(fa)=(c_i f)a\). For a transformation \(\eta:X\to X'\), let \(\ell:L\to L'\) be the colimit map, so \(\ell c_i=c'_i\eta_i\). Then

\[ \chi_{A,X'}[i,\eta_i f] =c'_i\eta_i f =\ell c_i f. \tag{1.3} \]

These are both naturality squares, including their identity and composite laws. Changing the colimit replaces (1.2) by postcomposition with the unique isomorphism preserving every \(c_i\). An object is \(\pi\)-accessible precisely when (1.2) is bijective for every such \(I,X\), as in the complete accessibility comparison and definition.

2. Coproducts on functions and their empty subfamilies

Put

\[ P_E=\coprod_{e\in E}G, \qquad j_e^E:G\to P_E. \tag{2.1} \]

Choose these coproducts for the actual set-indexed collections used in the proof. For universe-member indexing sets, their collection is an ambient set in an enlargement, so set-indexed Choice licenses these choices. Relabeling other small sets transports the specified coproduct maps along bijections. There is no choice over a proper class of all relabelings.

For a function \(b:E\to F\), the coproduct universal property gives the unique arrow

\[ P(b):P_E\to P_F, \qquad P(b)j_e^E=j_{b(e)}^F. \tag{2.2} \]

The component equations show \(P(1_E)=1_{P_E}\) and \(P(db)=P(d)P(b)\). They also show that a bijection induces the compatible coproduct isomorphism, with inverse induced by its inverse function. For \(E=\varnothing\), \(P_E=0\) is initial; the empty component equations specify its unique map out. Thus (2.2) supplies the whole coproduct-on-functions construction, not just its object assignment.

Subfamily Hom bound. If \(S\subseteq T\), then the specified inclusion map \(P(S\hookrightarrow T)\) induces an injection

\[ \operatorname{Hom}(G,P_S) \longrightarrow\operatorname{Hom}(G,P_T). \tag{2.3} \]

For nonempty \(S\), choose \(s_0\in S\), and define \(r:T\to S\) to fix \(S\) and send its complement to \(s_0\). The composite \(P(r)P(S\hookrightarrow T)\) is \(1_{P_S}\) on every component, hence is the identity. Postcomposition by \(P(r)\) is a left inverse of (2.3).

For empty \(S\), if \(\operatorname{Hom}(G,0)\) is empty, (2.3) has empty domain and is injective. Otherwise choose an actual \(a:G\to0\). The constant component family \(a\) defines \(v:P_T\to0\). If \(u:0\to P_T\) is the initial map, \(vu=1_0\), because \(0\) has one endomorphism. Postcomposition by \(v\) is the required left inverse. This also covers empty \(T\). It never asserts that a nonempty set retracts onto the empty set. This argument proves a Hom injection; an arbitrary coproduct inclusion is not presumed monic. No regularity is used in (2.3).

There is also a canonical evaluation arrow

\[ \varepsilon_Y:P_{\operatorname{Hom}(G,Y)}\to Y, \qquad\varepsilon_Yj_h=h. \tag{2.4} \]

It is epic under \(H\). Indeed, if two maps \(a,b:Y\to Z\) agree on every \(h:G\to Y\), their equalizer \(e:E\to Y\) induces a bijection on \(G\)-Hom sets: each \(h\) factors uniquely through \(e\). Detection makes \(e\) invertible, so \(a=b\). If \(a\varepsilon_Y=b\varepsilon_Y\), the component equations give exactly that situation. This is the complete evaluation-epimorphism argument, including an empty indexing set. For \(v:Y\to Y'\), the component equation gives

\[ v\varepsilon_Y =\varepsilon_{Y'}P(\operatorname{Hom}(G,v)). \tag{2.5} \]

3. A whole coslice and a small-target stage lemma

Fix \(i_0\in I\). The category \(J=(i_0\downarrow I)\) has all objects \(s:i_0\to i\), and all arrows \(t:s\to s'\) satisfying \(ts=s'\). Identity and composition satisfy that equation. It is small: its objects are a subset of the whole arrow set of \(I\), and its arrows are a subset of products of that set. Its projection is \(p(s)=i\), \(p(t)=t\).

Here are the complete bounded filtering checks. Receive fewer than \(\pi\) objects \(s_a:i_0\to i_a\) at \(z\) using \(r_a:i_a\to z\). For a nonempty family, equalize the entire bounded parallel family \(r_as_a:i_0\to z\) by one \(q:z\to w\). Its common composite is a coslice object, and the \(qr_a\) are its receiving arrows. For an empty family use \(1_{i_0}\). A bounded family of parallel coslice arrows \(t_b:(i,s)\to(i',s')\) has one ambient equalizing arrow \(h:i'\to k\); this is the coslice arrow from \(s'\) to \(hs'\). Empty parallel families use the target identity. Thus \(J\) is \(\pi\)-filtered.

The projection is cofinal. For an object \(i\), an object of \((i\downarrow p)\) is the complete pair of legs \(i_0\xrightarrow{s}k\xleftarrow{r}i\). Such an object exists by ordinary filteredness. For two such objects, receive their targets at one target and then equalize the two resulting legs from \(i_0\) and the two from \(i\), using two successive postcompositions. The resulting pair of legs is a common receiver in this comma category. Therefore it is nonempty and connected. The complete cofinal cocone extension and its inverse shows that restricting to \(J\) preserves the colimit with all its specified legs. In particular,

\[ \operatorname{colim}_{s\in J}X_{p(s)} \xrightarrow{\sim}L, \qquad\text{leg at }s\text{ is }c_{p(s)}. \tag{3.1} \]

This uses the whole coslice, rather than a selected list of objects or only a generating graph. The same complete coslice mechanism appears in Common arrows, Exercise 1.

Stage epimorphism lemma. Under \(H\), let \(D:I\to C\) be small \(\pi\)-filtered and let \(u:\operatorname{colim}_I D\to Y\) be epic. Assume either \(|\operatorname{Hom}(G,Y)|<\pi\) or that \(Y\) is \(\pi\)-accessible. Here accessibility means that the canonical Hom comparison is bijective for every small \(\pi\)-filtered diagram. Then one original leg \(u_i:D_i\to Y\) is epic.

The two alternatives share the following image construction. For each \(i\), form

\[ Q_i=Y\amalg_{D_i}Y, \qquad Z_i=\operatorname{eq}(q_i^0,q_i^1), \qquad m_i:Z_i\to Y. \tag{3.2} \]

The notation in (3.2) means that \(m_i\) is the equalizer inclusion of the two maps \(q_i^0,q_i^1:Y\to Q_i\). A transition \(s:i\to j\) induces the unique \(Q(s):Q_i\to Q_j\) preserving both \(Y\)-legs, because \(u_jD(s)=u_i\). Pushout uniqueness gives both functor laws. Equalizer uniqueness then gives \(Z(s):Z_i\to Z_j\) with \(m_jZ(s)=m_i\). Cancellation of the monic \(m_j\) gives its functor laws and shows each \(Z(s)\) monic.

A cocone \(Q_i\to T\) gives two compatible families of maps from \(Y\). Nonempty filteredness makes each family constant: arrows identify its entries, and a common receiver compares any two entries. The resulting pair \(a,b:Y\to T\) satisfies \(au_i=bu_i\) for every \(i\), which is equivalent to \(au=bu\) by the original colimit property. Conversely that pair uniquely defines every compatible pushout factor. These are inverse factor constructions, preserving both \(Y\)-legs and postcomposition in \(T\). Consequently \(\operatorname{colim}Q_i=Y\amalg_{\operatorname{colim}D_i}Y\) compatibly.

For any nonempty filtered category, the constant identity diagram at an object has that object as its colimit: a cocone has one common leg by the same receiver argument. Apply the finite-limit preservation in \(H\) to the entire equalizer diagram (3.2). Since \(u\) is epic, the two legs of its self-pushout agree. Their equalizer is \(Y\). We obtain the specified isomorphism

\[ \operatorname{colim}_I Z_i\xrightarrow{\sim}Y, \qquad\text{its leg at }i\text{ is }m_i. \tag{3.3} \]

Small-probe alternative. Assume \(|\operatorname{Hom}(G,Y)|<\pi\). Put \(S=\operatorname{colim}_I\operatorname{Hom}(G,Z_i)\) in sets, with class maps \(e_i\). The function \([i,h]\mapsto m_i h\) injects \(S\) into \(\operatorname{Hom}(G,Y)\): receive two representatives at a common stage \(k\), cancel the monic \(m_k\), and use the resulting actual quotient witness. Each \(e_i\) is also injective, since its composite with this function is postcomposition by \(m_i\). Hence \(|S|<\pi\). We do not identify \(S\) with the entire probe of \(Y\).

The complete small-set accessibility proof represents \(1_S\) at one stage: there are \(i_1\) and \(a:S\to\operatorname{Hom}(G,Z_{i_1})\) with \(e_{i_1}a=1_S\). This includes empty \(S\), because the indexing category is nonempty. Since \(e_{i_1}\) is injective, it is bijective. For every actual \(s:i_1\to i\), the equation

\[ e_i\operatorname{Hom}(G,Z(s))=e_{i_1} \tag{3.4} \]

makes \(\operatorname{Hom}(G,Z(s))\) bijective: injectivity follows after \(e_i\); for a target element choose its \(e_i\)-image's inverse under \(e_{i_1}\), then cancel \(e_i\). Detection makes every \(Z(s)\) invertible.

On the whole cofinal coslice \((i_1\downarrow I)\), these maps \(Z(s)\) form a natural isomorphism from the constant identity diagram at \(Z_{i_1}\) to the restricted \(Z\)-diagram; naturality is \(Z(t)Z(s)=Z(ts)\). Its colimit is \(Z_{i_1}\). Cofinality and (3.3) therefore make the original inclusion \(m_{i_1}:Z_{i_1}\to Y\) invertible, with that precise map, because the identity coslice object gives its original leg.

Accessible-target alternative. Assume instead that \(Y\) is \(\pi\)-accessible. Write \(d_i:Z_i\to Z\) for the colimit legs and \(m:Z\xrightarrow{\sim}Y\) for the specific isomorphism (3.3), so \(m d_i=m_i\). The canonical accessibility bijection followed by postcomposition with \(m\) is

\[ \begin{gathered} \operatorname{colim}_{i\in I}\operatorname{Hom}_C(Y,Z_i) \xrightarrow{\ \sim\ }\operatorname{Hom}_C(Y,Y),\\ [i,a]\longmapsto m_i a. \end{gathered} \tag{3.5} \]

Represent \(1_Y\) by one actual pair \([i_1,a:Y\to Z_{i_1}]\). Thus \(m_{i_1}a=1_Y\). Since \(m_{i_1}\) is monic, cancel it in \(m_{i_1}a m_{i_1}=m_{i_1}\) to obtain

\[ a m_{i_1}=1_{Z_{i_1}}, \qquad m_{i_1}a=1_Y. \tag{3.6} \]

Therefore this original image inclusion is invertible. Accessibility is applied to \(Y\), not to \(G\), and does not assert that the probe preserves this colimit. The index remains nonempty even if a Hom value is empty; the identity \(1_Y\) itself has a representative by the assumed comparison.

In either alternative, we have an index \(i_1\) for which \(m_{i_1}\) is invertible. Thus \(q_{i_1}^0=q_{i_1}^1\). If \(v,w:Y\to T\) agree after \(u_{i_1}\), their self-pushout factor \(h:Q_{i_1}\to T\) satisfies \(v=hq_{i_1}^0=hq_{i_1}^1=w\). This proves that the original \(u_{i_1}\) is epic. No colimit preservation by the probe, epimorphic lift of every probe map, or epimorphism from \(D_i\) to its image has been assumed. \(\square\)

4. The first bound proves injectivity

Injectivity lemma. Suppose only \(|\operatorname{Hom}(G,A)|<\pi\), in addition to \(H\) and infinite regular \(\pi\). Then \(\chi_{A,X}\) is injective for every small \(\pi\)-filtered \(X\). The second bound in the next section is not needed here.

Take two representatives with equal target maps. Receive their indices at \(i_0\), transporting them to \(f,g:A\rightrightarrows X_{i_0}\) with \(c_{i_0}f=c_{i_0}g\). For each actual \(s:i_0\to i\), let

\[ N_s=\operatorname{eq}(X(s)f,X(s)g), \qquad n_s:N_s\longrightarrow A. \tag{4.1} \]

Here \(n_s\) is the specified equalizer inclusion into \(A\). For a coslice arrow \(t:s\to s'\), postcomposition transports the equalizer equation. There is a unique \(N(t):N_s\to N_{s'}\) with \(n_{s'}N(t)=n_s\). Its identity and composition equations follow by canceling \(n_{s'}\). These are the entire diagram and its inclusion cocone.

The colimit of the constant \(A\)-diagram is \(A\), and the colimit of the restricted \(X\)-diagram is (3.1). The two resulting maps are both \(c_{i_0}f=c_{i_0}g\), because \(c_iX(s)=c_{i_0}\). Filtered finite-limit exactness therefore identifies the specified comparison with

\[ \operatorname{colim}_{s\in(i_0\downarrow I)}N_s \xrightarrow{\sim}A, \qquad\text{leg at }s\text{ is }n_s. \tag{4.2} \]

Apply the stage epimorphism lemma in its small-probe alternative to this epic comparison and the target \(A\). One \(n_s\) is epic. Its equalizer equation is \(X(s)f n_s=X(s)g n_s\), so epic cancellation gives \(X(s)f=X(s)g\). This one actual arrow \(s:i_0\to i\) is the equality witness for the original colimit classes. The comparison is injective. Empty Hom values add no representative choices, and the coslice always contains \(1_{i_0}\). \(\square\)

5. Both bounds lift a map by descending its cover

Theorem 5.1 (two Hom bounds). Under \(H\), let \(\pi\) be infinite regular and assume

\[ T=\operatorname{Hom}(G,A), \qquad |T|<\pi, \qquad |\operatorname{Hom}(G,P_T)|<\pi. \tag{5.1} \]

Then \(A\) is \(\pi\)-accessible.

The preceding lemma supplies injectivity. To prove surjectivity, take an actual \(f:A\to L\). For every \(i\), form the pullback

\[ Y_i=X_i\times_L A, \qquad t_i:Y_i\to X_i, \qquad p_i:Y_i\to A, \qquad c_it_i=fp_i. \tag{5.2} \]

For \(s:i\to j\), the pair \(X(s)t_i,p_i\) defines the unique transition \(Y(s):Y_i\to Y_j\). Its equations are \(t_jY(s)=X(s)t_i\) and \(p_jY(s)=p_i\); pullback uniqueness gives both functor laws. The colimits of the constant \(L,A\)-diagrams are \(L,A\). Exactness applied to this entire pullback diagram gives

\[ \operatorname{colim}_IY_i\xrightarrow{\sim}A, \qquad\text{leg at }i\text{ is }p_i. \tag{5.3} \]

Indeed the final pullback is \(L\times_L A\), whose specified projection to \(A\) is invertible. The first bound and the stage lemma give \(i_0\) such that \(p=p_{i_0}:Y_{i_0}\to A\) is epic.

Now retain exactly the generator maps that lift. Set

\[ \begin{gathered} E=\operatorname{Hom}(G,Y_{i_0}),\\ r:E\to T,\qquad r(h)=ph,\\ K=r(E)\subseteq T,\qquad \bar r:E\twoheadrightarrow K. \end{gathered} \tag{5.4} \]

The notation \(\bar r\) is the actual function onto its image. It is not an assertion that \(r\) is onto \(T\). Define \(\varepsilon_K:P_K\to A\) by \(\varepsilon_Kj_k=k\). The component equations give

\[ \varepsilon_KP(\bar r)=p\varepsilon_{Y_{i_0}}. \tag{5.5} \]

The right side is a composite of epimorphisms, by (2.4) and the choice of \(i_0\). Therefore \(\varepsilon_K\) is epic: maps equal after it are equal after that composite. Choice selects a section \(\sigma:K\to E\) of the actual surjection \(\bar r\); for empty \(K\) this is the unique empty function. Equation (2.2) gives \(P(\bar r)P(\sigma)=1_{P_K}\).

Write \(B=P_K\), and put

\[ \ell=\varepsilon_{Y_{i_0}}P(\sigma):B\to Y_{i_0}, \qquad b=t_{i_0}\ell:B\to X_{i_0}. \tag{5.6} \]

Equations (5.2), (5.5) and the section identity show

\[ p\ell=\varepsilon_K, \qquad c_{i_0}b=f\varepsilon_K. \tag{5.7} \]

Thus we have lifted an epimorphic cover of \(A\), rather than every map from \(G\) to \(A\).

Let \(R=B\times_A B\) for this cover, with projections \(r_0,r_1:R\to B\). The second bound in (5.1) and (2.3), applied to \(K\subseteq T\), give \(|\operatorname{Hom}(G,B)|<\pi\). The pullback property gives an actual bijection between maps \(G\to R\) and pairs of maps \(G\to B\) with the same composite to \(A\). In particular,

\[ |\operatorname{Hom}(G,R)| \leq|\operatorname{Hom}(G,B)|^2<\pi. \tag{5.8} \]

For finite Hom sets the square is finite, including cardinal zero. For infinite ones the complete infinite-square proof makes the square equal to the original cardinal. This particular inequality needs no regularity beyond \(\pi\) being infinite; regularity is retained for the theorem's full hypotheses.

Since \(\varepsilon_K\) is strict and epic, (1.1) is the actual coequalizer fork \(R\rightrightarrows B\xrightarrow{\varepsilon_K}A\). Equation (5.7) gives

\[ c_{i_0}br_0=f\varepsilon_Kr_0 =f\varepsilon_Kr_1=c_{i_0}br_1. \tag{5.9} \]

Apply only the injectivity lemma of Section 4 to the object \(R\), using (5.8). It says that the classes of \(br_0,br_1:R\to X_{i_0}\) are equal. The one-arrow same-stage criterion supplies an actual \(s:i_0\to i\) with

\[ X(s)br_0=X(s)br_1. \tag{5.10} \]

The coequalizer property now defines a unique \(a:A\to X_i\) with \(a\varepsilon_K=X(s)b\). Consequently

\[ c_i a\varepsilon_K =c_iX(s)b =c_{i_0}b =f\varepsilon_K. \tag{5.11} \]

Cancel the epic \(\varepsilon_K\) to get \(c_i a=f\). This is surjectivity of the precise function (1.2), and hence the claimed accessibility. Its inverse is independent of the sections, representatives, coproduct choices and stages because injectivity has already been proved. The naturality equations (1.3) and the precomposition equation therefore apply also to these inverse bijections.

Every empty case is retained: empty \(T\) and empty \(K\), the initial coproduct, a possibly empty \(\operatorname{Hom}(G,0)\), and empty values in the filtered Set quotients. A \(\pi\)-filtered index is always nonempty. Neither \(B\) nor \(R\) is assumed accessible before its needed property is proved; only the first bound is applied to \(R\). \(\square\)

Worked example: three points in a growing set. In sets take \(G=\{*\}\), \(A=\{a,b,c\}\), \(X_n=\{0,\ldots,n\}\) and the inclusion transitions. The colimit is \(\mathbb N\). Here \(T=A\) by evaluation at \(*\), and \(P_T\) is a three-element set, so both bounds hold at \(\pi=\aleph_0\). For \(f(a)=2,f(b)=5,f(c)=2\), stage \(5\) already contains every value. Its pullback over \(A\) is \(A\), \(K=T\), and the descended stage map has exactly those three values. Equality of two functions in the colimit is coordinatewise eventual equality; the finite witness family is synchronized by one later arrow. In a category with nontrivial parallel arrows, that synchronization is part of the proof, not an assumption.

Sets satisfy \(H\): small tagged-union quotients construct all colimits, compatible tuples construct finite limits, and the complete filtered finite-limit comparison proves exactness. A singleton detects bijections. Set epimorphisms are surjections: if a point is missed, its indicator and the constant-zero function disagree but agree after the map. A surjection is the coequalizer of its fibre pair, by the unique class factor, so is strict.

6. Two cardinal parameters with four distinct conditions

For the next theorem keep \(H\) and cardinals \(\pi_0,\pi\) satisfying all four conditions:

\[ \begin{array}{ll} \text{(a)}&\pi_0,\pi\text{ are infinite regular};\\ \text{(b)}&G\text{ is }\pi_0\text{-accessible};\\ \text{(c)}&\rho^{\pi_0}<\pi\text{ for every cardinal }\rho<\pi;\\ \text{(d)}&P_E\twoheadrightarrow Q,\ |E|<\pi_0\\ &\hspace{1em}\Longrightarrow\ |\operatorname{Hom}(G,Q)|<\pi. \end{array} \tag{6.1} \]

The fourth condition includes \(E=\varnothing\). The second is an actual accessibility statement, not merely detection by \(G\). The exponent in (c) is \(\pi_0\), not \(\pi\). Applying (c) to \(\rho=2\) implies \(\pi_0<\pi\), by Cantor's theorem; this relation is a consequence, rather than an additional unmentioned hypothesis.

Here is a complete way to obtain these parameters under \(H\). Both \(\operatorname{Hom}(G,G)\) and \(\operatorname{Hom}(G,P_{\operatorname{Hom}(G,G)})\) are small sets. Choose an infinite cardinal bounding their cardinalities, then its cardinal successor \(\pi_0\). The complete regular-successor proof makes \(\pi_0\) regular, and Theorem 5.1, applied to \(A=G\) with both bounds, gives (b).

For each initial cardinal \(\alpha<\pi_0\), choose a small set of representative strict quotients of \(P_\alpha\), with their quotient arrows. This is licensed by the entire strict-quotient encoding proof: the kernel pair is a subobject of \(P_\alpha\times P_\alpha\), possible subobjects are encoded by subsets of small probe sets, and two quotients with the same kernel pair are uniquely isomorphic over \(P_\alpha\). Because every epimorphism is strict, these representatives cover every epimorphic quotient here.

The initial cardinals below \(\pi_0\) form a small subset of \(\pi_0\). Collect the whole tagged family of representatives over this subset, and then the whole tagged union of their small \(G\)-Hom sets. Universe closure makes this one small family and one small union. Choose a cardinal \(\pi_1\geq\pi_0\) strictly larger than that union's cardinal. For any small \(E\) of size below \(\pi_0\), a bijection \(E\to\alpha\) induces the compatible coproduct isomorphism by (2.2). Transport an arbitrary quotient of \(P_E\) across it, and then across its representative target isomorphism. Postcomposition by that target isomorphism is a Hom bijection. Thus the one bound \(|\operatorname{Hom}(G,Q)|<\pi_1\) covers all such quotients, including the initial coproduct. Per-index smallness alone would not supply this uniform bound.

Set \(\pi=(2^{\pi_1})^+\), the cardinal successor of the power-set cardinal. Both \(\pi,\pi_0\) are regular; no regularity of the intermediate \(\pi_1\) is required. If \(\rho<\pi\), then \(\rho\leq2^{\pi_1}\). Postcomposition with an injection of the bases and the complete function-set currying and cardinal product proofs give

\[ \rho^{\pi_0} \leq(2^{\pi_1})^{\pi_0} =2^{\pi_1\cdot\pi_0} =2^{\pi_1}<\pi. \tag{6.2} \]

Here \(\pi_1\cdot\pi_0=\pi_1\) because both are infinite and \(\pi_1\geq\pi_0\). The currying map sends a function \(\pi_0\to\{0,1\}^{\pi_1}\) to \((a,b)\mapsto F(b)(a)\), with inverse \(b\mapsto(a\mapsto f(a,b))\). The base-injection step includes \(\rho=0,1\). The uniform \(\pi_1\)-bound gives (d), since \(\pi_1<\pi\). All cardinals and representative collections stay in the working universe by the retained closure and successor proofs. This construction derives (6.1) without using the quotient theorem proved next.

7. Count every small subset, including zero and one point

Let \(A\) be a small set with \(|A|<\pi\), and put

\[ I=\{B\subseteq A:|B|<\pi_0\}, \qquad\beta=\max(2,|A|). \tag{7.1} \]

Regard \(I\) as the full inclusion category, with arrows all \((B,D)\) such that \(B\subseteq D\), identity \((B,B)\), and composition \((D,E)(B,D)=(B,E)\). Object and arrow sets are subsets of \(\mathcal P(A)\) and its square, with the appropriate universe encodings. Regularity of \(\pi_0\) says that the union of fewer than \(\pi_0\) subsets of cardinal below \(\pi_0\) still has that bound. The union receives the whole bounded family by inclusion; the empty family is received by \(\varnothing\). Thinness makes the target identity equalize every parallel family. Thus \(I\) is small and \(\pi_0\)-filtered, as in the complete small-subset proof. We do not assert \(|I|<\pi_0\).

The needed different bound is

\[ |I|\leq\max(2,|A|)^{\pi_0}<\pi. \tag{7.2} \]

Here is the complete coding proof of the first inequality. If \(A\) is empty, its one subset is coded by the constant-zero function \(\pi_0\to2\). For a singleton \(A\), its two subsets are coded by the distinct constant-zero and constant-one functions; they differ at \(0\in\pi_0\). These cases have \(\beta=2\).

If \(A\) has distinct \(a_0,a_1\), then \(\beta=|A|\). For every nonempty \(B\in I\), choose \(b_B\in B\) and an injection \(e_B:B\to\pi_0\). This is Choice over the set of nonempty members of \(I\). Define \(s_B:\pi_0\to B\) to take value \(b\) at \(e_B(b)\), and value \(b_B\) at the remaining arguments. Its image is exactly \(B\). There is an explicit bijection

\[ d:\pi_0\xrightarrow{\sim}\pi_0\setminus\{0\}, \qquad d(n)=n+1\ (n<\omega), \qquad d(\xi)=\xi\ (\xi\geq\omega). \tag{7.3} \]

Its inverse takes positive finite ordinals to their predecessors and fixes infinite ordinals; when \(\pi_0=\omega\), the infinite part is empty. Code the empty subset by the constant function with value \(a_0\). For nonempty \(B\), define

\[ f_B(0)=a_1, \qquad f_B(d(\xi))=s_B(\xi). \tag{7.4} \]

The flag at \(0\) distinguishes emptiness, and the image on \(\pi_0\setminus\{0\}\) recovers every nonempty \(B\). These are therefore distinct functions for distinct subsets, giving an injection \(I\to A^{\pi_0}\) in this case. The code graphs and their set-indexed choices have the retained universe bounds. This coding uses only infinitude of the exponent; regularity is used separately for filteredness of \(I\). Since \(\beta<\pi\), condition (c) gives the strict inequality in (7.2). The unpadded bound with base \(|A|\) would be false for empty and singleton \(A\).

8. Coimages form the entire subcover diagram

Theorem 8.1 (quotient probe bound). Under \(H\) and all four conditions (6.1), an epimorphism \(u:P_A\to X\) with \(|A|<\pi\) satisfies

\[ |\operatorname{Hom}(G,X)|<\pi. \tag{8.1} \]

For every \(B\in I\) from (7.1), let \(\iota_B:B\hookrightarrow A\), \(f_B=uP(\iota_B)\), and form its coimage factorization

\[ P_B\xrightarrow{q_B}X_B \xrightarrow{m_B}X, \qquad m_Bq_B=f_B. \tag{8.2} \]

The quotient \(q_B\) is strict epic. Under the assumption that all epimorphisms are strict, \(m_B\) is monic, by the full coimage composition proof. To keep its logical use explicit, that proof works as follows. For a general \(f=mq\) with \(q=\operatorname{coim}(f)\), form \(t=\operatorname{coim}(m)\). The maps \(q,t,tq\) are strict epic, the last by the hypothesis on all epimorphisms. For maps \(a,b\) into the original source, \(fa=fb\) is equivalent to \(qa=qb\), by the original kernel pair and the factorization. Also \(tqa=tqb\) implies \(fa=fb\), since \(m\) factors through \(t\); the reverse implication follows from \(qa=qb\). Thus \(q\) and \(tq\) have the same kernel pair. They are its two coequalizers, so their comparison \(t\) is invertible. The coimage of \(m\) being invertible forces its kernel-pair projections to agree, and the universal pullback test then makes \(m\) monic. This does not identify coimage with image for an arbitrary arrow.

For every inclusion \(v:B\hookrightarrow D\), the map \(q_D P(v):P_B\to X_D\) descends across \(q_B\). Indeed, if \(r_0,r_1\) are the kernel-pair projections of \(q_B\), their composites under this map agree after the monic \(m_D\), because

\[ m_Dq_DP(v)r_a =m_Bq_Br_a\qquad(a=0,1). \tag{8.3} \]

Cancel \(m_D\), and use the coequalizer property of \(q_B\) to define the unique \(x_{BD}:X_B\to X_D\) with

\[ x_{BD}q_B=q_DP(v), \qquad m_Dx_{BD}=m_B. \tag{8.4} \]

The second equation follows by canceling \(q_B\). Identity and composition follow by the same epic cancellation and the coproduct functor laws. Also \(x_{BD}\) is monic: its composite with \(m_D\) is the monic \(m_B\). We have the whole \(I\)-diagram of compatible subobjects and natural quotients, including \(B=\varnothing\).

Let \(Z=\operatorname{colim}_{B\in I}X_B\), with legs \(d_B\), and let

\[ m:Z\to X, \qquad md_B=m_B. \tag{8.5} \]

This actual comparison is monic. Every diagonal \(X_B\to X_B\times_X X_B\) is an isomorphism because \(m_B\) is monic. The transitions in (8.4) make these diagonals natural. Filtered finite-limit exactness, applied to the pullback diagram \(X_B\to X\leftarrow X_B\), identifies

\[ \operatorname{colim}_{B\in I}(X_B\times_X X_B) \xrightarrow{\sim} Z\times_X Z. \tag{8.6} \]

The constant identity \(X\)-diagram has colimit \(X\). The colimit of the diagonal isomorphisms is an isomorphism, since their natural inverses induce its inverse. On every \(d_B\), the transported map has both projections equal to \(d_B\); hence it is exactly the diagonal \(\delta_m:Z\to Z\times_X Z\). Its invertibility makes \(m\) monic by the complete diagonal cancellation test: if \(ma=mb\), the pullback factor with projections \(a,b\) has equal projections because the diagonal is invertible, so \(a=b\).

There is also the compatible coproduct colimit

\[ \operatorname{colim}_{B\in I}P_B \xrightarrow{\sim}P_A, \qquad\text{leg at }B\text{ is }P(\iota_B). \tag{8.7} \]

For completeness, a cocone \(h_B:P_B\to T\) gives, for every \(a\in A\), the map \(h_{\{a\}}j_a:G\to T\). These component maps define one \(h:P_A\to T\). For \(a\in B\), the actual inclusion \(\{a\}\subseteq B\) gives \(hP(\iota_B)j_a=h_Bj_a\); coproduct uniqueness gives \(hP(\iota_B)=h_B\). For empty \(B\), both maps have initial source. Conversely, restrictions of any \(h\) give the cocone, and the two constructions recover every component and every \(h_B\). They commute with postcomposition in \(T\). For empty \(A\), \(I\) has the sole object \(\varnothing\), and this is the identity colimit at \(P_\varnothing\).

The compatible maps \(d_Bq_B\) and (8.7) define \(v:P_A\to Z\). They satisfy \(vP(\iota_B)=d_Bq_B\). Therefore

\[ mvP(\iota_B)=m_Bq_B=uP(\iota_B) \quad\text{for every }B, \qquad mv=u. \tag{8.8} \]

The last equality follows from the colimit factor uniqueness in (8.7), or on every singleton component. Since \(u\) is epic, \(m\) is epic. By \(H\) it is strict, and we already proved it monic; Section 1 gives its inverse. Thus (8.5) is the specified isomorphism from the whole subcover colimit to \(X\). No blanket preservation of epimorphisms by a colimit functor has been invoked.

Only now use condition (b). It applies to the actual small \(\pi_0\)-filtered \(X_B\)-diagram. Its canonical comparison followed by \(\operatorname{Hom}(G,m)\) is a bijection

\[ \begin{gathered} \operatorname{colim}_{B\in I}\operatorname{Hom}(G,X_B) \xrightarrow{\sim}\operatorname{Hom}(G,X),\\ [B,h]\longmapsto m_Bh. \end{gathered} \tag{8.9} \]

Each \(q_B\) is a quotient of fewer than \(\pi_0\) copies of \(G\), so condition (d) gives \(|\operatorname{Hom}(G,X_B)|<\pi\). Formula (7.2) gives \(|I|<\pi\). Regularity of \(\pi\), used on this entire tagged family, gives

\[ \left|\coprod_{B\in I}\operatorname{Hom}(G,X_B)\right|<\pi. \tag{8.10} \]

Its Set-colimit is a quotient of that tagged union. Well-order the tagged union and choose the least representative of each equivalence class; this injects the quotient into it. The empty union has empty quotient and its unique empty injection. Combining (8.9) and (8.10) proves (8.1).

The two regularities have distinct jobs: \(\pi_0\) bounds the unions making \(I\) filtered; \(\pi\) bounds the final tagged union of Hom sets. Condition (c) bounds the number of stages, and (d) bounds every stage's probe. Accessibility of \(G\) is used precisely at (8.9), not inferred from detection. For empty \(A\), condition (d) itself includes the original quotient of the initial coproduct; there is no assumption that its probe is empty or that this quotient is initial. All empty and singleton stages remain in the diagram. \(\square\)

Worked example: a four-label quotient. In sets let \(G=1\), \(A=\{0,1,2,3\}\), and let \(u:A\twoheadrightarrow\{p,q\}\) send \(0,1,3\) to \(p\) and \(2\) to \(q\). With \(\pi_0=\aleph_0\), the index \(I\) contains all sixteen subsets. The coimage \(X_B\) is the set of fibres of \(u|_B\), compatibly identified with \(u(B)\), by its explicit class map. Its values are \(\varnothing,\{p\},\{q\},\{p,q\}\); its transitions are the actual inclusions of these images. Stage \(\{0,2\}\) already has image \(\{p,q\}\), but the proof retains every inclusion and every subset. For \(A=\varnothing\), the sole stage is empty and an epic Set map out of it has empty target.

Here conditions (6.1) hold with \(\pi_0=\aleph_0\) and \(\pi=(2^{\aleph_0})^+\). The singleton is \(\aleph_0\)-accessible by the complete small-set comparison. For \(\rho<\pi\), \(\rho^{\aleph_0}\leq(2^{\aleph_0})^{\aleph_0}=2^{\aleph_0}<\pi\). Quotients of finite sets are finite, including an empty source, which proves (d). This example uses an explicit parameter pair, not an assumption that every regular \(\pi\) automatically satisfies (c).

9. Naturality of the quotient comparison

The constructions retain their specified arrows under a morphism of covers. Suppose \(a:A\to A'\), \(t:X\to X'\), and \(t u=u'P(a)\). Use the same \(\pi_0\), and define the inclusion functor \(F_a:I_A\to I_{A'}\) by \(B\mapsto a(B)\). Its image cardinal is at most \(|B|\); every inclusion gives the actual inclusion between the images. Identity and composition hold for these set images.

For each \(B\), strict descent defines a unique arrow

\[ s_B:X_B\to X'_{a(B)}, \qquad s_Bq_B=q'_{a(B)}P(a|_B). \tag{9.1} \]

To check descent, the right side's two kernel-pair composites agree after the monic \(m'_{a(B)}\), since their composites there are \(t m_Bq_B\). Cancel that monomorphism. The quotient \(q_B\) then supplies (9.1), and its epiness gives \(m'_{a(B)}s_B=t m_B\). For an inclusion \(B\subseteq D\), the two naturality composites agree after \(q_B\) by the coproduct component equations, so agree. The same cancellation verifies identity and composite cover morphisms.

These stage maps induce a map \(z:Z\to Z'\) with \(z d_B=d'_{a(B)}s_B\). Checking those equations in (8.5) gives

\[ m' z d_B=t m d_B, \qquad m'z=tm. \tag{9.2} \]

Thus the compatible colimit isomorphism is natural in the cover. On a Hom representative, the two routes of (8.9) both give \(t m_Bh=m'_{a(B)}s_Bh\). Changing the chosen coimages instead gives their unique isomorphisms commuting with the quotient legs; (8.4) then makes them a natural isomorphism of the whole diagrams. Their colimit comparisons and inverses preserve (8.5) by uniqueness. This proves choice independence and naturality of the actual comparisons, rather than only an abstract isomorphism of the resulting objects.

10. Four graded exercises with full solutions

Exercise 1. Beginner: the empty subfamily

Let \(S\subseteq T\), and let \(P_E\) be the coproducts of copies of an arbitrary \(G\). Prove the required Hom injection for \(S=\varnothing\), distinguishing an empty and a nonempty \(\operatorname{Hom}(G,0)\). Give its values for sets with \(G=1\), and for abelian groups with \(G=\mathbb Z\). Explain why a retraction of the indexing sets is not the argument.

Solution. The unique \(u:0\to P_T\) defines \(h\mapsto uh\). If \(\operatorname{Hom}(G,0)=\varnothing\), it has empty domain, hence is injective. Otherwise take an existing \(a:G\to0\). The family with component \(a\) at every \(t\in T\) gives \(v:P_T\to0\). Initiality gives \(vu=1_0\). Therefore \(h\mapsto vh\) is a left inverse on the Hom sets, so \(uh=uh'\) implies \(h=h'\). For empty \(T\), the same component family is empty, \(P_T=0\), and both arrows are \(1_0\).

For sets with \(G=1\), the initial object is empty and there is no function \(1\to\varnothing\). Thus the Hom injection is \(\varnothing\to\operatorname{Hom}(1,T)\), including empty \(T\). For abelian groups, \(0\) is the zero group and \(\operatorname{Hom}(\mathbb Z,0)\) is the singleton consisting of the zero map. The coproduct \(P_T\) is the direct sum of copies of \(\mathbb Z\); \(u\) sends zero to zero and \(v\) is the zero homomorphism. The singleton Hom domain is sent to its zero map and the left inverse returns it. When \(T\ne\varnothing\), no set function \(T\to\varnothing\) exists; these valid categorical/Hom arguments do not use one. \(\square\)

Exercise 2. Intermediate: retain both parallel witnesses

Let \(I\) have objects \(0,1,2\), arrows \(r,s:0\rightrightarrows1\), \(t:1\to2\), \(u:0\to2\), and the relation \(tr=ts=u\), together with identities. In sets put \(X_0=\{a,b\}\), \(X_1=\{c,d\}\), \(X_2=\{z\}\). Let \(X(r)\) preserve the displayed order, \(X(s)\) reverse it, and \(X(t)\) be constant. Determine the colimit, the one-arrow witness for the two maps \(1\rightrightarrows X_0\) with values \(a,b\), and every equalizer stage in \((0\downarrow I)\). Explain why a two-arrow equality witness need not already be a one-arrow witness.

Solution. The functor laws hold because both composites to \(X_2\) take every point to \(z\), which defines \(X(u)\). Object \(2\) is terminal: its unique incoming nonidentity arrows are \(t,u\). Thus a cocone is determined by its component out of \(X_2\), and \(X_2\) is the specified colimit. Both original maps have the same colimit image.

At stage \(1\), \(X(r)(a)=c=X(s)(b)\), so the distinct arrows \(r,s\) witness equality of classes. But \(X(r)(a)=c\ne d=X(r)(b)\), and \(X(s)(a)=d\ne c=X(s)(b)\). Neither one alone witnesses the same-stage equality. Postcomposition with \(t\) equalizes \(r,s\), yielding the single actual arrow \(u=tr=ts\), and \(X(u)(a)=z=X(u)(b)\).

The coslice has objects \(1_0,r,s,u\). Its nonidentity arrows are the underlying \(r:1_0\to r\), \(s:1_0\to s\), \(u:1_0\to u\), and \(t:r\to u\), \(t:s\to u\), with the two composite equations. The equalizers of the transported maps from \(1\) are empty at \(1_0,r,s\), and are all of \(1\) at \(u\). Their transitions are the unique maps forced by inclusion into \(1\). The inclusion at \(u\) is the stage epimorphism; the others are not surjective and hence not epic in sets. Keeping both parallel witnesses and their common postarrow is exactly what turns equal colimit images into one genuine later-stage equality. \(\square\)

Exercise 3. Advanced: an epimorphism misses generator maps

In abelian groups take \(G=\mathbb Z\oplus\mathbb Z/2\) and \(p:Y=\mathbb Z\twoheadrightarrow A=\mathbb Z/2\). Prove that \(G\) detects isomorphisms, compute \(E=\operatorname{Hom}(G,Y)\), \(T=\operatorname{Hom}(G,A)\) and their image \(K\), and construct the lifted epic cover \(P_K\to Y\to A\). Check both bounds of (5.1) at \(\pi=\aleph_1\). Does the first bound alone meet the two-bound statement at \(\pi=\aleph_0\)?

Solution. A map from \(G\) is a pair of maps from its two summands. These Hom sets contain zero maps. If the product of their two induced functions is bijective, each factor function is bijective: fix zero maps in the other coordinate for injectivity and place a desired element with zero in the other target coordinate for surjectivity. In particular \(\operatorname{Hom}(\mathbb Z,v)\) is bijective. Evaluation at \(1\) identifies it with the underlying function of the group homomorphism \(v\); a bijective homomorphism has an additive inverse by applying \(v\) to each addition equation and canceling it. Hence \(G\) detects isomorphisms.

Every homomorphism \(\mathbb Z/2\to\mathbb Z\) is zero, since twice its value must be zero in \(\mathbb Z\). Thus \(E\cong\mathbb Z\): integer \(n\) specifies the image of the free summand's generator. A map \(G\to A\) is a pair \((a,b)\in(\mathbb Z/2)^2\), the images of those two generators, so \(T\) has four elements. The probe of \(p\) is

\[ n\longmapsto(n\bmod2,0), \qquad K=\{(0,0),(1,0)\}\subsetneq T. \tag{10.1} \]

In particular the map with \((a,b)=(0,1)\) does not lift. Choose section values \(0,1\) for the two elements of \(K\). Then \(P_K=G\oplus G\). Its lift is

\[ \ell(n_0,\epsilon_0,n_1,\epsilon_1)=n_1, \qquad p\ell=n_1\bmod2=\varepsilon_K. \tag{10.2} \]

This cover is surjective, hence epic: its second free summand already maps onto \(\mathbb Z/2\). Its component maps are exactly the two elements of \(K\), and its selected lifts are those in (10.2). No map corresponding to \((0,1)\) was required.

The first Hom set has size four. The object \(P_T=G^4\) has countably many elements, and its elements killed by two form the finite set \((\mathbb Z/2)^4\). Therefore

\[ \operatorname{Hom}(G,P_T) \cong P_T\times(P_T[2]) \tag{10.3} \]

is countably infinite: a homomorphism is exactly an arbitrary free-generator value and a value killed by two, with their independent inverses by defining on the summands. Finite powers of the countable integers are countable by the proved infinite square. Thus both bounds hold below \(\aleph_1\). At \(\aleph_0\), the first bound holds but the second does not. The two-bound proposition therefore cannot be applied at \(\aleph_0\) from these data; this is not a claim that \(A\) itself fails ordinary accessibility. The example demonstrates why epiness of \(p\) is not surjectivity of its probe and why the second bound cannot be silently discarded from this proof. \(\square\)

Exercise 4. Expert: transport every subcover and its comparison

Under \(H\) and (6.1), take two covers \(u:P_A\twoheadrightarrow X\), \(u':P_{A'}\twoheadrightarrow X'\), with both index sizes below \(\pi\), and a morphism of covers \((a,t)\) as in Section 9. Construct every stage map between their coimage diagrams, prove identity and composite laws, and prove the resulting colimit and Hom comparisons natural, including empty source subsets. Identify separately the assumptions used to establish the isomorphisms and to establish the cardinal bound.

Solution. A subset \(B\) of size below \(\pi_0\) has image \(a(B)\) of size at most \(|B|\); an inclusion maps to an inclusion. Thus \(B\mapsto a(B)\) is a functor on the entire inclusion category. With \(a_B:B\to a(B)\) its actual restricted function, define \(h_B=q'_{a(B)}P(a_B):P_B\to X'_{a(B)}\). If \(r_0,r_1\) are the kernel-pair projections of \(q_B\), then

\[ m'_{a(B)}h_Br_0 =t m_Bq_Br_0 =t m_Bq_Br_1 =m'_{a(B)}h_Br_1. \tag{10.4} \]

The coimage factor \(m'_{a(B)}\) is monic under \(H\), so cancel it. Strictness of the epic \(q_B\) descends \(h_B\) uniquely to \(s_B:X_B\to X'_{a(B)}\). Canceling \(q_B\) gives \(m'_{a(B)}s_B=t m_B\).

For \(B\subseteq D\), both \(x'_{a(B),a(D)}s_B\) and \(s_Dx_{BD}\) become \(q'_{a(D)}P(B\to a(D))\) after \(q_B\), by their defining equations. They are equal. For the identity cover morphism, \(1_{X_B}\) satisfies the same descent equation and is its unique factor. For successive cover morphisms \((a,t)\), \((a',t')\), their two successive stage maps compose, after \(q_B\), to the map induced by \(a'a|_B\). Epic cancellation proves that this composite is the stage map for \((a'a,t't)\). All laws involve the original arrows.

The maps \(d'_{a(B)}s_B\) are a cocone, so give a unique \(z:Z\to Z'\). On every \(d_B\), the equations yield \(m'z d_B=t m_B=tm d_B\). Colimit uniqueness gives \(m'z=tm\); it also gives identity and composite laws for \(z\). Since the main proof made \(m,m'\) invertible, their inverses satisfy the same naturality after cancellation. On each probe representative \([B,h]\), both Hom routes have value \(t m_Bh=m'_{a(B)}s_Bh\). Every quotient class has a representative, so that equation proves naturality of the whole Hom comparison, and hence of its inverse.

For \(B=\varnothing\), \(a(B)=\varnothing\), and \(P(a_B)\) is the specified identity of the initial coproduct. The same kernel-pair, monic cancellation and strict descent argument applies. An empty entire index set \(A\) still gives the nonempty subset category with its one empty object, so none of the colimit arguments is over an empty filtered category.

The isomorphism \(m\) uses regular \(\pi_0\) to make the subset diagram filtered, finite-limit exactness to prove monicity, the singleton-component coproduct colimit to prove epiness, and all epimorphisms strict to turn both into invertibility. To bound its probe, (b) supplies the exact Hom comparison, (c) and the padded coding bound the number of stages below \(\pi\), (d) bounds every stage probe, and regular \(\pi\) bounds their entire tagged union. The Set quotient then cannot increase that cardinal. None of these roles can be replaced by assuming that the probe preserves epimorphisms. \(\square\)

References and proof interfaces