Definition finsum {X} (fin : isfinite X) (f : X -> nat) : nat. Proof. intros. unfold isfinite,finstruct,nelstruct in fin. simple refine (squash_to_set isasetnat (λ (x : ∑ n, stn n ≃ X), iterop_fun_mon (M := nataddabmonoid) (f ∘ pr2 x)) _ fin). intros. induction x as [n x]. induction x' as [n' x']. assert (p := weqtoeqstn (invweq x' ∘ x)%weq). induction p. assert (w := nat_plus_commutativity (f ∘ x') (invweq x' ∘ x)%weq). simple refine (_ @ w). unfold iterop_fun_mon. apply maponpaths. rewrite weqcomp_to_funcomp. apply funextfun; intro i. simpl. apply maponpaths. exact (! homotweqinvweq x' (x i)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.