#Contents# * table of contents {:toc} ## Definition ## 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: $$p: (f^{-\infty}(R) \subseteq T) \times \left(f^{-\infty}(R) \cong \sum_{x:S} \left[\sum_{b:f^{-\infty}(R)} f(x) = b\right]\right)$$ ## See also ## * [[inverse image]] * [[iterated inverse image]] category: not redirected to nlab yet