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

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

Contents

Definition

For types TT and SS, let f:STf:S \to T be a function from SS to TT. Given any subtype RTR \subseteq T, the inverse image of RR under ff is defined as

f 1(R):= x:S b:Rf(x)=bf^{-1}(R) := \sum_{x:S} \Vert \sum_{b:R} f(x) = b \Vert

See also

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