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 infinitely iterated inverse image is defined as the maximal subtype $f^{-\infty}(R) \subseteq T$ such that the inverse image of $f^{-\infty}(R)$ under $f$ is equivalent to $f^{-\infty}(R)$ itself: