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
Refactors some equivalences related to coproducs and adds one new definition.
removes the abstract block around
is-equiv-coproduct
infoundation.functorality-coproduct-types
, thus allowingmap-inv-equiv (equiv-coproduct e e')
to compute tomap-coproduct (map-inv-equiv e) (map-inv-equiv e')
. We keep abstract blocks around the proof that the inverse map is a section and retractioncomputes the underlying map of the equivalence
Fin-add-ℕ
inunivalent-combinatorics.coproduct-types