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

$f^{-2}(R) \coloneqq \sum_{x:S} \Vert \sum_{b:f^{-1}(R)} f(x) = b\Vert$

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$.

$f^{-0}(R) \coloneqq R$
$n:\mathbb{N} \vdash f^{-(n+1)}(S) \coloneqq \sum_{x:S} \Vert\sum_{b:f^{-(n)}(R)} f(x) = b\Vert$