I just remembered something, see Proposition 2.9.
Given the presheaf \(H_X\in \hat I\), assigning to each \(i\in I\) the set \(H(i,X)\) the inclusions \(\iota_X:{\bf H}_X\to {\hat I}_{/H_X}\) are just the yoneda embedding!
In fact the much complex and richer universe of \( {\hat I}_{/H_X} \), i.e. the category of presheaf homomorphism with codomain \(H_X\), is just a presheaf category itself!!
By proposition 2.9, the slice topos \((\widehat {\mathcal C})_{/F}\) over a presheaf \(F\) is equivalent to the topos of presheaves over the category of elements of \(F\)
This can be applied to our case and we get \( \widehat { I} _{/H_X} \cong \widehat {{\bf H}_X} \)
This enable a second analysis of \(\bf H_X\):
Given the presheaf \(H_X\in \hat I\), assigning to each \(i\in I\) the set \(H(i,X)\) the inclusions \(\iota_X:{\bf H}_X\to {\hat I}_{/H_X}\) are just the yoneda embedding!
In fact the much complex and richer universe of \( {\hat I}_{/H_X} \), i.e. the category of presheaf homomorphism with codomain \(H_X\), is just a presheaf category itself!!
By proposition 2.9, the slice topos \((\widehat {\mathcal C})_{/F}\) over a presheaf \(F\) is equivalent to the topos of presheaves over the category of elements of \(F\)
\( \widehat {\mathcal C} _{/F} \cong \widehat {\int_ {\mathcal C} F} \)
This can be applied to our case and we get \( \widehat { I} _{/H_X} \cong \widehat {{\bf H}_X} \)
This enable a second analysis of \(\bf H_X\):
- the inlcusion \(\iota_X:{\bf H}_X\to {\hat I}_{/H_X}\) help us by seeing \(\bf H_X\)'s objects, eg. iterations, ackermann functions, goodstein maps, as actual homomorphisms, i.e. categorically;
- the yoneda maps \(y_X:{\bf H}_X\to \widehat {{\bf H}_X}\) make us see iterations, ackermann functions or goodstein maps as spaces of some exotic flavours. This mean we can perform sums, products, limits, glueing, functional spaces, subspaces and study the intrinsic logic of their parts.
Mother Law \(\sigma^+\circ 0=\sigma \circ \sigma^+ \)
\({\rm Grp}_{\rm pt} ({\rm RK}J,G)\cong \mathbb N{\rm Set}_{\rm pt} (J, \Sigma^G)\)

![[Image: immagine.png]](https://i.ibb.co/BVs7bPNd/immagine.png)