Bounded subfunctor solution set for precomposition (source code)

= Bounded subfunctor solution set for precomposition
{title2=$Q\longrightarrow GF\text{ factors through }G'F,\quad |G'(d)|\leq\kappa$}

For <small categories> $\mathcal C,\mathcal D$, a <functor> $F:\mathcal C\to\mathcal D$ and $Q:\mathcal C\to\mathbf{Set}$, choose an infinite <cardinal number> $\kappa$ bounding the number of <morphisms> of $\mathcal D$ and the total number of elements of $Q$. Given a <natural transformation> $\eta:Q\to GF$, generate a subfunctor $G'\subseteq G$ from all $\eta_c(x)$ by applying every outgoing $\mathcal D$-<morphism>. Each $G'(d)$ has at most $\kappa$ elements. Label bounded values by subsets of $\kappa$; only a <set> of such <functors> and transformations exists. These factorizations give the <solution-set condition> for precomposition, whose <left adjoint> is the <left Kan extension>.