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

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 inverse image f 1(R)f^{-1}(R) by definition is a subtype of SS and thus a subtype of TT. One could restrict the domain of ff to f 1(R)f^{-1}(R) and the codomain of ff to RR, and find the inverse image of f 1(R)f^{-1}(R) under ff, or the 2-fold iterated inverse image of RR under ff:

f 2(R) x:S b:f 1(R)f(x)=bf^{-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)f^{-n}(R) representing the nn-fold iterated inverse image of RR under ff.

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

See also

Revision on June 15, 2022 at 22:54:59 by Anonymous?. See the history of this page for a list of all contributions to it.