Definition weqstnsum1_prelim {n : nat} (f : ⟦n⟧ -> nat) : (∑ i, ⟦f i⟧) ≃ ⟦stnsum f⟧. Proof. revert f. induction n as [ | n' IHn ]. { intros f. apply weqempty. - exact (negstn0 ∘ pr1). - exact negstn0. } intros f. change (⟦stnsum f⟧) with (⟦stnsum (f ∘ dni lastelement) + f lastelement⟧). use (weqcomp _ (weqfromcoprodofstn _ _)). use (weqcomp (weqoverdnicoprod _) _). apply weqcoprodf1. apply IHn. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.