Type-theoretic replacement with higher induction-recursion

[ecavallo]

A nice way to construct it quickly, though it uses a stronger tool than is necessary.

[mortberg]

Nice! Please add an equivalence with the image that already exist in Functions.Image. Maybe also add a simpler construction for sets?

[ecavallo]

I proved the equivalence (actually uniqueness of image factorizations more generally). The case for sets I think can wait for another PR.

[felixwellen]

All good now -> merging.

[felixwellen]

Hope it works with current master...