Lemma helper_D (P:nat->Type) (p0:P 0) (IH:∏ n, P n->P(S n)) : (∑ f:∏ n, P n, (f 0=p0) × (∏ n, f(S n)=IH n (f n))) ≃ (@hfiber (∑ (f:∏ n, P n), ∏ n, f(S n)=IH n (f n)) (P 0) (λ fh, pr1 fh 0) p0). Proof. intros. simple refine (make_weq _ (isweq_iso _ _ _ _)). { intros [f [h0 h']]. exact ((f,,h'),,h0). } { intros [[f h'] h0]. exact (f,,(h0,,h')). } { intros [f [h0 h']]. reflexivity. } { intros [[f h'] h0]. reflexivity. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.