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

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 April 16, 2022 at 07:57:50 by Anonymous?. See the history of this page for a list of all contributions to it.