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.

[fredrik-bakke]

Looks to me like you should define

map-equiv-coproduct = map-coproduct (map-equiv f) (map-equiv g)

and

map-inv-equiv-coproduct = map-coproduct (map-inv-equiv f) (map-inv-equiv g)

And then this should be

is-section map-equiv-coproduct map-inv-equiv-coproduct

[fredrik-bakke]

Same as above

is-retraction map-equiv-coproduct map-inv-equiv-coproduct

[fredrik-bakke]

I see that the original name Fin-add-ℕ is not your fault, but having a capitalized word (Fin) before an uncapitalized one (add) is a sure sign that the naming should be improved.

I think better names for the entries in this file would be, in order,

• coproduct-Fin -> compute-coproduct-Fin
• map-coproduct-Fin -> map-compute-coproduct-Fin
• Fin-add-ℕ -> inv-compute-coproduct-Fin, and then please add a definition for map-inv-compute-coproduct-Fin
• inl-coproduct-Fin is fine
• inr-coproduct-Fin is fine
• map-Fin-add-ℕ -> map-compute-map-inv-compute-coproduct-Fin (since the maps are not definitionally the same)
• compute-map-Fin-add-ℕ -> compute-map-inv-compute-coproduct-Fin

Could you please make these renamings as part of this pull request?

[fredrik-bakke]

After my above suggested renamings

Suggested change

	(k l : ℕ) → map-equiv (Fin-add-ℕ k l) ~ map-Fin-add-ℕ k l
	(k l : ℕ) →
	map-inv-compute-coproduct-Fin k l ~
	map-compute-map-inv-compute-coproduct-Fin k l

[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