Homotopy Type Theory image > history (Rev #3)

Definition

Given a function $f:A \to B$ , we define the propositional image of $f$ as

\mathrm{im}(f) \coloneqq \sum_{y:B} \left[\mathrm{fiber}(f, y)\right]

See also

References

Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson, Symmetry book (2021)

category: not redirected to nlab yet

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