Lemma helper_C (P:nat->Type) (p0:P 0) (IH:∏ n, P n->P(S n)) : (∑ f:∏ n, P n, f = nat_rect P p0 IH) ≃ (∑ f:∏ n, P n, f 0=p0 × ∏ n, f(S n)=IH n (f n)). Proof. intros. apply weqfibtototal. intros f. apply helper_B. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.