Refactor coproduct equivalences

[morphismz]

Refactors some equivalences related to coproducs and adds one new definition.

• removes the abstract block around is-equiv-coproduct in foundation.functorality-coproduct-types, thus allowing map-inv-equiv (equiv-coproduct e e') to compute to map-coproduct (map-inv-equiv e) (map-inv-equiv e'). We keep abstract blocks around the proof that the inverse map is a section and retraction

• computes the underlying map of the equivalence Fin-add-ℕ in univalent-combinatorics.coproduct-types

[fredrik-bakke]

Thanks for the contribution, and apologies for taking so long! I have a couple of requests on naming and good-practice definitions.

[morphismz]

Hey @fredrik-bakke No worries for the delay, and sorry for the delay on my end :). I'll implement these changes this weekend.

[VojtechStep]

@morphismz I'm marking this one as a draft for now, feel free to get back to it when you have time

[fredrik-bakke]

I'm picking up this PR so it can be merged.