proposition: Lemma equiv_PropTrunc_rec `{Funext} (A P : Type) `{IsHProp P} : (PropTrunc A -> P) <~> (A -> P).
proof: Proof. refine (_ oE equiv_colim_seq_rec _ P). srapply equiv_iff_hprop. { intros h. exact (h 0). } intros f. induction n. - exact f. - cbn. srapply Join_rec. 1,2: assumption. intros a b. rapply path_ishprop. Defined.
imports: Basics Types Diagrams.Sequence Homotopy.Join.Core Colimits.Colimit Colimits.Sequential