Definition FiniteSetSum {I : FiniteSet} (X : I -> FiniteSet) : FiniteSet. Proof. intros. exists (∑ i, X i). apply isfinitetotal2. - exact (pr2 I). - exact (λ (i : I), pr2 (X i)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.