Homotopy Type Theory fiber > history (changes)

Showing changes from revision #4 to #5: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~
~~A fiber of a function $f:A \to B$ over a term $b:B$ is the type~~
~~$fiber(f, b) \coloneqq \sum_{a:A} f(a) = b$~~
~~See also~~

inverse image

image

equivalence

univalence

monic function

epic function?

~~category: not redirected to nlab yet~~

Last revised on June 17, 2022 at 22:11:23. See the history of this page for a list of all contributions to it.