# Homotopy Type Theory infinitely iterated inverse image > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

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