proposition: Corollary weqstnsum2 { X : UU } {n : nat} (f : ⟦n⟧ -> nat) (g : X -> ⟦n⟧ ) : (∏ i, ⟦f i⟧ ≃ hfiber g i) -> X ≃ ⟦stnsum f⟧.
proof: Proof. intros w. use (weqcomp _ (weqstnsum _ _ w)). apply weqtococonusf. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions