For every type $T$ and subtype $S \subseteq T$, let $f:S \to T$ be a function from the subtype $S$ to $T$. Given any subtype $R \subseteq T$, the inverse image$f^{-1}(R)$ by definition is a subtype of $S$ and thus a subtype of $T$. One could restrict the domain of $f$ to $f^{-1}(R)$ and the codomain of $f$ to $R$, and find the inverse image of $f^{-1}(R)$ under $f$, or the 2-fold iterated inverse image of $R$ under $f$:

One could repeat this definition indefinitely, which could be formalised by the dependent types $f^{-n}(R)$ representing the $n$-fold iterated inverse image of $R$ under $f$.