Functoriality of chosen representations (source code)

= Functoriality of chosen representations

If $H:\mathcal A^{\mathrm{op}}\times\mathcal B\to\mathbf{Set}$ has chosen representations $\psi_B:\mathcal A(-,GB)\cong H(-,B)$, the <Yoneda lemma> determines a unique <functor> $G$ on morphisms by $\mathcal A(-,Gb)=\psi_{B'}^{-1}H(-,b)\psi_B$. This makes the representing <natural isomorphisms> natural in $B$.