Suppose $\mathbb{X}$ and $\mathbb{Y}$ are classes, and $f:\mathbb{X}\rightarrow\mathbb{Y}$. It seems like pretty standard course to consider an 'induced function' $f:\mathcal{P}\mathbb{X}\rightarrow\mathcal{P}\mathbb{Y}$ defined by $f(U)=\{f(u):u\in U\}$ for all $U\in\mathcal{P}\mathbb{X}$, and $f=\langle f(U):U\in\mathcal{P}\mathbb{X}\rangle$ (where we have abused the symbol $f$ in a safe way since the former function induces the latter and vice-verse by the image of singletons). 


This is done when considering the continuity of a function in topology, for example, since we actually want to consider the preimage of open sets of $\mathbb{Y}$ under the mapping $f:\mathcal{P}\mathbb{X}\rightarrow\mathcal{P}\mathbb{Y}$ instead of individual elements.


I was wondering if this behaviour had been formalized and studied, particularly the suggested inductive tower of functions defined by $$f\_0=f:\mathbb{X}\rightarrow\mathbb{Y},$$ $$f\_{n+1}=\langle f\_n(U):U\subseteq dmn f\_n\rangle,$$ so $dmnf\_0=\mathbb{X},\ dmnf\_1=\mathcal{P}\mathbb{X},\dots,dmnf\_n=\mathcal{P}^n\mathbb{X}=\mathcal{P}\dots\mathcal{P}\mathbb{X}$. I believe we could further define $$\mathcal{P}^\omega\mathbb{X}=\bigcup\_{n<\omega}\mathcal{P}^n\mathbb{X},$$ or perhaps $$\mathcal{P}^\omega\mathbb{X}=\{\mathcal{U}:\mathcal{U}\subseteq\bigcup\_{n<\omega}\mathcal{P}^n\mathbb{X}\},$$ and then define $f\_\omega:\mathcal{P}^\omega\mathbb{X}\rightarrow\mathcal{P}^\omega\mathbb{Y}$ in the same fashion as above and extend the recursion on $\omega$ to a recursion on all of $O\_n$ where we repeat the above step each time we encounter a limit ordinal. This would allow for the construction of an inductive tower of functions $\{f\_\alpha\}\_{\alpha\in O\_n}$, where each successor function $f\_{n+1}$ is, in general, much more complicated than $f\_n$ (for example if $f\_n$ is defined on a countable set then $f\_{n+1}$ will be defined on an uncountable set, so on and so forth, and it also seems like $f\_{n+1}$ carries the 'topological information' about $f\_n$ in some sense), but all members of the tower are faithfully induced by some single base function.


I thought that perhaps a model theorist or a set theorist had written something about this somewhere that I could read to enlighten myself, or that perhaps one of the members here could see some obvious connection to a more well-known area of mathematics.


**EDIT:** Another place where it appears we are implicitly thinking in this manner is fibrations -- the Hopf fibration $p:S^3\rightarrow S^2$ seems to be the unique function from $S^3$ to $S^2$ whose induced function $p\_1:\mathcal{P}S^3\rightarrow\mathcal{P}S^2$ has the property that $p\_1^{-1}(U)$ is a circle in $S^3$ iff $U$ is a singleton. I believe that higher geometrical thinking can also be done in this fashion, since all the 'shapes' in $\mathbb{R}^n$ are elements of $\mathcal{P}\mathbb{R}^n$, so functions to lower dimensional spaces whose induced functions map certain kinds of subsets onto singletons should be fibrations of some type. 


My question is really whether or not there are books/articles/papers already written which explore this approach, understanding higher order properties of functions in terms of induced functions on higher order powersets rather than considering the action of a element-wise function on a subset/collection of subsets etc.



Towers of induced functions
If you work in ZFA (ZF with atoms), and if $A$ is the class (or set) of atoms, and $f:A\to A$ is a permutation, then $f$ will (inductively, as you have described) induce a permutation $\bar f$ of the whole universe $V\_A$, where $V\_A = \bigcup\_{\alpha\in ORD} V\_{A,\alpha}$, 
$V\_{A,0}=A$, $V\_{A,\alpha+1} = A \cup {\mathcal P}V\_{A,\alpha}$, $V\_{A,\delta} = \bigcup\_{\alpha < \delta} V\_{A,\alpha}$ for limit ordinals $\alpha$. 


Such maps $f$ and $\bar f$ have been studied a long time ago; they can be used to construct a "Fraenkel-Mostowski model"; in this model (of ZFA) the axiom of choice fails. 


