# Contents

## 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)$