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

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



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 June 10, 2022 at 15:21:57 by Anonymous?. See the history of this page for a list of all contributions to it.