Homotopy Type Theory infinitely iterated inverse image > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed


< infinitely iterated preimage


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

Last revised on June 17, 2022 at 23:01:35. See the history of this page for a list of all contributions to it.