Lemma helper_A (P:nat->Type) (p0:P 0) (IH:∏ n, P n->P(S n)) (f:∏ n, P n) : weq (∏ n, f n = nat_rect P p0 IH n) (f 0=p0 × ∏ n, f(S n)=IH n (f n)). Proof. intros. simple refine (_,,isweq_iso _ _ _ _). { intros h. split. { exact (h 0). } { intros. exact (h (S n) @ maponpaths (IH n) (! h n)). } } { intros [h0 h'] ?. induction n as [|n' IHn']. { exact h0. } { exact (h' n' @ maponpaths (IH n') IHn'). } } { simpl. intros h. apply funextsec; intros n; simpl. induction n as [|n IHn]. { simpl. reflexivity. } { simpl. rewrite <- path_assoc. simple refine (_ @ pathscomp0rid _). rewrite <- maponpathscomp0. rewrite IHn. rewrite pathsinv0l. simpl. reflexivity. } } { intros [h0 h']. apply maponpaths. apply funextsec; intro n; simpl. rewrite <- path_assoc. rewrite <- maponpathscomp0. rewrite pathsinv0r. apply pathscomp0rid. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.