Homotopy Type Theory infinitely iterated inverse image > history (Rev #1)

Contents

Definition

For every type TT and subtype STS \subseteq T, let f:STf:S \to T be a function from the subtype SS to TT. Given any subtype RTR \subseteq T, the infinitely iterated inverse image is defined as the maximal subtype f (R)Tf^{-\infty}(R) \subseteq T such that the inverse image of f (R)f^{-\infty}(R) under ff is equivalent to f (R)f^{-\infty}(R) itself:

p:(f (R)T)×(f (R) x:S[ b:f (R)f(x)=b])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

Revision on April 16, 2022 at 08:16:32 by Anonymous?. See the history of this page for a list of all contributions to it.