Image of a function

[felixwellen]

Construct the image, show that an embedding, (co-)restricted to its image is an equivalence.

(see this external issue: https://github.com/felixwellen/synthetic-geometry/issues/12)

[mortberg]

Great! Merging once the CI is finished