#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 [[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$$ ## See also ## * [[inverse image]] * [[infinitely iterated inverse image]] category: not redirected to nlab yet