Theorem weqstnsum { n : nat } (P : ⟦n⟧ -> UU) (f : ⟦n⟧ -> nat) : (∏ i, ⟦f i⟧ ≃ P i) -> total2 P ≃ ⟦stnsum f⟧. Proof. intros w. intermediate_weq (∑ i, ⟦f i⟧). - apply invweq. apply weqfibtototal. assumption. - apply weqstnsum1. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.